Prove hub excess 4h(h+1) for every hub count (no new κ)

research/p112-hub-excess-all-h/PROOF.md

@@ -0,0 +1,222 @@
+# The hub excess is exactly 4h(h+1) for every hub count
+
+## Setting
+
+This is the model of unpaidmoon's
+[PR4145](https://github.com/CrocSwap/integer-mult-bounds/pull/4145)
+(`research/p112-third-hub-extremal/PROOF.md`), unchanged. Work over a field of
+characteristic zero. For \(h \ge 1\), take independent \(E,F,G,V_0,\ldots,V_{h-1}\)
+and the \(3+3h\) queries
+
+\[
+g=G,\quad d=E+F,\quad t=E+F+G,\qquad
+v_j=V_j,\quad x_j=E+G-V_j,\quad y_j=F+G-V_j .
+\]
+
+A **minimal \(M\)-reader** is a query set whose span contains the mark \(M\)
+while no proper subset's span does. A **maximal \(M\)-source** is a query set
+\(S\) with \(M \notin \operatorname{span}(O,S)\), where \(O\) is the other
+mark, such that adding any further query puts \(M\) in the span. Each reader
+and each source is one row. A reader row costs the least number of its queries
+that an evaluator \(\phi\) with \(\phi(M)=1,\ \phi(O)=0\) must leave nonzero;
+a source row costs the least number of nonzero queries over every minimal
+\(M\)-reader, with the evaluator also vanishing on the source. The charge is
+twice the summed row costs, and the baseline is twice the number of rows.
+`verify.py` implements these definitions literally as paid-set searches.
+
+PR4145 proves that the \(h(h+1)\) masks of its families A–C give
+\(2h(h+1)\) rows of cost exactly 2 for every \(h\), so the excess is at least
+\(4h(h+1)\). It establishes the extremal table, and hence equality, only for
+\(h \le 3\). This file proves equality for every \(h\).
+
+**Theorem.** For every \(h \ge 1\):
+
+1. the minimal \(E\)-readers are exactly the \(3h(h+1)\) sets listed in PR4145
+   (six per hub, six per pair of hubs);
+2. the maximal \(E\)-sources are exactly the \(2^{h+1}\) sets: anchor \(g\)
+   with, for each hub, \(\{x_j\}\) or \(\{v_j,y_j\}\); or anchor \(t\) with, for
+   each hub, \(\{v_j,x_j\}\) or \(\{y_j\}\);
+3. the \(F\) rows are the images of the \(E\) rows under \(\sigma\) below;
+4. every row outside families A–C costs exactly 1.
+
+Hence the table has \(2\bigl(3h(h+1)+2^{h+1}\bigr)\) rows, the minimum charge is
+\[
+16h(h+1)+2^{h+3},
+\]
+and the excess over the one-unit baseline is exactly \(4h(h+1)\).
+
+At \(h=1,2,3\) this gives charges 48, 128 and 256, as PR4145 reports. At
+\(h=4\) and \(h=5\) it gives 448 and 736, with excesses 80 and 120.
+
+**Symmetry.** The linear map \(\sigma\) exchanging \(E\) and \(F\) and fixing
+\(G\) and every \(V_j\) fixes \(g,d,t,v_j\) and exchanges \(x_j\) with \(y_j\).
+It maps \(E\)-rows bijectively to \(F\)-rows of the same cost. So it suffices
+to treat \(M=E\), \(O=F\).
+
+Only integer vectors occur below. Over a field of characteristic zero their
+linear relations are those over \(\mathbb Q\), so the finite checks over
+\(\mathbb Q\) in `verify.py` apply to every such field.
+
+## Readers
+
+**Lemma 1 (hub shape).** Let \(S\) be a minimal \(E\)-reader. Then \(S\) is
+linearly independent, the expression \(E=\sum_{q\in S}\lambda_q q\) is unique
+and every \(\lambda_q\ne0\). For each hub, \(S_j=S\cap\{v_j,x_j,y_j\}\) is
+empty or one of
+\[
+a=\{v_j,x_j\},\quad b=\{v_j,y_j\},\quad c=\{x_j,y_j\},\quad m=\{v_j,x_j,y_j\},
+\]
+and the hub contributes \(\lambda_{x_j}(E+G)+\lambda_{y_j}(F+G)\). For kinds
+\(a,b,c\) this is a nonzero multiple of
+\[
+w_a=E+G,\qquad w_b=F+G,\qquad w_c=E-F .
+\]
+
+*Proof.* If \(S\) were dependent, subtracting a multiple of a relation would
+zero a coefficient and give a smaller reader. The \(V_j\)-coordinate of the
+expression gives \(\lambda_{v_j}=\lambda_{x_j}+\lambda_{y_j}\) (absent queries
+have coefficient 0). A single query cannot satisfy this with a nonzero
+coefficient. For \(\{v_j,x_j\}\), \(\lambda_{v_j}=\lambda_{x_j}\) and the
+contribution is \(\lambda_{x_j}w_a\); for \(\{v_j,y_j\}\) it is
+\(\lambda_{y_j}w_b\); for \(\{x_j,y_j\}\), \(\lambda_{y_j}=-\lambda_{x_j}\) and it
+is \(\lambda_{x_j}w_c\). \(\square\)
+
+**Lemma 2 (no repeated kind, no full hub).** In a minimal \(E\)-reader no two
+hubs have the same kind among \(a,b,c\), the kinds \(a,b,c\) never all occur,
+and no hub has kind \(m\).
+
+*Proof.* Each case gives a nontrivial relation inside \(S\), contradicting
+independence: \((v_i+x_i)-(v_j+x_j)=0\) for two hubs of kind \(a\), and
+likewise for \(b\) and \(c\);
+\((v_i+x_i)-(v_j+y_j)-(x_k-y_k)=0\) for kinds \(a,b,c\). If hub \(j\) has kind
+\(m\), any other touched hub \(i\) contains one of \(a,b,c\), and the same
+two-term relations with hub \(j\) apply. So hub \(j\) is the only touched hub
+and \(S=\{v_j,x_j,y_j\}\cup C\) with \(C\subseteq\{g,d,t\}\). Here
+\(\operatorname{span}(S)=\langle V_j\rangle\oplus\bigl(\langle w_a,w_b\rangle+
+\operatorname{span}C\bigr)\), so independence forces
+\(2+|C|\le3\). Since \(E\notin\langle w_a,w_b\rangle\), \(|C|=1\). For each
+\(q\in\{g,d,t\}\) the unique solution of
+\(E=\lambda_x w_a+\lambda_y w_b+\mu q\) has \(\lambda_y=0\) (\(q=g\)),
+\(\lambda_x+\lambda_y=0\) (\(q=d\)) or \(\lambda_x=0\) (\(q=t\)). Each
+makes a coefficient of \(S\) zero. `verify.py` checks these three systems.
+\(\square\)
+
+**Lemma 3 (reduced circuits).** In the seven vectors
+\(E,\ g,\ d,\ t,\ w_a,\ w_b,\ w_c\) of \(\langle E,F,G\rangle\), the independent sets
+\(T\subseteq\{g,d,t,w_a,w_b,w_c\}\) expressing \(E\) with all coefficients
+nonzero are exactly the nine sets
+\[
+\{g,w_a\},\ \{d,t,w_a\},\ \{g,d,w_b\},\ \{t,w_b\},\ \{d,w_c\},\ \{g,t,w_c\},\
+\{d,w_a,w_b\},\ \{t,w_a,w_c\},\ \{g,w_b,w_c\}.
+\]
+
+*Proof.* A finite check of all 63 nonempty subsets by exact elimination
+(`verify.py`, `check_core`). For example
+\(E=w_a-g=d+w_a-t=\tfrac12(d+w_c)=\tfrac12(d+w_a-w_b)\). \(\square\)
+
+**Proposition 1 (all readers).** The minimal \(E\)-readers are exactly the
+lifts of the nine sets of Lemma 3, where each \(w_\kappa\) in \(T\) is
+replaced by the kind-\(\kappa\) pair of a hub, distinct kinds using distinct
+hubs. There are \(6h+3h(h-1)=3h(h+1)\) of them, and they are the PR4145 list.
+
+*Proof.* By Lemmas 1 and 2, a minimal reader \(S\) determines
+\(T=C\cup\{w_\kappa:\kappa\text{ a hub kind in }S\}\) with distinct kinds. The
+expression of \(E\) descends to \(T\) with nonzero coefficients. \(T\) is
+independent: a relation on \(T\) lifts, through \(w_a=v_j+x_j\),
+\(w_b=v_j+y_j\), \(w_c=x_j-y_j\), to a nontrivial relation on \(S\). So \(T\) is
+one of the nine sets.
+
+Conversely, lift one of the nine sets with an injective hub assignment. The
+lifted expression of \(E\) has every coefficient nonzero. A relation
+\(\sum\mu_q q=0\) on the lift satisfies \(\mu_{v_j}=\mu_{x_j}+\mu_{y_j}\) on
+every hub, so each hub's part is a multiple of its \(w_\kappa\). The relation
+descends to \(T\), where it is trivial, and then every \(\mu_q=0\). An
+independent set expressing \(E\) with full support is a minimal reader.
+Distinct choices give distinct sets. Six of the nine sets use one hub kind
+and three use two, so the count is \(6h+3h(h-1)\). Writing out the lifts gives
+the PR4145 list: one-hub sets \((g,v_j,x_j)\), \((d,t,v_j,x_j)\),
+\((g,d,v_j,y_j)\), \((t,v_j,y_j)\), \((d,x_j,y_j)\), \((g,t,x_j,y_j)\), and the
+two orientations of \(\{d,w_a,w_b\}\), \(\{t,w_a,w_c\}\), \(\{g,w_b,w_c\}\) on
+each pair of hubs. \(\square\)
+
+## Sources
+
+**Lemma 4 (all sources).** The maximal \(E\)-sources are exactly the sets
+\(Z_\phi=\{q:\phi(q)=0\}\) for linear functionals \(\phi\) with
+\(\phi(E)=1\), \(\phi(F)=0\), \(\phi(G)=\gamma\in\{0,-1\}\) and each
+\(\nu_j=\phi(V_j)\) chosen so that hub \(j\) has a zero query. These are the
+\(2^{h+1}\) sets of part 2 of the theorem.
+
+*Proof.* The queries with \(F\) span the whole space \(\mathbb F^{3+h}\). Let
+\(S\) be a maximal source and \(W=\operatorname{span}(F,S)\). If
+\(\dim W\le 1+h\), some query \(q\) lies outside \(W+\langle E\rangle\).
+Maximality gives \(E\in W+\langle q\rangle\), hence \(q\in W+\langle E\rangle\),
+a contradiction. So \(W=\ker\phi\) for a unique \(\phi\) with \(\phi(E)=1\),
+and \(\phi(F)=0\). Every query in \(W\) belongs to \(S\), else adding it would
+keep \(E\) outside. Thus \(S=Z_\phi\), and \(\phi\) is the only functional
+with \(\phi(E)=1\) vanishing on \(F\) and \(Z_\phi\). Conversely, if \(\phi\) is
+so determined, \(\operatorname{span}(F,Z_\phi)=\ker\phi\) and \(Z_\phi\) is a
+maximal source. Distinct \(\phi\) give distinct sets.
+
+Now
+\(\phi(g)=\gamma\), \(\phi(d)=1\), \(\phi(t)=1+\gamma\),
+\(\phi(v_j)=\nu_j\), \(\phi(x_j)=1+\gamma-\nu_j\), \(\phi(y_j)=\gamma-\nu_j\).
+The vanishing conditions must determine the \(h+1\) unknowns
+\(\gamma,\nu_j\). A hub condition is one of \(\nu_j=0\), \(\nu_j=1+\gamma\),
+\(\nu_j=\gamma\). If \(\gamma\notin\{0,-1\}\), neither \(g\) nor \(t\)
+vanishes and these three are pairwise incompatible. At most one condition
+holds per hub, so at most \(h\) conditions bound \(h+1\) unknowns and
+\(\phi\) is not determined. If \(\gamma=0\), \(g\) vanishes and hub \(j\)
+vanishes on \(\{v_j,y_j\}\) (\(\nu_j=0\)) or \(\{x_j\}\) (\(\nu_j=1\)), and on
+nothing otherwise, leaving \(\nu_j\) free. If \(\gamma=-1\), \(t\) vanishes and
+the hub options are \(\{v_j,x_j\}\) (\(\nu_j=0\)) or \(\{y_j\}\)
+(\(\nu_j=-1\)). Each hub must choose an option, which gives \(2\cdot2^h\)
+sets. \(\square\)
+
+## Costs
+
+**Lemma 5 (cost one outside A–C).** Every \(E\)-reader outside families A–C
+and every \(E\)-source costs exactly 1.
+
+*Proof.* For a minimal reader \(S\), the only spanning support inside \(S\) is
+\(S\). A paid set \(P\subseteq S\) is admissible exactly when some \(\phi\)
+with \(\phi(E)=1\), \(\phi(F)=0\) vanishes on \(S\setminus P\). So the cost is
+the least number of queries of \(S\) on which such a \(\phi\) is nonzero.
+It is at least 1 because \(\sum\lambda_q\phi(q)=\phi(E)=1\).
+
+Take \(\gamma=0\) if \(g\in S\) and \(\gamma=-1\) otherwise, with every
+\(\nu_j=0\). The six non-family reduced circuits of Lemma 3 are
+\(\{g,w_a\},\{d,t,w_a\},\{g,d,w_b\},\{t,w_b\},\{t,w_a,w_c\},\{g,w_b,w_c\}\). With
+\(\nu_j=0\), the hub values are \((v,x,y)=(0,1+\gamma,\gamma)\). For
+\(\gamma=0\), pair \(a\) shows one nonzero, \(b\) none and \(c\) one. For
+\(\gamma=-1\), pair \(a\) shows none, \(b\) one and \(c\) one. The core values are
+\(g=\gamma,\ d=1,\ t=1+\gamma\). Exactly one value is nonzero in each case:
+\(x_j\) in \(\{g,w_a\}\), \(d\) in \(\{d,t,w_a\}\) and \(\{g,d,w_b\}\),
+\(y_j\) in \(\{t,w_b\}\), and the \(w_c\) hub in the two three-element sets.
+
+For a source \(S=Z_\phi\), \(\operatorname{span}(F,S)=\ker\phi\). An evaluator
+vanishing on \(F\) and \(S\) with value 1 at \(E\) must equal \(\phi\). So the
+cost is the least number of nonzero \(\phi\)-values on a minimal reader. For
+\(\gamma=0\), take the reader \((g,v_0,x_0)\): \(\phi(g)=0\) and exactly one of
+\(\phi(v_0)=\nu_0\), \(\phi(x_0)=1-\nu_0\) is nonzero when \(\nu_0\in\{0,1\}\).
+For \(\gamma=-1\), take \((t,v_0,y_0)\): \(\phi(t)=0\) and exactly one of
+\(\nu_0\), \(-1-\nu_0\) is nonzero when \(\nu_0\in\{0,-1\}\). \(\square\)
+
+*Proof of the theorem.* Parts 1–3 are Proposition 1, Lemma 4 and the
+symmetry. Families A–C are the reduced circuits \(\{d,w_c\}\), \(\{g,t,w_c\}\)
+and \(\{d,w_a,w_b\}\). Their \(h+h+h(h-1)=h(h+1)\) masks per mark cost exactly 2
+by PR4145, and every other row costs 1 by Lemma 5 and \(\sigma\). The summed
+cost is the row count plus \(2h(h+1)\). Doubling gives the charge and the
+excess \(4h(h+1)\). \(\square\)
+
+## What the program checks
+
+`verify.py` checks Lemma 3 by enumeration, the three Lemma 2 systems, the
+per-hub source cases of Lemma 4, and every Lemma 5 witness on the closed-form
+table for \(h\le 12\). As an independent control it enumerates every query
+subset of the \(h\)-hub star for \(h\le 4\) (opt-in \(h=5\)), compares the
+census with the closed-form table, and recomputes each row cost by exhaustive
+paid-set search. `test_controls.py` checks that three mutations are rejected
+and that the cost-two readers at \(h=2\) are exactly families A–C.
+
+The proof covers every \(h\); the census is not part of it.

research/p112-hub-excess-all-h/README.md

@@ -0,0 +1,116 @@
+# Hub excess 4h(h+1) for every hub count
+
+Scoped answer to Open next question 1 of unpaidmoon's
+[PR4145](https://github.com/CrocSwap/integer-mult-bounds/pull/4145)
+(`research/p112-third-hub-extremal`): does the extremal actual-reader excess
+stay equal to \(4h(h+1)\) for every hub count, not only through three hubs?
+
+**Result (scoped proof, every \(h \ge 1\)).** Yes. In the unchanged relaxed
+literal actual-reader model on the \(h\)-hub star, over any field of
+characteristic zero, the complete extremal table has
+\(2\bigl(3h(h+1)+2^{h+1}\bigr)\) rows, the minimum charge is
+
+\[
+16h(h+1)+2^{h+3},
+\]
+
+and the excess over the one-unit baseline is exactly \(4h(h+1)\). The charges
+are 48, 128, 256, 448 and 736 for \(h=1,\ldots,5\). No new \(\kappa\); the
+selected record is unchanged.
+
+PR4145 proved the lower bound for every \(h\) and equality for \(h\le3\) by
+subset census. The new step here is the extremal table and the matching upper
+bound for every \(h\):
+
+- **Readers.** Eliminating each hub coordinate \(V_j\) reduces every minimal
+  reader to a circuit through \(E\) in one fixed seven-vector configuration
+  \(\{E,\,G,\,E+F,\,E+F+G,\,E+G,\,F+G,\,E-F\}\) of a three-dimensional space,
+  with distinct hubs assigned to the last three vectors. That configuration
+  has exactly nine such circuits, so the readers are the PR4145 list for every
+  \(h\): \(3h(h+1)\) per mark.
+- **Sources.** Every maximal source is the zero set of a functional \(\phi\) with
+  \(\phi(E)=1\), \(\phi(F)=0\) and \(\phi(G)\in\{0,-1\}\); each hub then picks
+  one of two bundles. That gives \(2^{h+1}\) per mark.
+- **Costs.** Outside PR4145's families A–C, the evaluator with
+  \(\phi(G)=0\) if \(g\) is present (else \(-1\)) and every \(\phi(V_j)=0\) leaves
+  exactly one query nonzero. Every source has a one-hub reader of cost 1.
+
+[PROOF.md](PROOF.md) gives the argument.
+
+## Evidence
+
+`verify.py` checks the finite core of the proof exactly over \(\mathbb Q\):
+the nine reduced circuits (all 63 subsets), the excluded three-query hub, the
+per-hub source cases, and every cost-one witness on the closed-form table for
+\(h\le12\). As a control it enumerates every query subset of the \(h\)-hub star
+for \(h\le4\), compares the census with the closed-form table, and recomputes
+every row cost by exhaustive paid-set search. A second registered command runs
+the same census at \(h=5\) (\(2^{18}\) subsets). `test_controls.py` rejects
+three mutations (a moved \(t\), a dropped circuit, a family-C row treated as
+cost one) and confirms that the cost-two readers at \(h=2\) are exactly
+families A–C.
+
+The census is a check, not the proof. The proof covers every \(h\).
+
+## Reproduction
+
+From the repository root:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/p112-hub-excess-all-h
+```
+
+Direct checks:
+
+```sh
+python3.12 -B research/p112-hub-excess-all-h/verify.py
+python3.12 -B research/p112-hub-excess-all-h/verify.py --hmax 5 --closed-form-hmax 3
+python3.12 -B research/p112-hub-excess-all-h/test_controls.py
+```
+
+Expected tokens: `PASS_HUB_EXCESS_ALL_H` (twice) and
+`PASS_HUB_EXCESS_ALL_H_CONTROLS`. Local times on CPython 3.12: about 9 s,
+40 s and under 1 s. Not run: Lean, Docker, any selected cold replay.
+
+## Scope
+
+Task `uniform-transfer-audit`, scope **changed**, as in PR4145. The card asks
+for one caller-bound all-size implication. This package instead completes an
+open question from a merged package on the same card: the all-\(h\) shape of
+one finite row model. It is a side result, not a supplier or caller
+implication.
+
+What it does not establish: a characteristic-two statement (PR4145's
+question 2), a physical tariff, any supplier invoice, or a change in
+\(\kappa\). The cost-two lower bound for families A–C is cited from PR4145, not
+reproved; `verify.py` and the controls only recompute those costs at
+\(h\le5\). The 21-premise \(K_{3,2}\) certificate of PR3583/PR3698 is not
+revisited.
+
+Base `19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8.
+
+## Credit
+
+The extremal table through three hubs, families A–C and the lower bound
+\(4h(h+1)\) are unpaidmoon's PR4145. The one-hub star is Nick Petalas's PR3573,
+the second hub and its certificate PR3583, and the relaxed row model PR3698;
+that chain retains Philippe Van Velzen's expanded identity, ctoth's coverage
+question and the actual-reader lineage. The all-\(h\) reduction, source
+classification, cost-one witnesses and closed-form charge are produced by
+Nick Petalas.
+
+## Open next questions
+
+1. **Characteristic two.** Over GF(2) the vector \(E-F\) equals \(E+F=d\), so
+   the reduced configuration changes and the nine circuits need not persist.
+   Does the extremal table, and the excess, change in characteristic two? The
+   first step is to rerun Lemma 3's 63-subset check over GF(2) and GF(4). This
+   is related to PR4145's question 2 but asks about the whole table.
+2. **Other star shapes.** The reduction applies to any star whose hub queries
+   are \(V_j\) and two fixed core vectors minus \(V_j\). For which core triples
+   and hub vectors does the excess stay quadratic in \(h\)? The first step is to
+   parametrize the seven reduced vectors and enumerate their circuits through
+   \(E\). No caller currently uses such a change.
+3. **Charge-transfer meaning.** The row model is a relaxation. Whether the
+   quadratic excess transfers to a physical actual-reader tariff is still the
+   open link PR4145 names. That needs a caller, not more census.

research/p112-hub-excess-all-h/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/p112-third-hub-extremal/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "1e62423c1afe61e488d6ddb7f6eb77744f6e83d0",
+      "sha256": "bdff6cb8051cf8386991f26eb668b6857c54a934121b74ce1f6838d26d2ae086"
+    },
+    {
+      "path": "research/p112-third-hub-extremal/README.md",
+      "usage": "provenance",
+      "git_blob": "26825e24b01cfdbc1fe8b6f455b0d15a9ca9d524",
+      "sha256": "e40f43fd4450e6347f1ab1f308fbc880532cd96e14b70a58b38b04144dc19e9a"
+    }
+  ]
+}