Record the three-hub extremal actual-reader charge.

research/p112-third-hub-extremal/PROOF.md

@@ -0,0 +1,167 @@
+# The third hub adds crossed two-bearing rows
+
+## Statement
+
+Work over any field of characteristic zero. For an integer \(h \ge 1\), take
+independent marks \(E,F\) and independent internal potentials \(G,V_0,\ldots,V_{h-1}\).
+Index \(3+3h\) queries by
+
+\[
+g=G,\quad d=E+F,\quad t=E+F+G,
+\]
+\[
+v_j=V_j,\quad x_j=E+G-V_j,\quad y_j=F+G-V_j.
+\]
+
+This is the one-hub star of PR3573 when \(h=1\), and it is that star with the
+hubs \(k,z,w\) of PR3583 adjoined when \(h=2\). The third hub is \(h=3\).
+
+A subset of queries is a **minimal reader** for a mark when the mark lies in
+the span of those queries and in no proper subset. It is a **maximal source**
+when the mark lies outside the span of the other mark and those queries, but
+enters that span after every added query. The relaxed literal actual-reader
+model is the one minimized in PR3698 and again for \(h=1\) in the single-hub
+charge argument: each extremal row chooses an evaluator with value 1 on its
+mark and 0 on the other mark, and a reader supported on a minimal reader set
+of its mark (the row's own premise, if the row is itself a reader). The cost
+of a row is the number of queries where the reader coefficient and the
+evaluator are both nonzero. The charge is twice the sum of the row costs.
+Companions contribute a zero port, so the one-unit baseline is twice the
+number of rows.
+
+**Theorem.** In this model, for every \(h \ge 1\), the charge exceeds the
+one-unit baseline by at least \(4h(h+1)\). For \(h \le 3\) the excess is
+exactly that number, and the minimum charges are
+
+| hubs | rows | baseline | minimum charge | excess |
+| --- | ---: | ---: | ---: | ---: |
+| 1 | 20 | 40 | 48 | 8 |
+| 2 | 52 | 104 | 128 | 24 |
+| 3 | 104 | 208 | 256 | 48 |
+
+At three hubs there are 24 two-bearing rows, not only the four rows
+\((d,x_0,y_0)\) and \((g,t,x_0,y_0)\). Twelve of them are crossed five-query
+readers, two for each pair of hubs. The excess 48 is not the twelve-unit
+\(K_{3,2}\) excess. That twelve is the separate 21-premise certificate of
+PR3583/PR3698, whose charge this package recomputes as 54.
+
+## The two-bearing families
+
+Write \(\phi\) for an evaluator with \(\phi(E)=1\) and \(\phi(F)=0\). Then
+\(\phi(d)=1\), \(\phi(t)-\phi(g)=1\) and \(\phi(x_j)-\phi(y_j)=1\). The same
+identities with the marks exchanged cover \(F\).
+
+**Family A.** For each hub \(j\), the three queries \(d,x_j,y_j\) are linearly
+independent: the minor on coordinates \(E,F,G\) equals \(-2\). The unique
+expression of \(E\) is
+\[
+E=\tfrac12 d+\tfrac12 x_j-\tfrac12 y_j.
+\]
+Every coefficient is nonzero, so the triple is a minimal reader, and every
+admissible reader uses all three queries. Since \(\phi(d)=1\) and
+\(\phi(x_j)-\phi(y_j)=1\), at least two of the three evaluator values are
+nonzero. The cost is at least 2. The evaluator with every free coordinate 0
+kills \(y_j\) and leaves \(d\) and \(x_j\), so the cost is exactly 2. The same
+triple is a minimal \(F\)-reader of cost 2.
+
+**Family B.** For each hub \(j\), the four queries \(g,t,x_j,y_j\) are
+linearly independent on \(E,F,G,V_j\). The unique expression of \(E\) is
+\[
+E=-\tfrac12 g+\tfrac12 t+\tfrac12 x_j-\tfrac12 y_j,
+\]
+so the quadruple is a minimal reader and every reader uses all four queries.
+The two differences above force at least one visible query in \(\{g,t\}\) and
+at least one in \(\{x_j,y_j\}\). The cost is at least 2, and the same zero
+free coordinates attain 2. The quadruple is likewise an \(F\)-reader of cost 2.
+
+**Family C.** For each pair \(i<j\), both of the five-query sets
+\[
+(d,v_i,y_i,v_j,x_j)\qquad\text{and}\qquad(d,v_i,x_i,v_j,y_j)
+\]
+are minimal readers of cost exactly 2 for each mark. On the first set the
+unique expression of \(E\) is
+\[
+E=\tfrac12 d-\tfrac12 v_i-\tfrac12 y_i+\tfrac12 v_j+\tfrac12 x_j.
+\]
+The five vectors meet the coordinates \(E,F,G,V_i,V_j\) in a matrix of
+determinant \(-2\), so they are independent and no proper subset can produce this
+expression. Every reader therefore uses all five queries. An evaluator cannot
+kill \(v_i,y_i,v_j,x_j\) simultaneously: killing \(v_i\) and \(y_i\) forces the
+\(G\)-coordinate to vanish, while killing \(v_j\) and \(x_j\) forces it to be
+\(-1\). The zero free coordinates attain cost 2, with \(d\) and \(x_j\)
+visible. Exchanging the two hubs' \(x\) and \(y\) gives the second set, and
+exchanging the marks gives the \(F\) rows.
+
+These \(h(h+1)\) masks are pairwise distinct, and each contributes two rows.
+That is \(2h(h+1)\) rows of cost at least 2. Every other extremal row costs at
+least 1, so the excess charge is at least \(4h(h+1)\) for every \(h \ge 1\).
+
+## The extremal table for at most three hubs
+
+Both programs enumerate every query subset for \(h \le 3\). One reduces rows
+over the rationals. The other uses only integer cross-multiplication. They
+agree, and the extremal table is exactly the following list.
+
+Minimal \(E\)-readers:
+
+- for each hub \(j\), the six 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)\);
+- for each pair \(i<j\), the six sets
+  \((d,v_i,y_i,v_j,x_j)\), \((t,x_i,y_i,v_j,x_j)\),
+  \((d,v_i,x_i,v_j,y_j)\), \((g,x_i,y_i,v_j,y_j)\),
+  \((t,v_i,x_i,x_j,y_j)\), \((g,v_i,y_i,x_j,y_j)\).
+
+Minimal \(F\)-readers are those sets with each hub's \(x\) and \(y\) exchanged.
+Maximal \(E\)-sources are obtained by choosing an anchor and, independently
+for each hub, one of two bundles:
+
+- anchor \(g\), and for each hub either \(\{x_j\}\) or \(\{v_j,y_j\}\);
+- anchor \(t\), and for each hub either \(\{v_j,x_j\}\) or \(\{y_j\}\).
+
+Maximal \(F\)-sources are those sets with \(g\) and \(t\) exchanged. There are
+\(3h(h+1)\) readers and \(2^{h+1}\) sources on each mark. The count of rows is
+therefore \(2\bigl(3h(h+1)+2^{h+1}\bigr)\) for \(h \le 3\). This shape is a
+checked classification, not a proof for every larger \(h\).
+
+On this table the search finds cost 1 for every row outside families A–C, and
+cost 2 on every family row. The search allows every rational evaluator and
+every reader supported on the legal premise, which is the same safe relaxation
+as PR3698. Equality follows:
+
+\[
+\text{excess charge}=4h(h+1)\qquad(h\le 3).
+\]
+
+In particular the third hub has 104 rows, charge 256 and excess 48. Twenty-four
+of the rows are two-bearing. Twelve of those use two hubs at once, so the new
+hub does add two-bearing rows beyond \(dxy\) and \(gtxy\).
+
+## The twelve-unit certificate is a different list
+
+PR3698 minimizes the same row model on 21 premises of the two-hub star, not on
+every extremal subset. Those premises are the seven source exclusions and
+fourteen reader containments named in PR3583. Both programs recompute that
+restricted minimum and obtain charge 54, excess 12, with the six extra units
+of cost on
+\[
+(d,x_0,y_0),\ (d,x_1,y_1),\ (g,t,x_0,y_0)
+\]
+for each mark. The crossed five-query readers are absent from that list, which
+is why its excess is 12 rather than the full two-hub excess 24. Adding the
+third hub to the complete extremal table does not repeat that twelve.
+
+## What this does not establish
+
+The result is the exact minimum of one finite row model on the complete
+extremal table for at most three hubs, plus a lower bound of the same shape
+for every larger hub count. It is not a graph classification, not a
+charge-transfer lemma, and not a characteristic-two obstruction. PR3573's GF4
+map and PR3583's characteristic-two failure are not rerun. Nothing here is a
+physical tariff, a supplier admission, or a change in \(\kappa\). The selected
+conditional exponent stays \(0.001672660197076918\).
+
+The equality \(4h(h+1)\) is checked through \(h=3\) only. A fourth hub has
+\(2^{15}\) query subsets and is a separate computation. Acquisition, dirty
+restoration, frames, hosting, precision, stock and both supplier invoices are
+unrun.

