Prove the exceptional single-hub literal charge is 48.

research/p112-single-hub-two-bearing/PROOF.md

@@ -0,0 +1,158 @@
+# The exceptional single-hub literal charge is 48
+
+## Statement
+
+Work over any field of characteristic zero. Use the exceptional single-hub
+star of PR3573, with independent `E,F,G,H`, marks `E,F`, and queries
+
+    g = G,  d = E+F,  t = E+F+G,  h = H,
+    x = E+G-H,  y = F+G-H.
+
+In coordinates `(E,F,G,H)` these are the six columns
+
+    g=(0,0,1,0), d=(1,1,0,0), t=(1,1,1,0),
+    h=(0,0,0,1), x=(1,0,1,-1), y=(0,1,1,-1).
+
+The extremal premises, rederived by enumerating all 64 subsets, are exactly
+the table in PR3573:
+
+| Mark | Minimal reader subsets | Maximal source subsets |
+| --- | --- | --- |
+| E | ghx, dthx, gdhy, thy, dxy, gtxy | gx, thx, ty, ghy |
+| F | gdhx, thx, ghy, dthy, dxy, gtxy | tx, ghx, gy, thy |
+
+A maximal source subset `S` is one for which the mark lies outside
+`span(other mark, Q_S)` and enters that span after every added query.
+A minimal reader subset is one that spans the mark and has no proper
+subset that does. Monotonicity makes these twenty rows the certificate:
+six readers and four sources for each mark.
+
+**Theorem.** In the relaxed literal actual-reader model below, every
+admissible factorization has total charge at least **48**, and the witness
+in `WITNESS.json` attains 48. The one-unit baseline is `2 * 20 = 40`, so
+the excess is exactly **8**. That excess sits on four reader rows,
+`E,F` crossed with `{dxy, gtxy}`, each of which pays two units rather than
+one. The GF4 hub-dependent transfer of PR3573 still satisfies every subset
+implication, so the excess is not an obstruction to that star transfer.
+
+## The row model
+
+This is the model minimized in PR3698, restricted to these twenty premises.
+For each premise row `p` choose an evaluator `phi_p` and a reader `u^(p)`
+with `sum_i u_i^(p) Q_i = mark(p)`, such that
+
+* `phi_p(mark(p)) = 1` and `phi_p(other mark) = 0`;
+* on a source row, `phi_p` vanishes on every query of the premise, and the
+  support of `u^(p)` lies in one of that mark's six minimal reader sets;
+* on a reader row, the support of `u^(p)` lies in that row's premise.
+
+Companions contribute a zero port, so there are 40 ports. With `a` and `b`
+the indicators of the active E and F rows,
+
+    a a^T + b b^T = sum_i u_i q_i^T,
+
+where `(q_i)_p = phi_p(Q_i)` and `(u_i)_p = u_i^(p)` on active rows. The
+charge is `2 * sum_p cost(p)`, and
+
+    cost(p) = #{ i : u_i^(p) != 0 and phi_p(Q_i) != 0 }.
+
+PR3698's coordinate functional is one admissible evaluator. The minimum
+below allows every rational evaluator with the two mark conditions. That
+is the same safe relaxation as PR3698: a lower bound in the larger model
+is a lower bound in the smaller one.
+
+## Proof
+
+**Step 1. Every row pays at least one.**
+The reader identity and the evaluator give
+
+    1 = phi_p(mark(p)) = sum_i u_i^(p) phi_p(Q_i).
+
+Some index has both factors nonzero, so `cost(p) >= 1`. Twenty rows give
+charge at least 40.
+
+**Step 2. Four reader rows pay at least two.**
+On each of these four premises the only spanning subset is the whole
+premise, and the reader coefficients are unique.
+
+For `E` on `dxy` they are `(1/2, 1/2, -1/2)`. Every admissible evaluator
+has the shape `phi = (1, 0, α, β)`, hence
+
+    phi(d) = 1,  phi(x) = 1+α-β,  phi(y) = α-β,
+
+and `phi(x) - phi(y) = 1`. The value on `d` is never zero, and `x` and `y`
+cannot vanish together. All three coefficients are nonzero, so `cost >= 2`.
+The same shape `phi = (0, 1, α, β)` on the `F` row `dxy`, whose unique
+coefficients are `(1/2, -1/2, 1/2)`, gives `phi(d) = 1` and
+`phi(y) - phi(x) = 1`.
+
+For `E` on `gtxy` the unique coefficients are
+`(-1/2, 1/2, 1/2, -1/2)` on `(g,t,x,y)`. Then
+
+    phi(t) - phi(g) = 1,  phi(x) - phi(y) = 1.
+
+Each pair contributes at least one visible query, so `cost >= 2`.
+For `F` on `gtxy` the unique coefficients are
+`(-1/2, 1/2, -1/2, 1/2)`, and the same two differences are `1` and `-1`.
+
+Thus four rows pay at least 2 and sixteen pay at least 1:
+
+    sum of costs >= 24,  charge >= 48.
+
+**Step 3. Both bounds are attained.**
+`WITNESS.json` gives one admissible `(u, phi)` per row. Its twenty costs
+are sixteen 1s and four 2s. Both programs recompute the reader identity,
+the evaluator conditions, the source vanishings, and all `40 * 40` entries
+of the Gram identity. One attaining per-query charge split, for
+`g,d,t,h,x,y`, is
+
+    [0, 20, 4, 8, 6, 10],  total 48.
+
+That split is a property of this witness. Another minimum witness can move
+charge between queries. The total cannot.
+
+**Step 4. Where the coordinate count overstates the excess.**
+If `phi` is forced to be the mark's coordinate functional, a query
+contributes exactly when its mark coordinate is nonzero. Under that
+stricter reading the minimum bearing counts on the E readers are
+
+    ghx:1, dthx:3, gdhy:1, thy:1, dxy:2, gtxy:2,
+
+and on the F readers
+
+    gdhx:1, thx:1, ghy:1, dthy:3, dxy:2, gtxy:2.
+
+The rows `dthx` and `dthy` look like cost 3. They are not. Their unique
+readers are `(1,-1,1,1)` on `(d,t,h,x)` and `(d,t,h,y)`. The evaluator
+`phi = (1,0,-1,0)` on the E row, and `phi = (0,1,-1,0)` on the F row,
+kills every query except `d`. The relaxed cost is 1. The two-bearing
+mechanism of PR3698 survives here only on `dxy` and `gtxy`.
+
+## The exceptional transfer still works
+
+Over GF4, with `w^2 + w + 1 = 0` and independent `e,f,g,h`, the PR3573
+hub map
+
+    d' = e+f+w(g+h),  t' = e+f+g+w h,
+    g' = g,  h' = h,  x' = e+g+h,  y' = f+g+h
+
+preserves all 128 oriented subset implications: a reader containment in
+the old star remains a reader containment, and a source exclusion remains
+a source exclusion. This is the point of the handoff. The `K3,2`
+certificate of PR3583 has no characteristic-two transfer, and its literal
+charge is forced from 42 up to 54. This star still has its transfer, and
+its literal charge is forced only from 40 up to 48.
+
+## What this does not establish
+
+The result is the exact minimum of one finite row model on one certificate.
+It is not a graph classification, not a charge bound for a third hub, not
+a literal tariff for the wider coverage identity, and not a physical or
+supplier cost. The per-query split above is not unique. No new kappa and
+no selected-frontier change follows. Acquisition, dirty restoration,
+frames, hosting, precision, stock, all-size admission and both supplier
+invoices are unrun.
+
+The mathematical argument is the pairing above together with the finite
+enumeration. Independent human and formal proof-kernel review are
+unclaimed.

