From a74c52264aef8540d128485e5442da7493deb1bd Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 15:24:22 +0000 Subject: [PATCH] feat(research): prove hub excess 4h(h+1) for every hub count Classify the minimal readers and maximal sources of the h-hub star for every h by eliminating hub coordinates to nine reduced circuits and phi(G) in {0,-1}, and give cost-one evaluators outside families A-C. The minimum charge is 16h(h+1)+2^(h+3), answering open question 1 of PR4145. A brute-force census through h=5 is included as a control. --- research/p112-hub-excess-all-h/PROOF.md | 222 ++++++++++ research/p112-hub-excess-all-h/README.md | 116 ++++++ research/p112-hub-excess-all-h/SOURCES.json | 30 ++ research/p112-hub-excess-all-h/TASK.json | 95 +++++ research/p112-hub-excess-all-h/VERIFY.json | 40 ++ .../p112-hub-excess-all-h/test_controls.py | 56 +++ research/p112-hub-excess-all-h/verify.py | 387 ++++++++++++++++++ 7 files changed, 946 insertions(+) create mode 100644 research/p112-hub-excess-all-h/PROOF.md create mode 100644 research/p112-hub-excess-all-h/README.md create mode 100644 research/p112-hub-excess-all-h/SOURCES.json create mode 100644 research/p112-hub-excess-all-h/TASK.json create mode 100644 research/p112-hub-excess-all-h/VERIFY.json create mode 100644 research/p112-hub-excess-all-h/test_controls.py create mode 100644 research/p112-hub-excess-all-h/verify.py diff --git a/research/p112-hub-excess-all-h/PROOF.md b/research/p112-hub-excess-all-h/PROOF.md new file mode 100644 index 0000000000..ef91cc260c --- /dev/null +++ b/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. diff --git a/research/p112-hub-excess-all-h/README.md b/research/p112-hub-excess-all-h/README.md new file mode 100644 index 0000000000..13757a07ef --- /dev/null +++ b/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. diff --git a/research/p112-hub-excess-all-h/SOURCES.json b/research/p112-hub-excess-all-h/SOURCES.json new file mode 100644 index 0000000000..d60b4e19a8 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/p112-hub-excess-all-h/TASK.json b/research/p112-hub-excess-all-h/TASK.json new file mode 100644 index 0000000000..d497d61286 --- /dev/null +++ b/research/p112-hub-excess-all-h/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact extremal table and minimum charge of the relaxed literal actual-reader model on the h-hub star of PR4145, for every hub count h >= 1 over any field of characteristic zero.", + "scope_change_reason": "Open Next Question 1 of unpaidmoon's PR4145 (research/p112-third-hub-extremal), on the same uniform-transfer-audit card, asks whether the excess 4h(h+1) is exact for every h; that package proves equality only for h <= 3. This package answers that question. It is a side result about one finite row model, not a caller-bound all-size implication.", + "bottleneck_link": "Side result. The actual-reader pair floor is one retained complex-side tariff relaxation; this fixes its exact growth in the hub count. It does not change any supplier bill or kappa.", + "budget_minutes": 60, + "stop_rule": "Stop once the extremal table, the cost-one witnesses and the closed-form charge are proved for every h, with a census control through h=5. Do not attempt characteristic two.", + "outcome": "completed", + "evidence": "PROOF.md: hub-coordinate elimination to nine reduced circuits, source functionals with phi(G) in {0,-1}, explicit cost-one evaluators. verify.py checks the finite core exactly and runs a brute-force census control for h<=4 (opt-in h=5 registered separately); test_controls.py rejects three mutations.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the extremal table, and the excess, change in characteristic two, where E-F equals E+F?", + "why_it_matters": "The reduced configuration acquires a coincidence, so the nine circuits and the quadratic excess need not persist; PR4145 question 2 asks a related support-transfer question.", + "first_step": "Rerun the 63-subset reduced-circuit check over GF(2) and GF(4).", + "blocked_by": "Nothing mathematical; outside this session's scope." + }, + { + "question": "For which core triples and hub vectors does the hub excess stay quadratic in h?", + "why_it_matters": "The reduction applies to any star of this hub shape, so the growth law is a property of a seven-vector configuration.", + "first_step": "Parametrize the seven reduced vectors and enumerate circuits through E.", + "blocked_by": "No caller currently uses a changed star." + }, + { + "question": "Does the quadratic excess transfer to a physical actual-reader tariff?", + "why_it_matters": "The row model is a relaxation; the transfer is the open link PR4145 names.", + "first_step": "Pin one caller that consumes these rows.", + "blocked_by": "No such caller is bound." + } + ] +} diff --git a/research/p112-hub-excess-all-h/VERIFY.json b/research/p112-hub-excess-all-h/VERIFY.json new file mode 100644 index 0000000000..18616ac17c --- /dev/null +++ b/research/p112-hub-excess-all-h/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Nine reduced circuits through E; excluded three-query hub; per-hub source cases; every cost-one witness on the closed-form table for h<=12; brute-force census for h<=4 equals the closed-form table, with charges 48, 128, 256, 448." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--hmax", + "5", + "--closed-form-hmax", + "3" + ], + "timeout_seconds": 300, + "checks": "The same census control at h=5 (2^18 subsets): 308 rows, charge 736, excess 120." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_controls.py" + ], + "timeout_seconds": 60, + "checks": "A moved t, a dropped circuit and a family-C row treated as cost one are rejected; the h=2 cost-two E-readers are exactly families A-C." + } + ] +} diff --git a/research/p112-hub-excess-all-h/test_controls.py b/research/p112-hub-excess-all-h/test_controls.py new file mode 100644 index 0000000000..b8db1f7551 --- /dev/null +++ b/research/p112-hub-excess-all-h/test_controls.py @@ -0,0 +1,56 @@ +#!/usr/bin/env python3 +"""Failure controls: each mutation must be rejected by the checks in verify.py.""" +import verify + +PASS = "PASS_HUB_EXCESS_ALL_H_CONTROLS" + + +def rejects(action): + try: + action() + except AssertionError: + return True + return False + + +def main(): + # 1. Moving t off E+F+G changes the reduced circuits through E. + original = verify.CORE["t"] + verify.CORE["t"] = (1, 1, 2) + try: + if not rejects(verify.check_core): + raise SystemExit("control 1: mutated t accepted") + finally: + verify.CORE["t"] = original + + # 2. Dropping one circuit from the expected list breaks the h=2 census match. + saved = verify.EXPECTED_CIRCUITS + verify.EXPECTED_CIRCUITS = saved - {frozenset("tac")} + try: + if not rejects(lambda: verify.census_charge(2)): + raise SystemExit("control 2: truncated table accepted") + finally: + verify.EXPECTED_CIRCUITS = saved + + # 3. Treating a family-C reader as non-family: no cost-one evaluator exists. + saved_family = verify.FAMILY_CIRCUITS + verify.FAMILY_CIRCUITS = saved_family - {frozenset("dab")} + try: + if not rejects(lambda: verify.check_costs_closed_form(2)): + raise SystemExit("control 3: family C given cost one") + finally: + verify.FAMILY_CIRCUITS = saved_family + + # 4. Census cost of every family reader is exactly 2 at h=2 (12 rows). + names, vecs, E, F, readers, _ = verify.census(2) + by_name = dict(zip(names, vecs)) + twos = [r for r in readers[0] if verify.min_paid(by_name, (), r, E, F) == 2] + if sorted(map(verify.circuit_of, twos), key=sorted) != sorted( + [frozenset("dc")] * 2 + [frozenset("gtc")] * 2 + [frozenset("dab")] * 2, key=sorted): + raise SystemExit("control 4: cost-two readers are not exactly families A-C") + + print(PASS, "mutations_rejected=3", "h2_cost_two_E_readers=6") + + +if __name__ == "__main__": + main() diff --git a/research/p112-hub-excess-all-h/verify.py b/research/p112-hub-excess-all-h/verify.py new file mode 100644 index 0000000000..acca53350e --- /dev/null +++ b/research/p112-hub-excess-all-h/verify.py @@ -0,0 +1,387 @@ +#!/usr/bin/env python3 +"""Hub-excess equality 4h(h+1) for every hub count. + +Part 1 checks the finite core of PROOF.md: the circuits through E in the +seven-vector reduced configuration, the excluded three-query hub, the source +functional cases and every explicit cost-one evaluator. +Part 2 is a control: a brute-force subset census of the h-hub star for +h = 1..H (default H = 4), compared with the closed-form table, and its +minimum charge computed by exhaustive paid-set search. + +Exact rational arithmetic only. Usage: verify.py [--hmax H] +""" +import argparse +import itertools +from fractions import Fraction + +PASS = "PASS_HUB_EXCESS_ALL_H" + +# Reduced configuration, coordinates (E, F, G). +CORE = { + "g": (0, 0, 1), + "d": (1, 1, 0), + "t": (1, 1, 1), + "a": (1, 0, 1), # {v_j, x_j}: x_j + v_j = E + G + "b": (0, 1, 1), # {v_j, y_j}: y_j + v_j = F + G + "c": (1, -1, 0), # {x_j, y_j}: x_j - y_j = E - F +} +E3 = (1, 0, 0) +HUB_TYPES = ("a", "b", "c") +EXPECTED_CIRCUITS = { + frozenset(s) for s in ( + "ga", "dta", "gdb", "tb", "dc", "gtc", "dab", "tac", "gbc", + ) +} +FAMILY_CIRCUITS = {frozenset("dc"), frozenset("gtc"), frozenset("dab")} + + +def solve(columns, target): + """Unique coefficients expressing target in independent columns, or None. + + Returns "dependent" if the columns are linearly dependent. + """ + rows = len(target) + width = len(columns) + matrix = [[Fraction(columns[j][i]) for j in range(width)] + [Fraction(target[i])] + for i in range(rows)] + pivots = [] + r = 0 + for col in range(width + 1): + pivot = next((i for i in range(r, rows) if matrix[i][col] != 0), None) + if pivot is None: + continue + if col == width: + return None # target outside span + matrix[r], matrix[pivot] = matrix[pivot], matrix[r] + scale = matrix[r][col] + matrix[r] = [value / scale for value in matrix[r]] + for i in range(rows): + if i != r and matrix[i][col] != 0: + factor = matrix[i][col] + matrix[i] = [x - factor * y for x, y in zip(matrix[i], matrix[r])] + pivots.append(col) + r += 1 + if len(pivots) < width: + return "dependent" + return [matrix[i][width] for i in range(width)] + + +def core_circuits(): + """Independent T subset of CORE with E in span(T), all coefficients nonzero.""" + found = {} + names = sorted(CORE) + for size in range(1, len(names) + 1): + for subset in itertools.combinations(names, size): + coeffs = solve([CORE[n] for n in subset], E3) + if coeffs is None or coeffs == "dependent": + continue + if all(c != 0 for c in coeffs): + found[frozenset(subset)] = dict(zip(subset, coeffs)) + return found + + +def check_core(): + circuits = core_circuits() + if set(circuits) != EXPECTED_CIRCUITS: + raise AssertionError(f"core circuits {sorted(map(sorted, circuits))}") + for t in circuits: + if set(HUB_TYPES) <= t: + raise AssertionError("a, b and c are dependent; cannot share a circuit") + # Lemma 2: a hub using all of v, x, y contributes the plane ; + # with one core query q the representation needs lambda_x, lambda_y, + # lambda_x + lambda_y (the v coefficient) and mu all nonzero. + for q in ("g", "d", "t"): + coeffs = solve([CORE["a"], CORE["b"], CORE[q]], E3) + if coeffs is None or coeffs == "dependent": + continue + lx, ly, mu = coeffs + if lx != 0 and ly != 0 and lx + ly != 0 and mu != 0: + raise AssertionError(f"three-query hub survives with {q}") + # No core query lies in the plane , so at most one can be added. + for q in ("g", "d", "t"): + if solve([CORE["a"], CORE["b"]], CORE[q]) is not None: + raise AssertionError(f"{q} in hub plane") + single = sum(1 for t in circuits if len(t & set(HUB_TYPES)) == 1) + double = sum(1 for t in circuits if len(t & set(HUB_TYPES)) == 2) + if (single, double) != (6, 3): + raise AssertionError((single, double)) + return circuits + + +def check_sources_local(): + """phi(G) in {0,-1} and the per-hub vanishing bundles (PROOF.md Lemma 4).""" + # Hub values: phi(v)=nu, phi(x)=1+gamma-nu, phi(y)=gamma-nu. + def zeros(gamma, nu): + out = set() + if nu == 0: + out.add("v") + if 1 + gamma - nu == 0: + out.add("x") + if gamma - nu == 0: + out.add("y") + return frozenset(out) + expected = {0: {frozenset("vy"), frozenset("x")}, -1: {frozenset("vx"), frozenset("y")}} + for gamma, bundles in expected.items(): + got = {zeros(gamma, nu) for nu in (0, 1 + gamma, gamma)} + if got != bundles: + raise AssertionError((gamma, got)) + # For gamma outside {0,-1} the three hub conditions are pairwise exclusive. + for gamma in (Fraction(1), Fraction(-2), Fraction(1, 2), Fraction(-1, 3)): + for nu in (0, 1 + gamma, gamma): + if len(zeros(gamma, nu)) != 1: + raise AssertionError((gamma, nu)) + + +# ---------------------------------------------------------------- star model + + +def star(h): + dim = 3 + h + def vec(**kw): + row = [0] * dim + for key, value in kw.items(): + row[{"E": 0, "F": 1, "G": 2}[key] if key in "EFG" else 3 + int(key[1:])] = value + return tuple(row) + names = ["g", "d", "t"] + vecs = [vec(G=1), vec(E=1, F=1), vec(E=1, F=1, G=1)] + for j in range(h): + names += [f"v{j}", f"x{j}", f"y{j}"] + vecs += [vec(**{f"V{j}": 1}), vec(E=1, G=1, **{f"V{j}": -1}), + vec(F=1, G=1, **{f"V{j}": -1})] + return names, vecs, vec(E=1), vec(F=1) + + +def closed_form(h): + """E readers, F readers, E sources, F sources as frozensets of names.""" + def hub(j, kind): + return {"a": {f"v{j}", f"x{j}"}, "b": {f"v{j}", f"y{j}"}, "c": {f"x{j}", f"y{j}"}}[kind] + e_readers = set() + for circuit in EXPECTED_CIRCUITS: + core = {q for q in circuit if q in "gdt"} + kinds = sorted(circuit & set(HUB_TYPES)) + for hubs in itertools.permutations(range(h), len(kinds)): + names = set(core) + for j, kind in zip(hubs, kinds): + names |= hub(j, kind) + e_readers.add(frozenset(names)) + swap = {} + for j in range(h): + swap[f"x{j}"], swap[f"y{j}"] = f"y{j}", f"x{j}" + f_readers = {frozenset(swap.get(n, n) for n in r) for r in e_readers} + e_sources = set() + for anchor, options in (("g", ("x", "vy")), ("t", ("vx", "y"))): + for choice in itertools.product(options, repeat=h): + names = {anchor} + for j, letters in enumerate(choice): + names |= {f"{c}{j}" for c in letters} + e_sources.add(frozenset(names)) + f_sources = {frozenset(swap.get(n, n) for n in s) for s in e_sources} + return e_readers, f_readers, e_sources, f_sources + + +def phi_values(h, gamma, nus): + """Values of the functional phi(E)=1, phi(F)=0, phi(G)=gamma, phi(V_j)=nu_j.""" + out = {"g": gamma, "d": 1, "t": 1 + gamma} + for j in range(h): + nu = nus[j] + out[f"v{j}"] = nu + out[f"x{j}"] = 1 + gamma - nu + out[f"y{j}"] = gamma - nu + return out + + +def circuit_of(reader): + """Core queries plus hub kinds (a={v,x}, b={v,y}, c={x,y}) of an E-reader.""" + hubs = {} + for name in reader: + if name[0] in "vxy": + hubs.setdefault(name[1:], set()).add(name[0]) + kind = {frozenset("vx"): "a", frozenset("vy"): "b", frozenset("xy"): "c"} + return frozenset({q for q in reader if q in "gdt"} | {kind[frozenset(m)] for m in hubs.values()}) + + +def check_costs_closed_form(h): + """Every non-family row has an explicit cost-one evaluator (all h).""" + e_readers, _, e_sources, _ = closed_form(h) + family = 0 + for reader in e_readers: + if circuit_of(reader) in FAMILY_CIRCUITS: + family += 1 + continue + # PROOF.md Lemma 5: phi(G) = 0 if g is present, else -1; every nu_j = 0. + values = phi_values(h, 0 if "g" in reader else -1, [0] * h) + if sum(1 for n in reader if values[n] != 0) != 1: + raise AssertionError(f"no cost-one witness for {sorted(reader)}") + for source in e_sources: + gamma = 0 if "g" in source else -1 + nus = [] + for j in range(h): + if gamma == 0: + nus.append(1 if f"x{j}" in source else 0) + else: + nus.append(0 if f"x{j}" in source else -1) + values = phi_values(h, gamma, nus) + if any(values[n] != 0 for n in source) or values["g" if gamma == -1 else "t"] == 0: + raise AssertionError(f"source functional wrong for {sorted(source)}") + reader = {"g", "v0", "x0"} if gamma == 0 else {"t", "v0", "y0"} + if frozenset(reader) not in e_readers: + raise AssertionError("anchor reader missing") + if sum(1 for n in reader if values[n] != 0) != 1: + raise AssertionError(f"source {sorted(source)} has no cost-one reader") + if family != h * (h + 1): + raise AssertionError(f"family readers {family} != h(h+1)") + return len(e_readers), len(e_sources) + + +# ---------------------------------------------------------------- census control + + +class Basis: + """Reduced row echelon basis over Q, modified in place with undo.""" + + def __init__(self): + self.rows = [] # (pivot, row) + self.saved = [] + + def reduce(self, vec): + v = list(vec) + for pivot, row in self.rows: + if v[pivot] != 0: + f = v[pivot] + v = [a - f * b for a, b in zip(v, row)] + return v + + def insert(self, vec): + v = self.reduce(vec) + pivot = next((i for i, x in enumerate(v) if x != 0), None) + if pivot is None: + return False + s = v[pivot] + v = [Fraction(x) / s for x in v] + new_rows = [] + for p, row in self.rows: + if row[pivot] != 0: + f = row[pivot] + row = [a - f * b for a, b in zip(row, v)] + new_rows.append((p, row)) + self.saved.append(self.rows) + self.rows = new_rows + [(pivot, v)] + return True + + def undo(self): + self.rows = self.saved.pop() + + +def in_span_with(rE, rO): + """E in span(S, O) given reductions of E and O against the basis of S.""" + if not any(rE): + return True + if not any(rO): + return False + k = next(i for i, x in enumerate(rO) if x != 0) + c = Fraction(rE[k]) / rO[k] + return all(Fraction(a) == c * b for a, b in zip(rE, rO)) + + +def census(h): + names, vecs, E, F = star(h) + n = len(names) + spans = [bytearray(1 << n), bytearray(1 << n)] # mark in span(S) + outside = [bytearray(1 << n), bytearray(1 << n)] # mark not in span(S, other) + basis = Basis() + + def walk(i, mask): + if i == n: + rE, rF = basis.reduce(E), basis.reduce(F) + spans[0][mask] = not any(rE) + spans[1][mask] = not any(rF) + outside[0][mask] = not in_span_with(rE, rF) + outside[1][mask] = not in_span_with(rF, rE) + return + walk(i + 1, mask) + inserted = basis.insert(vecs[i]) + walk(i + 1, mask | (1 << i)) + if inserted: + basis.undo() + + walk(0, 0) + readers, sources = [set(), set()], [set(), set()] + for mask in range(1 << n): + members = [i for i in range(n) if mask >> i & 1] + for m in (0, 1): + if spans[m][mask] and mask and all(not spans[m][mask ^ (1 << i)] for i in members): + readers[m].add(frozenset(names[i] for i in members)) + if outside[m][mask] and all(not outside[m][mask | (1 << i)] + for i in range(n) if not mask >> i & 1): + sources[m].add(frozenset(names[i] for i in members)) + return names, vecs, E, F, readers, sources + + +def separated(vecs_by_name, killed, mark, other): + basis = Basis() + for name in killed: + basis.insert(vecs_by_name[name]) + return not in_span_with(basis.reduce(mark), basis.reduce(other)) + + +def min_paid(vecs_by_name, fixed, reader, mark, other): + reader = sorted(reader) + for size in range(0, len(reader) + 1): + for paid in itertools.combinations(reader, size): + killed = list(fixed) + [q for q in reader if q not in paid] + if separated(vecs_by_name, killed, mark, other): + return size + raise AssertionError("no admissible evaluator") + + +def census_charge(h): + names, vecs, E, F, readers, sources = census(h) + expect = closed_form(h) + if (readers[0], readers[1], sources[0], sources[1]) != expect: + raise AssertionError(f"h={h} census differs from the closed-form table") + by_name = dict(zip(names, vecs)) + total = 0 + two = 0 + for m, (mark, other) in enumerate(((E, F), (F, E))): + for reader in readers[m]: + cost = min_paid(by_name, (), reader, mark, other) + total += cost + two += cost == 2 + if cost not in (1, 2): + raise AssertionError(cost) + for source in sources[m]: + cost = min(min_paid(by_name, source, r, mark, other) for r in readers[m]) + if cost != 1: + raise AssertionError(f"h={h} source cost {cost}") + total += cost + rows = sum(map(len, readers)) + sum(map(len, sources)) + return rows, 2 * total, two + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--hmax", type=int, default=4) + parser.add_argument("--closed-form-hmax", type=int, default=12) + args = parser.parse_args() + check_core() + check_sources_local() + for h in range(1, args.closed_form_hmax + 1): + readers, sources = check_costs_closed_form(h) + if readers != 3 * h * (h + 1) or sources != 2 ** (h + 1): + raise AssertionError((h, readers, sources)) + report = [] + for h in range(1, args.hmax + 1): + rows, charge, two = census_charge(h) + if rows != 2 * (3 * h * (h + 1) + 2 ** (h + 1)): + raise AssertionError((h, rows)) + if charge != 16 * h * (h + 1) + 2 ** (h + 3) or charge - 2 * rows != 4 * h * (h + 1): + raise AssertionError((h, charge)) + if two != 2 * h * (h + 1): + raise AssertionError((h, two)) + report.append(f"h{h}:rows={rows},charge={charge},excess={charge - 2 * rows}") + print(PASS, "core_circuits=9", f"closed_form_h<={args.closed_form_hmax}", + f"census_h<={args.hmax}", *report, "no_new_kappa") + + +if __name__ == "__main__": + main()