research/p112-third-hub-extremal/README.md

@@ -0,0 +1,89 @@
+# Third-hub extremal charge
+
+Scoped answer to the second question in
+[discussion #1166, comment 19021149](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19021149):
+after the single-hub two-bearing charge, does one further hub add two-bearing
+rows beyond `dxy` and `gtxy`, or repeat the twelve-unit `K3,2` excess?
+
+**Result.** On the complete extremal table, a third hub does add crossed
+two-bearing rows, and it does not repeat the twelve-unit excess. In the relaxed
+literal actual-reader model the minimum charges are 48, 128 and 256 at one, two
+and three hubs. The excesses over the one-unit baseline are 8, 24 and 48, which
+is \(4h(h+1)\) for \(h \le 3\). The same families force excess at least
+\(4h(h+1)\) for every larger \(h\). No new \(\kappa\). Selected \(\kappa\) stays
+`0.001672660197076918`.
+
+At three hubs the table has 104 rows. Twenty-four of them cost 2. Twelve of
+those twenty-four are five-query readers that each use two hubs. The twelve-unit
+figure remains the minimum of the different 21-premise `K3,2` certificate, which
+this package recomputes as charge 54.
+
+## Evidence
+
+`PROOF.md` gives the pairing for the three families and the determinant that
+makes each crossed five-query set a minimal reader. `verify.py` enumerates the
+extremal table by rational row reduction. `independent.py` repeats that census
+with integer cross-multiplication and does not import `verify.py`.
+`test_controls.py` checks that the two ranks agree on every two-hub mask, that
+the one-hub triple is minimal of cost 2, that the full two-hub charge 128 is not
+the 21-premise charge 54, that dropping one forced third-hub row breaks the
+census, and that the two minors in `PROOF.md` equal \(-2\).
+
+## Reproduction
+
+From the repository root, Python 3.12:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/p112-third-hub-extremal
+```
+
+Direct checks:
+
+```sh
+python3.12 -B research/p112-third-hub-extremal/verify.py
+python3.12 -B research/p112-third-hub-extremal/independent.py
+python3.12 -B research/p112-third-hub-extremal/test_controls.py
+```
+
+Expected tokens: `PASS_THIRD_HUB_EXTREMAL`,
+`PASS_THIRD_HUB_EXTREMAL_INDEPENDENT`,
+`PASS_THIRD_HUB_EXTREMAL_CONTROLS`. Local runs finished in a few seconds each.
+Not run: Lean, Docker, a selected cold replay, hosted CI, and the \(h=4\) census.
+
+## Scope
+
+Task `uniform-transfer-audit`, scope **changed**. The card asks for one
+all-size, compiler, precision, hosting or restoration implication. The live
+handoff instead asks whether the two-bearing mechanism of the single-hub star
+persists after another hub is added. This package takes that second question.
+It does not reprove the one-hub minimum as its result; the charge 48 appears
+only as the \(h=1\) case of the same census.
+
+Base `bb4bccbf42844d2801487450727c2f63e10d1d0f`, priority revision 6.
+Open PR #4124 answers the first question in the same comment, the one-hub
+charge. This package does not import it. Open PR #3698 is the 21-premise
+two-hub minimum of 54, recomputed here as a control and not replaced.
+The ordered eligible-handoff list for this session is in the pull-request body.
+
+## Credit
+
+The one-hub star and its extremal table are Nick Petalas's PR3573. The second
+hub and the 21-premise certificate are Nick Petalas's PR3583. The relaxed row
+model and the charge 54 are Nick Petalas's PR3698. That chain retains Philippe
+Van Velzen's expanded identity, ctoth's coverage question and the actual-reader
+lineage. The third-hub census and the excess count are by unpaidmoon, with
+substantial AI assistance (Cursor Grok 4.7). No independent human or
+proof-kernel review is claimed.
+
+## Open next questions
+
+1. Does the excess stay equal to \(4h(h+1)\) for every hub count, rather than
+   only through three hubs? The inequality is already proved for every \(h\).
+   Equality needs the extremal table. The first step is the same subset census
+   at \(h=4\), where there are \(2^{15}\) query masks. Nothing mathematical
+   blocks that pass; this session stops at the third hub named in the handoff.
+2. Does any three-hub extremal row survive a characteristic-two support
+   transfer? The first step is to test PR3573's GF4 shape on one crossed
+   five-query reader. It is blocked as a charge statement because PR3591 moves
+   support obstructions, not this row cost, and a failed transfer would not by
+   itself raise the pair floor.

research/p112-third-hub-extremal/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ]
+}

research/p112-third-hub-extremal/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 6,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "docs/audit.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the selected review scope and choose one exact all-size or precision implication.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "Choose one tape, precision, hosting or restoration lemma."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact minimum of the relaxed literal actual-reader model on the complete extremal table of the PR3573 star with one, two and three independent hubs, including the crossed five-query rows that appear once a second hub exists.",
+  "scope_change_reason": "Handoff-first, and a refinement of that handoff rather than the handoff's first question. The catalogue card asks for one all-size, compiler, precision, hosting or restoration implication. Discussion #1166 comment 19021149 asks two questions: whether the two-bearing mechanism appears in the PR3573 single-hub certificate, and whether a further hub repeats the twelve-unit K3,2 excess. Open PR #4124 takes the first question. This package takes the second. The card's acceptance gate asks for an identified proposition and its downstream effect: the proposition is the excess 4h(h+1), exact through three hubs, and the downstream effect is that the twelve-unit K3,2 figure is a different 21-premise certificate, not the charge of the complete extremal table.",
+  "bottleneck_link": "The actual-reader pair floor is one retained complex-side tariff. The single-hub excess of 8 does not stay fixed when hubs are added, but the larger finite excess is still not a supplier bill or a kappa change.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the three-hub extremal charge and the 21-premise control are proved. Do not run the h=4 census or a characteristic-two transfer in this session.",
+  "outcome": "completed",
+  "evidence": "PROOF.md pairing and determinant; verify.py rational census for h<=3 and the K3,2 charge 54; independent.py integer cross-multiplication census; test_controls.py rank agreement, minimality, certificate separation and a dropped-row mutation.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial AI assistance from Cursor Grok 4.7.",
+  "open_questions": [
+    {
+      "question": "Does the excess stay equal to 4h(h+1) for every hub count, rather than only through three hubs?",
+      "why_it_matters": "The inequality is proved for every h. Equality at every h would say the crossed families are the whole excess, not an accident of three hubs.",
+      "first_step": "Run the same subset census at h=4, where there are 2^15 query masks.",
+      "blocked_by": "Nothing mathematical. This session stops at the third hub named in the handoff."
+    },
+    {
+      "question": "Does any three-hub extremal row survive a characteristic-two support transfer?",
+      "why_it_matters": "PR3573 still has a GF4 transfer at one hub, and PR3583 loses characteristic-two transfer on a different two-hub premise list. A transfer here would say whether the excess 48 can meet a star that still moves.",
+      "first_step": "Test one crossed five-query reader against the shape of PR3573's GF4 map.",
+      "blocked_by": "PR3591 moves support obstructions, not this row cost. A failed transfer would not by itself raise the pair floor."
+    }
+  ]
+}

research/p112-third-hub-extremal/VERIFY.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 90,
+      "checks": "Rational census for h=1,2,3 matches the predicted extremal table, charges 48, 128 and 256, and the 21-premise K3,2 charge is 54."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/independent.py"
+      ],
+      "timeout_seconds": 90,
+      "checks": "The same census and charges, recomputed with integer cross-multiplication and no import of verify.py."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/test_controls.py"
+      ],
+      "timeout_seconds": 90,
+      "checks": "The two rank methods agree on every two-hub mask; the one-hub triple is minimal of cost 2; charge 128 is not charge 54; dropping one forced row breaks the census; the written minors equal -2."
+    }
+  ]
+}