research/p112-single-hub-two-bearing/README.md

@@ -0,0 +1,91 @@
+# Single-hub two-bearing charge
+
+Scoped answer to the open question in
+[discussion #1166, comment 19021149](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19021149):
+does the two-bearing-query mechanism from the PR3583/PR3698 literal
+actual-reader model appear in a factorization of the exceptional single-hub
+star of PR3573, where a hub-dependent transfer still works?
+
+**Result.** Yes, on exactly four of the twenty extremal rows. The relaxed
+row model has minimum charge **48** against baseline **40**. The excess of
+**8** is the four reader rows `E dxy`, `E gtxy`, `F dxy` and `F gtxy`, each
+forced to cost 2. The other sixteen rows attain cost 1. PR3573's GF4 map
+still preserves all 128 oriented subset implications, so this is not a
+transfer obstruction. No new κ. Selected κ stays `0.001672660197076918`.
+
+The coordinate-functional count is larger than this minimum: `dthx` and
+`dthy` contain three mark-bearing queries, but a non-coordinate evaluator
+sees only `d` and pays 1. The mechanism that survives the PR3698 relaxation
+is the pairing on `dxy` and `gtxy`, not every mark-bearing pair.
+
+## Evidence
+
+`PROOF.md` contains the pairing argument. `verify.py` rederives the extremal
+table from the six columns, searches the row model, checks the witness, and
+replays the GF4 map. `independent.py` does not import it: minors and Cramer's
+rule replace row reduction, and GF4 is `{0,1,2,3}`. `test_controls.py`
+rejects a broken `dxy` reader, a substituted `y` image, and the collapse of
+the strict `dthx` count onto the relaxed cost.
+
+One attaining per-query split in `WITNESS.json`, for `g,d,t,h,x,y`, is
+`[0, 20, 4, 8, 6, 10]`. The total 48 is the minimum. That split is not
+claimed to be the only one.
+
+## Reproduction
+
+From the repository root, Python 3.12:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/p112-single-hub-two-bearing
+```
+
+Direct checks:
+
+```sh
+python3 -B research/p112-single-hub-two-bearing/verify.py
+python3 -B research/p112-single-hub-two-bearing/independent.py
+python3 -B research/p112-single-hub-two-bearing/test_controls.py
+```
+
+Expected tokens: `PASS_SINGLE_HUB_TWO_BEARING`,
+`PASS_SINGLE_HUB_TWO_BEARING_INDEPENDENT`,
+`PASS_SINGLE_HUB_TWO_BEARING_CONTROLS`. Local runs finished in well under
+a second each. Not run: Lean, Docker, a selected cold replay, and hosted CI.
+
+## Scope
+
+Task `uniform-transfer-audit`, scope **changed**. The card asks for one
+all-size, compiler, precision, hosting or restoration implication. This
+session takes the explicit single-hub handoff instead of redrawing a card.
+The finite charge is the missing comparison with the two-hub excess of 12.
+It does not admit a supplier.
+
+Base `bb4bccbf42844d2801487450727c2f63e10d1d0f`, priority revision 6.
+The PR3573 and PR3698 heads are on `petalas/integer-mult-bounds` and are not
+objects of this repository, so the six columns are restated from PR3573's
+published star and rederived here. Overlap at 2026-10-20T02:23Z covered 814
+open PR bodies and 2642 discussion records. The single-hub factorization was
+still the open question in comment 19021149. PR #4113 quotes that question
+and reviews a different tensor-pairing bound.
+
+## Credit
+
+The star, the extremal table and the GF4 map are Nick Petalas's PR3573.
+The row model, the charge, and the two-bearing mechanism are Nick Petalas's
+PR3583 and PR3698. That chain retains Philippe Van Velzen's expanded
+identity, ctoth's coverage question and the actual-reader lineage. New
+enumeration and pairing by unpaidmoon, with substantial AI assistance
+(Cursor Grok). No independent human or proof-kernel review is claimed.
+
+## Open next questions
+
+1. Does one further independent hub add two-bearing rows beyond `dxy` and
+   `gtxy`, or repeat the twelve-unit `K3,2` excess? The first step is to
+   write the third hub's queries the way PR3583 added `k,z,w` and rerun this
+   row model on the new extremal table. Blocked by the absence of a
+   charge-transfer lemma: PR3591 moves support obstructions, not this charge.
+2. Can the working GF4 map be lifted to a characteristic-zero literal
+   factorization whose charge is strictly below 48? The first step is one
+   explicit portwise lift, or a proof that every lift pays at least 48.
+   Blocked by the gap between a support transfer and an evaluated Gram
+   factorization. A failed lift would not by itself raise the pair floor.

research/p112-single-hub-two-bearing/SOURCES.json

@@ -0,0 +1,32 @@
+{
+  "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"
+    }
+  ],
+  "predecessor_heads": [
+    {
+      "pr": 3573,
+      "commit": "f0cb59da21fbde87b4ca6a7480b0905d6f6fb9bc",
+      "repo": "petalas/integer-mult-bounds",
+      "role": "Exceptional single-hub star, extremal table and GF4 map. Not an object of this repository; columns are restated and rederived."
+    },
+    {
+      "pr": 3698,
+      "commit": "f8893fdfcb41a236ac085a92bca68ec6e5139cdc",
+      "repo": "petalas/integer-mult-bounds",
+      "role": "Relaxed literal actual-reader model and the two-hub minimum 54. The model is restated, not vendored."
+    }
+  ]
+}

research/p112-single-hub-two-bearing/TASK.json

@@ -0,0 +1,65 @@
+{
+  "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 charge of the PR3698 relaxed literal actual-reader model on the twenty extremal premises of the PR3573 exceptional single-hub star.",
+  "scope_change_reason": "Handoff-first, not card-first. The catalogue card asks for one all-size, compiler, precision, hosting or restoration implication. Discussion #1166 comment 19021149 asks whether the two-bearing mechanism appears in a literal factorization of the PR3573 single-hub certificate, where the exceptional transfer still works. That finite row model is the comparison with the two-hub excess of 12 proved in PR3698. The card's acceptance gate asks for an identified proposition and its downstream effect: the proposition is the charge 48, and the downstream effect is that the excess of 8 is confined to four reader rows and does not remove the GF4 star transfer.",
+  "bottleneck_link": "The actual-reader pair floor is one retained complex-side tariff. A forced excess that survives on the star which still has a transfer is a different obstruction from the K3,2 loss of 12, and it is not yet a supplier or a kappa change.",
+  "stop_rule": "Stop once the twenty-row minimum and the GF4 transfer check are proved. Do not start a third-hub census or a physical caller in this session.",
+  "evidence": "PROOF.md pairing; verify.py enumeration, Gram identity and GF4 replay; independent.py minor/Cramer replay; test_controls.py rejecting a broken dxy reader, a substituted y image, and equating the strict dthx count with the relaxed cost. WITNESS.json attains charge 48.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial AI assistance from Cursor Grok 4.7.",
+  "outcome": "completed",
+  "open_questions": [
+    {
+      "question": "Does one further independent hub add two-bearing rows beyond dxy and gtxy, or repeat the twelve-unit K3,2 excess?",
+      "why_it_matters": "The single-hub excess is 8, not 12. A third hub is the handoff's second question and decides whether the pairing is special to this star.",
+      "first_step": "Write the third hub's queries the way PR3583 added k,z,w and rerun this row model on the new extremal table.",
+      "blocked_by": "No charge-transfer lemma. PR3591 moves support obstructions, not this row charge."
+    },
+    {
+      "question": "Can PR3573's GF4 hub map lift to a characteristic-zero literal factorization with charge strictly below 48?",
+      "why_it_matters": "The star transfer still works. A cheaper evaluated lift would show that 48 is an artifact of the rational row model rather than a bill the working transfer must pay.",
+      "first_step": "Exhibit one portwise lift of map (5), or prove that every literal lift pays at least 48.",
+      "blocked_by": "A support transfer is not yet an evaluated Gram factorization. A failed lift does not raise the pair floor."
+    }
+  ]
+}

research/p112-single-hub-two-bearing/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": 60,
+      "checks": "Extremal table, pairing lower bound, canonical witness, 40-by-40 Gram identity, GF4 transfer and charge 48"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/independent.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Minor/Cramer recomputation of the twenty row minima, the pairing and the integer GF4 transfer"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/test_controls.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Rejects a broken dxy reader, a substituted y image, and equating the strict dthx bearing count with the relaxed cost"
+    }
+  ]
+}