diff --git a/research/p112-single-hub-two-bearing/PROOF.md b/research/p112-single-hub-two-bearing/PROOF.md new file mode 100644 index 0000000000..d01a1617f9 --- /dev/null +++ b/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. diff --git a/research/p112-single-hub-two-bearing/README.md b/research/p112-single-hub-two-bearing/README.md new file mode 100644 index 0000000000..46b5e31d81 --- /dev/null +++ b/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. diff --git a/research/p112-single-hub-two-bearing/SOURCES.json b/research/p112-single-hub-two-bearing/SOURCES.json new file mode 100644 index 0000000000..c4b56f47eb --- /dev/null +++ b/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." + } + ] +} diff --git a/research/p112-single-hub-two-bearing/TASK.json b/research/p112-single-hub-two-bearing/TASK.json new file mode 100644 index 0000000000..460bd6d937 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/p112-single-hub-two-bearing/VERIFY.json b/research/p112-single-hub-two-bearing/VERIFY.json new file mode 100644 index 0000000000..e72d41d40e --- /dev/null +++ b/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" + } + ] +} diff --git a/research/p112-single-hub-two-bearing/WITNESS.json b/research/p112-single-hub-two-bearing/WITNESS.json new file mode 100644 index 0000000000..71a155efa7 --- /dev/null +++ b/research/p112-single-hub-two-bearing/WITNESS.json @@ -0,0 +1,425 @@ +{ + "schema_version": 1, + "rows": [ + { + "kind": "source", + "mark": 0, + "premise": "gx", + "pool": "ghx", + "support": "ghx", + "u": [ + "-1", + "1", + "1" + ], + "phi": [ + "1", + "0", + "0", + "1" + ], + "alive": "h", + "cost": 1 + }, + { + "kind": "source", + "mark": 0, + "premise": "thx", + "pool": "dthx", + "support": "dthx", + "u": [ + "1", + "-1", + "1", + "1" + ], + "phi": [ + "1", + "0", + "-1", + "0" + ], + "alive": "d", + "cost": 1 + }, + { + "kind": "source", + "mark": 0, + "premise": "ty", + "pool": "thy", + "support": "thy", + "u": [ + "1", + "-1", + "-1" + ], + "phi": [ + "1", + "0", + "-1", + "-1" + ], + "alive": "h", + "cost": 1 + }, + { + "kind": "source", + "mark": 0, + "premise": "ghy", + "pool": "gdhy", + "support": "gdhy", + "u": [ + "1", + "1", + "-1", + "-1" + ], + "phi": [ + "1", + "0", + "0", + "0" + ], + "alive": "d", + "cost": 1 + }, + { + "kind": "reader", + "mark": 0, + "premise": "ghx", + "pool": "ghx", + "support": "ghx", + "u": [ + "-1", + "1", + "1" + ], + "phi": [ + "1", + "0", + "0", + "0" + ], + "alive": "x", + "cost": 1 + }, + { + "kind": "reader", + "mark": 0, + "premise": "dthx", + "pool": "dthx", + "support": "dthx", + "u": [ + "1", + "-1", + "1", + "1" + ], + "phi": [ + "1", + "0", + "-1", + "0" + ], + "alive": "d", + "cost": 1 + }, + { + "kind": "reader", + "mark": 0, + "premise": "gdhy", + "pool": "gdhy", + "support": "gdhy", + "u": [ + "1", + "1", + "-1", + "-1" + ], + "phi": [ + "1", + "0", + "0", + "0" + ], + "alive": "d", + "cost": 1 + }, + { + "kind": "reader", + "mark": 0, + "premise": "thy", + "pool": "thy", + "support": "thy", + "u": [ + "1", + "-1", + "-1" + ], + "phi": [ + "1", + "0", + "-1", + "0" + ], + "alive": "y", + "cost": 1 + }, + { + "kind": "reader", + "mark": 0, + "premise": "dxy", + "pool": "dxy", + "support": "dxy", + "u": [ + "1/2", + "1/2", + "-1/2" + ], + "phi": [ + "1", + "0", + "-1", + "0" + ], + "alive": "dy", + "cost": 2 + }, + { + "kind": "reader", + "mark": 0, + "premise": "gtxy", + "pool": "gtxy", + "support": "gtxy", + "u": [ + "-1/2", + "1/2", + "1/2", + "-1/2" + ], + "phi": [ + "1", + "0", + "0", + "0" + ], + "alive": "tx", + "cost": 2 + }, + { + "kind": "source", + "mark": 1, + "premise": "tx", + "pool": "thx", + "support": "thx", + "u": [ + "1", + "-1", + "-1" + ], + "phi": [ + "0", + "1", + "-1", + "-1" + ], + "alive": "h", + "cost": 1 + }, + { + "kind": "source", + "mark": 1, + "premise": "ghx", + "pool": "gdhx", + "support": "gdhx", + "u": [ + "1", + "1", + "-1", + "-1" + ], + "phi": [ + "0", + "1", + "0", + "0" + ], + "alive": "d", + "cost": 1 + }, + { + "kind": "source", + "mark": 1, + "premise": "gy", + "pool": "ghy", + "support": "ghy", + "u": [ + "-1", + "1", + "1" + ], + "phi": [ + "0", + "1", + "0", + "1" + ], + "alive": "h", + "cost": 1 + }, + { + "kind": "source", + "mark": 1, + "premise": "thy", + "pool": "dthy", + "support": "dthy", + "u": [ + "1", + "-1", + "1", + "1" + ], + "phi": [ + "0", + "1", + "-1", + "0" + ], + "alive": "d", + "cost": 1 + }, + { + "kind": "reader", + "mark": 1, + "premise": "gdhx", + "pool": "gdhx", + "support": "gdhx", + "u": [ + "1", + "1", + "-1", + "-1" + ], + "phi": [ + "0", + "1", + "0", + "0" + ], + "alive": "d", + "cost": 1 + }, + { + "kind": "reader", + "mark": 1, + "premise": "thx", + "pool": "thx", + "support": "thx", + "u": [ + "1", + "-1", + "-1" + ], + "phi": [ + "0", + "1", + "-1", + "0" + ], + "alive": "x", + "cost": 1 + }, + { + "kind": "reader", + "mark": 1, + "premise": "ghy", + "pool": "ghy", + "support": "ghy", + "u": [ + "-1", + "1", + "1" + ], + "phi": [ + "0", + "1", + "0", + "0" + ], + "alive": "y", + "cost": 1 + }, + { + "kind": "reader", + "mark": 1, + "premise": "dthy", + "pool": "dthy", + "support": "dthy", + "u": [ + "1", + "-1", + "1", + "1" + ], + "phi": [ + "0", + "1", + "-1", + "0" + ], + "alive": "d", + "cost": 1 + }, + { + "kind": "reader", + "mark": 1, + "premise": "dxy", + "pool": "dxy", + "support": "dxy", + "u": [ + "1/2", + "-1/2", + "1/2" + ], + "phi": [ + "0", + "1", + "0", + "0" + ], + "alive": "dy", + "cost": 2 + }, + { + "kind": "reader", + "mark": 1, + "premise": "gtxy", + "pool": "gtxy", + "support": "gtxy", + "u": [ + "-1/2", + "1/2", + "-1/2", + "1/2" + ], + "phi": [ + "0", + "1", + "0", + "0" + ], + "alive": "ty", + "cost": 2 + } + ], + "query_charges": [ + 0, + 20, + 4, + 8, + 6, + 10 + ], + "units": 24, + "charge": 48 +} \ No newline at end of file diff --git a/research/p112-single-hub-two-bearing/independent.py b/research/p112-single-hub-two-bearing/independent.py new file mode 100644 index 0000000000..cf81bafb2c --- /dev/null +++ b/research/p112-single-hub-two-bearing/independent.py @@ -0,0 +1,259 @@ +"""Second implementation of the single-hub row minimum. + +No import from verify.py. Span tests use maximal minors. Linear systems use +Cramer's rule on one nonzero maximal minor, with free variables set to zero. +GF4 is the integer field {0,1,2,3}, not the bit-pair encoding. +""" + +import json +from fractions import Fraction +from itertools import combinations +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +ZERO = Fraction(0) +NAMES = "gdthxy" +QUERIES = [ + (0, 0, 1, 0), + (1, 1, 0, 0), + (1, 1, 1, 0), + (0, 0, 0, 1), + (1, 0, 1, -1), + (0, 1, 1, -1), +] +QUERIES = [tuple(Fraction(a) for a in row) for row in QUERIES] +MARKS = [(Fraction(1), ZERO, ZERO, ZERO), (ZERO, Fraction(1), ZERO, ZERO)] +INDEX = {name: i for i, name in enumerate(NAMES)} +READERS = { + 0: ["ghx", "dthx", "gdhy", "thy", "dxy", "gtxy"], + 1: ["gdhx", "thx", "ghy", "dthy", "dxy", "gtxy"], +} +SOURCES = {0: ["gx", "thx", "ty", "ghy"], 1: ["tx", "ghx", "gy", "thy"]} +FORCED = {("reader", 0, "dxy"), ("reader", 0, "gtxy"), ("reader", 1, "dxy"), ("reader", 1, "gtxy")} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def det(matrix): + size = len(matrix) + if size == 1: + return matrix[0][0] + total = ZERO + for column in range(size): + minor = [ + [matrix[row][other] for other in range(size) if other != column] + for row in range(1, size) + ] + sign = Fraction(1) if column % 2 == 0 else Fraction(-1) + total += sign * matrix[0][column] * det(minor) + return total + + +def rank(columns): + count = len(columns) + for size in range(min(4, count), 0, -1): + for chosen_columns in combinations(range(count), size): + for chosen_rows in combinations(range(4), size): + matrix = [ + [columns[column][row] for column in chosen_columns] + for row in chosen_rows + ] + if det(matrix) != 0: + return size + return 0 + + +def contained(columns, target): + return rank(columns) == rank(list(columns) + [tuple(target)]) + + +def dot(left, right): + return sum(a * b for a, b in zip(left, right)) + + +def solve(equations, targets, variables): + """One particular solution, or None when inconsistent.""" + count = len(equations) + chosen = None + for size in range(min(variables, count), -1, -1): + found = False + row_sets = list(combinations(range(count), size)) if size else [()] + column_sets = list(combinations(range(variables), size)) if size else [()] + for rows in row_sets: + for columns in column_sets: + minor = [[equations[row][column] for column in columns] for row in rows] + if size == 0 or det(minor) != 0: + chosen = (rows, columns) + found = True + break + if found: + break + if found: + break + rows, columns = chosen + square = [[equations[row][column] for column in columns] for row in rows] + rhs = [targets[row] for row in rows] + pivot = [] + if rows: + base = det(square) + for column_index in range(len(columns)): + replaced = [list(row) for row in square] + for row_index in range(len(rows)): + replaced[row_index][column_index] = rhs[row_index] + pivot.append(det(replaced) / base) + solution = [ZERO] * variables + for value, column in zip(pivot, columns): + solution[column] = value + if any(dot(equation, solution) != target for equation, target in zip(equations, targets)): + return None + return solution + + +def coefficients(support, mark): + equations = [[QUERIES[i][coordinate] for i in support] for coordinate in range(4)] + return solve(equations, list(MARKS[mark]), len(support)) + + +def evaluator(mark, killed): + equations = [list(MARKS[mark]), list(MARKS[1 - mark])] + targets = [Fraction(1), ZERO] + for index in killed: + equations.append(list(QUERIES[index])) + targets.append(ZERO) + return solve(equations, targets, 4) + + +def minimum(kind, mark, spec): + pools = [spec] if kind == "reader" else READERS[mark] + extra = () if kind == "reader" else tuple(INDEX[name] for name in spec) + best = None + for pool in pools: + indices = [INDEX[name] for name in pool] + for size in range(1, len(indices) + 1): + for pick in combinations(indices, size): + solution = coefficients(pick, mark) + if solution is None: + continue + support = tuple(i for i, coeff in zip(pick, solution) if coeff != 0) + for killed_count in range(len(support), -1, -1): + hit = False + for extra_killed in combinations(support, killed_count): + phi = evaluator(mark, tuple(sorted(set(extra) | set(extra_killed)))) + if phi is None: + continue + cost = sum(1 for i in support if dot(phi, QUERIES[i]) != 0) + best = cost if best is None else min(best, cost) + hit = True + break + if hit: + break + require(best is not None, "missing row") + return best + + +def pairing_holds(): + samples = (ZERO, Fraction(1), Fraction(-1)) + specs = ((0, "dxy"), (1, "dxy"), (0, "gtxy"), (1, "gtxy")) + for mark, spec in specs: + support = [INDEX[name] for name in spec] + require(coefficients(support, mark) is not None, spec) + for dropped in combinations(support, len(support) - 1): + require(coefficients(dropped, mark) is None, "proper subset of " + spec) + for alpha in samples: + for beta in samples: + phi = (Fraction(1), ZERO, alpha, beta) if mark == 0 else (ZERO, Fraction(1), alpha, beta) + values = [dot(phi, QUERIES[i]) for i in support] + gap = 1 if mark == 0 else -1 + if spec == "dxy": + require(values[0] == 1 and values[1] - values[2] == gap, spec) + else: + require(values[1] - values[0] == 1 and values[2] - values[3] == gap, spec) + require(sum(value != 0 for value in values) >= 2, spec) + + +def gf4_ok(): + mul = [ + [0, 0, 0, 0], + [0, 1, 2, 3], + [0, 2, 3, 1], + [0, 3, 1, 2], + ] + + def add(left, right): + return [a ^ b for a, b in zip(left, right)] + + def scale(scalar, vector): + return [mul[scalar][entry] for entry in vector] + + e, f, g, h = [1, 0, 0, 0], [0, 1, 0, 0], [0, 0, 1, 0], [0, 0, 0, 1] + images = [ + g, + add(add(e, f), scale(2, add(g, h))), + add(add(add(e, f), g), scale(2, h)), + h, + add(add(e, g), h), + add(add(f, g), h), + ] + marks = (e, f) + + def inside(columns, target): + rows = [[columns[col][row] for col in range(len(columns))] + [target[row]] for row in range(4)] + pivot = 0 + for col in range(len(columns)): + chosen = next((i for i in range(pivot, 4) if rows[i][col] != 0), None) + if chosen is None: + continue + rows[pivot], rows[chosen] = rows[chosen], rows[pivot] + inverse = next(cand for cand in range(1, 4) if mul[rows[pivot][col]][cand] == 1) + rows[pivot] = [mul[inverse][entry] for entry in rows[pivot]] + for i in range(4): + if i != pivot and rows[i][col] != 0: + factor = rows[i][col] + rows[i] = [a ^ mul[factor][b] for a, b in zip(rows[i], rows[pivot])] + pivot += 1 + return all(row[-1] == 0 for row in rows if all(entry == 0 for entry in row[:-1])) + + for mask in range(64): + chosen = [i for i in range(6) if mask >> i & 1] + for mark in (0, 1): + old_reader = contained([QUERIES[i] for i in chosen], MARKS[mark]) + old_outside = not contained([MARKS[1 - mark]] + [QUERIES[i] for i in chosen], MARKS[mark]) + new = [images[i] for i in chosen] + if old_reader and not inside(new, marks[mark]): + return False + if old_outside and inside([marks[1 - mark]] + new, marks[mark]): + return False + return True + + +def check_witness(payload): + require(len(payload["rows"]) == 20, "row count") + for record in payload["rows"]: + mark = record["mark"] + support = [INDEX[name] for name in record["support"]] + coeffs = [Fraction(value) for value in record["u"]] + phi = [Fraction(value) for value in record["phi"]] + total = [ZERO] * 4 + for coeff, index in zip(coeffs, support): + total = [a + coeff * b for a, b in zip(total, QUERIES[index])] + require(tuple(total) == MARKS[mark], record["premise"]) + require(dot(phi, MARKS[mark]) == 1 and dot(phi, MARKS[1 - mark]) == 0, "phi") + lower = 2 if (record["kind"], mark, record["premise"]) in FORCED else 1 + require(record["cost"] == lower, "stored cost") + require(minimum(record["kind"], mark, record["premise"]) == record["cost"], "searched cost") + require(payload["query_charges"] == [0, 20, 4, 8, 6, 10], "charges") + require(sum(payload["query_charges"]) == 48, "total") + + +def main(): + require(gf4_ok(), "GF4 transfer") + pairing_holds() + check_witness(json.loads((ROOT / "WITNESS.json").read_text(encoding="utf-8"))) + print("PASS_SINGLE_HUB_TWO_BEARING_INDEPENDENT") + + +if __name__ == "__main__": + main() diff --git a/research/p112-single-hub-two-bearing/test_controls.py b/research/p112-single-hub-two-bearing/test_controls.py new file mode 100644 index 0000000000..2b18da9e23 --- /dev/null +++ b/research/p112-single-hub-two-bearing/test_controls.py @@ -0,0 +1,50 @@ +"""Rejecting controls for the single-hub charge audit.""" + +import importlib.util +from pathlib import Path + +ROOT = Path(__file__).resolve().parent + + +def load_verify(): + spec = importlib.util.spec_from_file_location("single_hub_verify", ROOT / "verify.py") + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def expect_error(function): + try: + function() + except ValueError: + return + raise SystemExit("control failed to reject") + + +def main(): + verify = load_verify() + result = verify.audit() + if result["charge"] != 48 or result["excess"] != 8: + raise SystemExit("audit totals moved") + + witness = verify.json.loads((ROOT / "WITNESS.json").read_text(encoding="utf-8")) + broken = verify.json.loads(verify.json.dumps(witness)) + row = next(item for item in broken["rows"] if item["kind"] == "reader" and item["premise"] == "dxy" and item["mark"] == 0) + row["u"] = ["1", "0", "0"] + row["alive"] = "d" + row["cost"] = 1 + expect_error(lambda: verify.check_record(row)) + + expect_error(lambda: verify.gf4_transfer(replace_y=[(1, 0), (0, 0), (0, 0), (0, 0)])) + + # The coordinate count on dthx is three, and the relaxed minimum is one. + if verify.bearing_count(0, "dthx") != 3: + raise SystemExit("strict count") + relaxed = next(item for item in witness["rows"] if item["premise"] == "dthx" and item["mark"] == 0) + if relaxed["cost"] != 1: + raise SystemExit("relaxed dthx") + print("PASS_SINGLE_HUB_TWO_BEARING_CONTROLS") + + +if __name__ == "__main__": + main() diff --git a/research/p112-single-hub-two-bearing/verify.py b/research/p112-single-hub-two-bearing/verify.py new file mode 100644 index 0000000000..6b1942b906 --- /dev/null +++ b/research/p112-single-hub-two-bearing/verify.py @@ -0,0 +1,418 @@ +"""Literal actual-reader minimum for the PR3573 exceptional single-hub star. + +The row model is the relaxed model of PR3698: each extremal premise is one +row, an admissible evaluator separates the row's mark from the other mark, +and a reader support lies in that row's premise (or, for a source row, in +one of the mark's minimal reader premises). Charge is twice the number of +active ports where both the reader coefficient and the evaluator are nonzero. + +This file proves the minimum by enumerating that finite model and checks the +written pairing lower bound, the GF4 hub transfer, and WITNESS.json. +""" + +import json +from fractions import Fraction +from itertools import combinations +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +ZERO = Fraction(0) +WIDTH = 4 +NAMES = "gdthxy" +RAW = { + "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), +} +QUERIES = [tuple(Fraction(a) for a in RAW[name]) for name in NAMES] +MARKS = [tuple(Fraction(a) for a in row) for row in ((1, 0, 0, 0), (0, 1, 0, 0))] +INDEX = {name: i for i, name in enumerate(NAMES)} +READERS = { + 0: ["ghx", "dthx", "gdhy", "thy", "dxy", "gtxy"], + 1: ["gdhx", "thx", "ghy", "dthy", "dxy", "gtxy"], +} +SOURCES = { + 0: ["gx", "thx", "ty", "ghy"], + 1: ["tx", "ghx", "gy", "thy"], +} +STRICT_BEARING = { + 0: {"ghx": 1, "dthx": 3, "gdhy": 1, "thy": 1, "dxy": 2, "gtxy": 2}, + 1: {"gdhx": 1, "thx": 1, "ghy": 1, "dthy": 3, "dxy": 2, "gtxy": 2}, +} +FORCED = {(0, "dxy"), (0, "gtxy"), (1, "dxy"), (1, "gtxy")} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rref(matrix, rhs): + rows = [list(row) + [rhs[i]] for i, row in enumerate(matrix)] + columns = len(matrix[0]) if matrix else 0 + pivots, rank = [], 0 + for col in range(columns): + chosen = next((i for i in range(rank, len(rows)) if rows[i][col] != 0), None) + if chosen is None: + continue + rows[rank], rows[chosen] = rows[chosen], rows[rank] + pivot = rows[rank][col] + rows[rank] = [value / pivot for value in rows[rank]] + for i in range(len(rows)): + if i != rank and rows[i][col] != 0: + factor = rows[i][col] + rows[i] = [a - factor * b for a, b in zip(rows[i], rows[rank])] + pivots.append(col) + rank += 1 + if rank == len(rows): + break + consistent = all(row[-1] == 0 for row in rows if all(value == 0 for value in row[:-1])) + if not consistent: + return None + particular = [ZERO] * columns + for i, col in enumerate(pivots): + particular[col] = rows[i][-1] + return particular + + +def in_span(vectors, target): + if not vectors: + return all(value == 0 for value in target) + matrix = [[vector[j] for vector in vectors] for j in range(WIDTH)] + return rref(matrix, list(target)) is not None + + +def dot(left, right): + return sum(a * b for a, b in zip(left, right)) + + +def ids(spec): + return [INDEX[name] for name in spec] + + +def coefficients(support, mark): + matrix = [[QUERIES[i][j] for i in support] for j in range(WIDTH)] + return rref(matrix, list(MARKS[mark])) + + +def evaluator(mark, killed): + constraints = [list(MARKS[mark]), list(MARKS[1 - mark])] + targets = [Fraction(1), ZERO] + for i in killed: + constraints.append(list(QUERIES[i])) + targets.append(ZERO) + return rref(constraints, targets) + + +def extremal_premises(): + readers, sources = {0: [], 1: []}, {0: [], 1: []} + for mark in (0, 1): + for size in range(7): + for comb in combinations(range(6), size): + vectors = [QUERIES[i] for i in comb] + if in_span(vectors, MARKS[mark]) and all( + not in_span([QUERIES[i] for i in comb if i != j], MARKS[mark]) for j in comb + ): + readers[mark].append("".join(NAMES[i] for i in comb)) + outside = not in_span([MARKS[1 - mark]] + vectors, MARKS[mark]) + if not outside: + continue + added = [j for j in range(6) if j not in comb] + if all( + in_span([MARKS[1 - mark]] + vectors + [QUERIES[j]], MARKS[mark]) + for j in added + ): + sources[mark].append("".join(NAMES[i] for i in comb)) + return readers, sources + + +def exact_supports(mark, pool): + found = {} + for size in range(1, len(pool) + 1): + for pick in combinations(ids(pool), size): + solution = coefficients(pick, mark) + if solution is None: + continue + exact = tuple(i for i, coeff in zip(pick, solution) if coeff != 0) + if exact not in found: + found[exact] = tuple(coeff for coeff in solution if coeff != 0) + return found + + +def best_row(kind, mark, spec): + pools = [spec] if kind == "reader" else READERS[mark] + extra = () if kind == "reader" else tuple(ids(spec)) + best = None + for pool in pools: + for support, coeffs in exact_supports(mark, pool).items(): + for killed_count in range(len(support), -1, -1): + for extra_killed in combinations(support, killed_count): + killed = tuple(sorted(set(extra) | set(extra_killed))) + phi = evaluator(mark, killed) + if phi is None: + continue + alive = tuple( + i for i in support if dot(phi, QUERIES[i]) != 0 + ) + record = { + "kind": kind, + "mark": mark, + "premise": spec, + "pool": pool, + "support": "".join(NAMES[i] for i in support), + "u": [str(coeff) for coeff in coeffs], + "phi": [str(value) for value in phi], + "alive": "".join(NAMES[i] for i in alive), + "cost": len(alive), + } + key = ( + record["cost"], + record["pool"], + record["support"], + tuple(record["u"]), + tuple(record["phi"]), + ) + if best is None or key < best[0]: + best = (key, record) + break + require(best is not None, "no admissible row for " + spec) + return best[1] + + +def row_order(): + rows = [] + for mark in (0, 1): + for spec in SOURCES[mark]: + rows.append(("source", mark, spec)) + for spec in READERS[mark]: + rows.append(("reader", mark, spec)) + return rows + + +def canonical_rows(): + return [best_row(kind, mark, spec) for kind, mark, spec in row_order()] + + +def bearing_count(mark, spec): + best = None + for size in range(1, len(spec) + 1): + for pick in combinations(ids(spec), size): + if coefficients(pick, mark) is None: + continue + count = sum(1 for i in pick if QUERIES[i][mark] != 0) + best = count if best is None else min(best, count) + return best + + +def phi_family(mark, alpha, beta): + if mark == 0: + return (Fraction(1), ZERO, alpha, beta) + return (ZERO, Fraction(1), alpha, beta) + + +def assert_pairing(): + """The four forced rows pay at least two for every admissible evaluator.""" + samples = (ZERO, Fraction(1), Fraction(-1), Fraction(1, 3)) + unique = { + (0, "dxy"): (Fraction(1, 2), Fraction(1, 2), Fraction(-1, 2)), + (1, "dxy"): (Fraction(1, 2), Fraction(-1, 2), Fraction(1, 2)), + (0, "gtxy"): (Fraction(-1, 2), Fraction(1, 2), Fraction(1, 2), Fraction(-1, 2)), + (1, "gtxy"): (Fraction(-1, 2), Fraction(1, 2), Fraction(-1, 2), Fraction(1, 2)), + } + for (mark, spec), coeffs in unique.items(): + support = ids(spec) + solution = coefficients(support, mark) + require(solution == list(coeffs), "unique reader changed: " + spec) + require( + all(coefficients(pick, mark) is None for pick in combinations(support, len(support) - 1)), + "a proper subset spans " + spec, + ) + for alpha in samples: + for beta in samples: + phi = phi_family(mark, alpha, beta) + values = [dot(phi, QUERIES[i]) for i in support] + if spec == "dxy": + # phi(d) = 1 and the x/y evaluations differ by 1. + require(values[0] == 1, "d is invisible") + require(values[1] - values[2] == (1 if mark == 0 else -1), "x/y gap") + else: + require(values[1] - values[0] == 1, "g/t gap") + require(values[2] - values[3] == (1 if mark == 0 else -1), "x/y gap") + require(sum(value != 0 for value in values) >= 2, "pairing cost dropped") + + +def gf4_transfer(replace_y=None): + one, w = (1, 0), (0, 1) + + def add(left, right): + return (left[0] ^ right[0], left[1] ^ right[1]) + + def mul(left, right): + a, b = left + c, d = right + return ((a & c) ^ (b & d), (a & d) ^ (b & c) ^ (b & d)) + + def scale(scalar, vector): + return [mul(scalar, entry) for entry in vector] + + def vadd(left, right): + return [add(a, b) for a, b in zip(left, right)] + + zero, e1 = (0, 0), one + e = [e1, zero, zero, zero] + f = [zero, e1, zero, zero] + g = [zero, zero, e1, zero] + h = [zero, zero, zero, e1] + images = { + "g": g, + "d": vadd(vadd(e, f), scale(w, vadd(g, h))), + "t": vadd(vadd(vadd(e, f), g), scale(w, h)), + "h": h, + "x": vadd(vadd(e, g), h), + "y": vadd(vadd(f, g), h), + } + if replace_y is not None: + images["y"] = replace_y + marks = (e, f) + + def contained(vectors, target): + if not vectors: + return all(entry == zero for entry in target) + columns = len(vectors) + rows = [[vectors[col][row] for col in range(columns)] + [target[row]] for row in range(4)] + pivot_row = 0 + for col in range(columns): + chosen = next((i for i in range(pivot_row, 4) if rows[i][col] != zero), None) + if chosen is None: + continue + rows[pivot_row], rows[chosen] = rows[chosen], rows[pivot_row] + inverse = next(cand for cand in ((1, 0), (0, 1), (1, 1)) if mul(rows[pivot_row][col], cand) == one) + rows[pivot_row] = [mul(inverse, entry) for entry in rows[pivot_row]] + for i in range(4): + if i != pivot_row and rows[i][col] != zero: + factor = rows[i][col] + rows[i] = [add(a, mul(factor, b)) for a, b in zip(rows[i], rows[pivot_row])] + pivot_row += 1 + return all(row[-1] == zero for row in rows if all(entry == zero for entry in row[:-1])) + + failures = 0 + for mask in range(64): + chosen = [i for i in range(6) if mask >> i & 1] + for mark in (0, 1): + old_reader = in_span([QUERIES[i] for i in chosen], MARKS[mark]) + old_outside = not in_span([MARKS[1 - mark]] + [QUERIES[i] for i in chosen], MARKS[mark]) + new_vectors = [images[NAMES[i]] for i in chosen] + if old_reader and not contained(new_vectors, marks[mark]): + failures += 1 + if old_outside and not (not contained([marks[1 - mark]] + new_vectors, marks[mark])): + failures += 1 + require(failures == 0, "GF4 hub transfer failed " + str(failures) + " implications") + + +def parse_phi(values): + return tuple(Fraction(value) for value in values) + + +def check_record(record): + mark = record["mark"] + support = ids(record["support"]) + coeffs = [Fraction(value) for value in record["u"]] + phi = parse_phi(record["phi"]) + require(len(coeffs) == len(support), "coefficient width") + total = [ZERO] * WIDTH + for coeff, i in zip(coeffs, support): + total = [a + coeff * b for a, b in zip(total, QUERIES[i])] + require(tuple(total) == MARKS[mark], "reader misses the mark: " + record["premise"]) + require(dot(phi, MARKS[mark]) == 1 and dot(phi, MARKS[1 - mark]) == 0, "evaluator") + if record["kind"] == "source": + for i in ids(record["premise"]): + require(dot(phi, QUERIES[i]) == 0, "source evaluator sees " + NAMES[i]) + require(set(record["support"]).issubset(set(record["pool"])), "source reader pool") + else: + require(set(record["support"]).issubset(set(record["premise"])), "reader premise") + alive = "".join(NAMES[i] for i in support if dot(phi, QUERIES[i]) != 0) + require(alive == record["alive"] and len(alive) == record["cost"], "recorded cost") + require(all(coeff != 0 for coeff in coeffs), "zero coefficient inside support") + + +def gram_and_charges(records): + ports = 2 * len(records) + a = [0] * ports + b = [0] * ports + q_values = [[ZERO] * ports for _ in range(6)] + u_values = [[ZERO] * ports for _ in range(6)] + for row, record in enumerate(records): + active = 2 * row + if record["mark"] == 0: + a[active] = 1 + else: + b[active] = 1 + phi = parse_phi(record["phi"]) + support = {name: Fraction(coeff) for name, coeff in zip(record["support"], record["u"])} + for i, name in enumerate(NAMES): + q_values[i][active] = dot(phi, QUERIES[i]) + u_values[i][active] = support.get(name, ZERO) + for left in range(ports): + for right in range(ports): + target = a[left] * a[right] + b[left] * b[right] + got = sum(u_values[i][left] * q_values[i][right] for i in range(6)) + require(got == target, "Gram mismatch") + charges = [] + for i in range(6): + count = sum( + 1 + for record in records + if NAMES[i] in record["support"] + and Fraction(dict(zip(record["support"], record["u"]))[NAMES[i]]) != 0 + and NAMES[i] in record["alive"] + ) + charges.append(2 * count) + return charges + + +def audit(): + readers, sources = extremal_premises() + require( + {mark: set(specs) for mark, specs in readers.items()} + == {mark: set(specs) for mark, specs in READERS.items()} + and {mark: set(specs) for mark, specs in sources.items()} + == {mark: set(specs) for mark, specs in SOURCES.items()}, + "extremal table drifted", + ) + for mark in (0, 1): + for spec, expected in STRICT_BEARING[mark].items(): + require(bearing_count(mark, spec) == expected, "strict bearing count") + assert_pairing() + gf4_transfer() + records = canonical_rows() + for record in records: + check_record(record) + lower = 2 if (record["mark"], record["premise"]) in FORCED and record["kind"] == "reader" else 1 + require(record["cost"] == lower, "row minimum is not the proved bound") + stored = json.loads((ROOT / "WITNESS.json").read_text(encoding="utf-8")) + require(stored["rows"] == records, "WITNESS.json is not the canonical minimum") + charges = gram_and_charges(records) + require(charges == stored["query_charges"], "charge vector") + require(sum(record["cost"] for record in records) == 24, "unit total") + require(sum(charges) == 48 and len(records) == 20, "charge or row count") + return { + "rows": 20, + "units": 24, + "baseline": 40, + "charge": 48, + "excess": 8, + "forced_reader_rows": ["E dxy", "E gtxy", "F dxy", "F gtxy"], + "query_charges": charges, + } + + +def main(): + result = audit() + print("PASS_SINGLE_HUB_TWO_BEARING", json.dumps(result, separators=(",", ":"))) + + +if __name__ == "__main__": + main()