From a32407cb713c2828e5589e7ed341c530fff4378c Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 22:26:53 +0200 Subject: [PATCH 01/22] Add P112 rank-57 fit CANDIDATE.json --- .../p112-rational-decoder-gate/CANDIDATE.json | 754 ++++++++++++++++++ 1 file changed, 754 insertions(+) create mode 100644 research/p112-rational-decoder-gate/CANDIDATE.json diff --git a/research/p112-rational-decoder-gate/CANDIDATE.json b/research/p112-rational-decoder-gate/CANDIDATE.json new file mode 100644 index 0000000000..e645ae164f --- /dev/null +++ b/research/p112-rational-decoder-gate/CANDIDATE.json @@ -0,0 +1,754 @@ +{ + "schema_version": 1, + "scientific_base": "7ef5f7150476fdf995b286b9cdbed262c631939c", + "groups": [ + [ + 55 + ], + [ + 21, + 40, + 53 + ], + [ + 74, + 102, + 106 + ], + [ + 6, + 13, + 15 + ], + [ + 35, + 77, + 86 + ], + [ + 28, + 32, + 38 + ], + [ + 72, + 87, + 104 + ], + [ + 16, + 43, + 56 + ], + [ + 76, + 84, + 109 + ], + [ + 8, + 51, + 85 + ], + [ + 92, + 93, + 96 + ], + [ + 19, + 37, + 50 + ], + [ + 61, + 73, + 111 + ], + [ + 4, + 10, + 22 + ], + [ + 24, + 57, + 101 + ], + [ + 9, + 23, + 33 + ], + [ + 39, + 62, + 110 + ], + [ + 0, + 5, + 34 + ], + [ + 67, + 68, + 88 + ], + [ + 48, + 58, + 70 + ], + [ + 71, + 89, + 107 + ], + [ + 26, + 27, + 65 + ], + [ + 66, + 91, + 97 + ], + [ + 3, + 78, + 79 + ], + [ + 80, + 81, + 83 + ], + [ + 12, + 29, + 36 + ], + [ + 49, + 63, + 108 + ], + [ + 14, + 18, + 30 + ], + [ + 42, + 59, + 90 + ], + [ + 7, + 11, + 41 + ], + [ + 64, + 82, + 95 + ], + [ + 1, + 31, + 52 + ], + [ + 75, + 103, + 105 + ], + [ + 2, + 20, + 44 + ], + [ + 47, + 94, + 99 + ], + [ + 17, + 25, + 45 + ], + [ + 46, + 98, + 100 + ], + [ + 54, + 60, + 69 + ] + ], + "disjoint_free_triad_pairs": [ + [ + 1, + 2 + ], + [ + 3, + 4 + ], + [ + 5, + 6 + ], + [ + 7, + 8 + ], + [ + 9, + 10 + ], + [ + 11, + 12 + ], + [ + 13, + 14 + ], + [ + 15, + 16 + ], + [ + 17, + 18 + ], + [ + 19, + 20 + ], + [ + 21, + 22 + ], + [ + 23, + 24 + ], + [ + 25, + 26 + ], + [ + 27, + 28 + ], + [ + 29, + 30 + ], + [ + 31, + 32 + ], + [ + 33, + 34 + ], + [ + 35, + 36 + ] + ], + "orthogonal_group_pairs": [ + [ + 0, + 2 + ], + [ + 0, + 8 + ], + [ + 0, + 10 + ], + [ + 0, + 15 + ], + [ + 0, + 16 + ], + [ + 0, + 20 + ], + [ + 0, + 27 + ], + [ + 1, + 2 + ], + [ + 3, + 4 + ], + [ + 3, + 24 + ], + [ + 5, + 6 + ], + [ + 7, + 8 + ], + [ + 8, + 22 + ], + [ + 9, + 10 + ], + [ + 11, + 12 + ], + [ + 12, + 30 + ], + [ + 13, + 14 + ], + [ + 15, + 16 + ], + [ + 17, + 18 + ], + [ + 19, + 20 + ], + [ + 21, + 22 + ], + [ + 23, + 24 + ], + [ + 25, + 26 + ], + [ + 27, + 28 + ], + [ + 29, + 30 + ], + [ + 31, + 32 + ], + [ + 33, + 34 + ], + [ + 35, + 36 + ] + ], + "clique_groups": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 33, + 35, + 37 + ], + "factor_supports": [ + [ + 21, + 74 + ], + [ + 40, + 102 + ], + [ + 53, + 106 + ], + [ + 6, + 35 + ], + [ + 13, + 77 + ], + [ + 15, + 86 + ], + [ + 28, + 72 + ], + [ + 32, + 87 + ], + [ + 38, + 104 + ], + [ + 16, + 76 + ], + [ + 43, + 84 + ], + [ + 56, + 109 + ], + [ + 8, + 92 + ], + [ + 51, + 93 + ], + [ + 85, + 96 + ], + [ + 19, + 61 + ], + [ + 37, + 73 + ], + [ + 50, + 111 + ], + [ + 4, + 24 + ], + [ + 10, + 57 + ], + [ + 22, + 101 + ], + [ + 9, + 39, + 55 + ], + [ + 23, + 62 + ], + [ + 33, + 110 + ], + [ + 0, + 67 + ], + [ + 5, + 68 + ], + [ + 34, + 88 + ], + [ + 48, + 71 + ], + [ + 58, + 89 + ], + [ + 70, + 107 + ], + [ + 26, + 66 + ], + [ + 27, + 91 + ], + [ + 65, + 97 + ], + [ + 3, + 80 + ], + [ + 78, + 81 + ], + [ + 79, + 83 + ], + [ + 12, + 49 + ], + [ + 29, + 63 + ], + [ + 36, + 108 + ], + [ + 14, + 42 + ], + [ + 18, + 59 + ], + [ + 30, + 90 + ], + [ + 7, + 64 + ], + [ + 11, + 82 + ], + [ + 41, + 95 + ], + [ + 1, + 75 + ], + [ + 31, + 103 + ], + [ + 52, + 105 + ], + [ + 2, + 47 + ], + [ + 20, + 94 + ], + [ + 44, + 99 + ], + [ + 17, + 46 + ], + [ + 25, + 98 + ], + [ + 45, + 100 + ], + [ + 54 + ], + [ + 60 + ], + [ + 69 + ] + ], + "rational_test_scalings": [ + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2", + "1", + "2" + ], + "claimed_minimum_scalar_rank": 57, + "claimed_copy_profile": { + "3": 3, + "6": 53, + "7": 1 + }, + "claimed_copy_mass": 334, + "source_payload_sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "scope": "Finite scalar mask fit and exact port-space tariff, not a native supplier or improved exponent." +} From efb197e67da570a2eef170b0c557d858facf95f3 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 22:27:13 +0200 Subject: [PATCH 02/22] Add P112 rank-57 fit README.md --- research/p112-rational-decoder-gate/README.md | 116 ++++++++++++++++++ 1 file changed, 116 insertions(+) create mode 100644 research/p112-rational-decoder-gate/README.md diff --git a/research/p112-rational-decoder-gate/README.md b/research/p112-rational-decoder-gate/README.md new file mode 100644 index 0000000000..0390229996 --- /dev/null +++ b/research/p112-rational-decoder-gate/README.md @@ -0,0 +1,116 @@ +# A changed P112 three-plane cover with exact scalar fitting rank 57 + +**Constructive finite result and cost audit; no new supplier or kappa.** For the same 112 selected labels used by PR2041, this package supplies a different cover by 37 orthonormal triads and one residual line. Its strict scalar endpoint mask has minimum fitting rank **exactly 57**, with an explicit 57-term integral fit and a matching principal-submatrix lower bound. For the fixed cover in PR2041, PR2532 identified a rank-at-least-99 obstruction; this package also supplies a matching 99-term fit. Thus the exact fixed-mask minimum changes from **99 to 57** when the cover changes. This opens more scalar sharing without reusing the invalid binary decoder target. + +This is a partial result toward a rational decoder. Charging the full port spaces gives the displayed fit the profile `3 H3 + 53 H6 + H7`, of mass **334**. Even with the proposed coverage law and all additional costs set to zero, its zero-saving moment is **32871/32704 > 1**. Rational diagonal rescaling preserves the fit but does not reduce that bill. The number 57 counts rank-one scalar terms; it is not a verified number of physical child calls. + +## Exact object and contract + +Scientific base: `7ef5f7150476fdf995b286b9cdbed262c631939c`, priority revision 5. The labels come from [selected-replay.tar.gz](../community-frontier1094-audit/selected-replay.tar.gz), member `candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json`, payload SHA256 `c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa`. Exact source pins are in [SOURCES.json](SOURCES.json). No selected record or frozen predecessor is changed. + +Write the selected labels as `q_p` in `F2^9`, indexed by ports `p=0,...,111`. They are distinct and have odd weight. [CANDIDATE.json](CANDIDATE.json) partitions the ports into singleton `G0={55}` and 37 triples `G1,...,G37`. Within each group the label Gram matrix is the identity. Set + +\[ +E_g=\operatorname{span}_{\mathbf F_2}\{q_p:p\in G_g\},\qquad E_p=E_g\ (p\in G_g). +\] + +The inherited proposed endpoint is source `E_p -> FULL`, target `0 -> E_p^perp`. Under the strict scalar mask of PR1889 and PR2532, an addition from source `q` into target `p` is free only if `E_q` is orthogonal to `E_p`. A scalar fitting matrix `K` needs a common nonzero diagonal `c` and + +\[ +K_{pq}=0\quad\text{for }p\ne q\text{ whenever }E_p\not\perp E_q. +\] + +Other off-diagonal entries are free. This condition uses the whole group space at each port, not just the two original labels. Distinct ports in the same group also have forced zero entries because that group is nondegenerate. The new cover has **420 free ordered port pairs**; the predecessor cover has 102. These counts exclude diagonal entries. + +## A complete rank-57 certificate + +For `j=1,...,18`, the groups `G_(2j-1)` and `G_(2j)` are orthogonal. For each `k=0,1,2`, form a support from the `k`th stored port in each triad of this pair, giving 54 supports. The residual line is orthogonal to both `G15` and `G16`; append port 55 to their first support, giving `{9,39,55}`. Make the three ports of `G37={54,60,69}` singleton supports. + +These 57 supports `S_t` partition all 112 ports. Each contains at most one port from any group, and its represented groups are pairwise orthogonal. With `v_t` the indicator of `S_t`, define + +\[ +K=\sum_{t=1}^{57}v_t v_t^T. +\] + +Each diagonal entry is one. Nonzero off-diagonal entries occur only within supports, where they are free. Thus this is an exact fit. One chosen port from each support gives an identity minor of size 57; the displayed factorization gives rank at most 57. + +Conversely, the 19 odd-indexed triads `G1,G3,...,G35,G37` are pairwise nonorthogonal. The verifier checks every cross-group pairing matrix is nonzero. Among their 57 ports all off-diagonal entries are forced to zero, both within and between groups. Every valid fit therefore restricts to `c I57`, forcing rank at least 57. Together the certificates prove **minimum scalar fitting rank 57 for this fixed mask**, over any field with `c != 0`. They do not prove this cover is optimal among all covers of the selected labels. + +For comparison, the old cover attains rank 99 by pairing corresponding coordinates of its orthogonal triad pairs `(6,13)`, `(7,12)`, `(9,19)`, `(22,25)`, pairing the residual port with the first port of group 1, and leaving every other port singleton. This makes 99 disjoint supports. The 33 triads excluding groups `12,13,19,25` force a principal identity of size 99. Both certificates are replayed; the old fit costs `86 H3 + H4 + 12 H6 = 334` under the same tariff. + +For any nonsingular rational diagonal matrix `S`, there is also a rational fitting family + +\[ +K_S=SKS^{-1}=\sum_t(Sv_t)(S^{-1}v_t)^T. +\] + +Its diagonal, zero pattern and rank are unchanged. The positive fixture alternates diagonal entries 1 and 2, so actual even-denominator coefficients are checked. Their presence alone supplies no 2-adic cost gain: every factor has the same support as before. + +## Full port-space charge and stopping decision + +For a rank-one term `a b^T`, use the inherited one-total tariff: span **all group spaces** touched by the nonzero coordinates of `a`, do the same for `b`, then charge the `F2` rank of their bilinear pairing. This is the port-space convention of PR2532 and the native multiplicity issue made concrete in PR2203. Scalar coefficient rank and original-label support rank do not replace this charge. + +Here both spans are equal. Each ordinary pair support touches two orthogonal nondegenerate three-spaces and costs 6. The support also containing the residual line costs 7. Each singleton still touches its complete three-space and costs 3. Hence + +\[ +n_3=3,\qquad n_6=53,\qquad n_7=1,\qquad C=3\cdot3+53\cdot6+7=334. +\] + +This remains true after any diagonal conjugation above. It prices these factors; it is not a lower bound for arbitrary rational decoders under this mask. The integral construction does not evade the earlier 2-integral floor of 334 for this 37-triad/one-line contract. + +The exact average unpaid dimension is + +\[ +u=\frac{37\cdot3\cdot3+1}{112}=\frac{167}{56}. +\] + +Using uniform `u=3` would overcredit the residual port. Grant the mixed-group coverage law, selected non-centre profile `{1:2412, 2:418, 3:432, 4:142, 5:82}` of mass 5522, width `m=73`, and `w=896/9` live families per call. Adding the displayed decoder gives profile `{1:2412, 2:418, 3:435, 4:142, 5:82, 6:53, 7:1}`. Ideal idle mass is + +\[ +I=(73-u)w-5522=\frac{4346}{3}. +\] + +Its packing does not matter at zero saving: + +\[ +M(0)=\frac{5522+C+I}{73w} +=1+\frac{C-2672/9}{65408/9} +=1+\frac{334}{65408} +=\frac{32871}{32704}>1. +\] + +Every child rank is below 73, so `(r/73)^(1-a)` is nondecreasing for `a>=0`. Failure at zero rules out positive saving for the displayed profile before extra costs. This conditional screen does not establish a native implementation of the coverage law. Its necessary centre budget for any positive saving is `C < 2672/9`, hence `C<=296` for an integer invoice. Reaching the selected saving requires a substantially smaller bill, around 261 even under favorable rank-1-through-9 packing; PR2532's incumbent-tie screen is planning context, not a feasibility certificate. + +## Discovery and replay + +Discovery optimized the actual free mask. A bounded randomized exact-cover search, seed `2026101501`, packed orthogonal six-label sets and split each into two triads, obtaining 17 disjoint orthogonal triad pairs. A local repair, seed `2026101502`, repacked 22 ports: two six-label blocks plus ten remaining ports became three six-label blocks, one triad and one line. This produced the 18-pair cover. Attaching the residual line as above gives rank 57. + +These were bounded heuristic searches, not an exhaustive optimization over covers. The finite certificate is independent of discovery order, random choices and time limits. Scientific replay uses the saved cover and witnesses, without rerunning discovery. + +From the repository root, standard library only: + +```sh +python3 -I -O -B research/p112-rational-decoder-gate/verify.py +python3 -I -O -B research/p112-rational-decoder-gate/independent_check.py +python3 scripts/research_package.py --package research/p112-rational-decoder-gate --check-only +python3.12 scripts/research_package.py --package research/p112-rational-decoder-gate +``` + +The primary and separately implemented checker reconstruct labels, the cover, the whole-space mask, rank witnesses, rational fitting entries and term charges. Commands, controls and input requirements are in [VERIFY.json](VERIFY.json); the receipt is [RESULT.json](RESULT.json). Neither checker is a native word compiler or proof-assistant kernel. Independent checks here are AI-agent checks, not independent human review. + +## Predecessors, overlap and credit + +- **Cinna Davis (`1337isnot1337`), [PR2041](https://github.com/CrocSwap/integer-mult-bounds/pull/2041):** selected P112 three-plane cover, endpoint proposal and binary factorization. That binary identity and local correction remain valid in their algebra. This package changes the cover and certifies the stricter scalar mask. +- **Adam Gall (`adamgall`), [PR1889](https://github.com/CrocSwap/integer-mult-bounds/pull/1889):** paired-plane scalar-mask obstruction. **ctoth and collaborators** and **Philippe Van Velzen (`philippeVV`)**, in [Discussion1587](https://github.com/CrocSwap/integer-mult-bounds/discussions/1587), supplied the port endpoint, masked-set count, whole-space pricing and 2-integral/Smith framework used by the later audit. +- **Sagar Thakrar (`thakrarsagar`), [PR2532](https://github.com/CrocSwap/integer-mult-bounds/pull/2532), head `bcb6f278503bd2a6b3ffb9bdcfcda9f36c18d2f4`:** exact application of that mask and pricing to PR2041, including its 102 free pairs, rank-at-least-99 obstruction and 334 floor. The changed triad cover is the new premise here; the new fit does not contradict that fixed-cover audit. +- **Cinna Davis, [PR2126](https://github.com/CrocSwap/integer-mult-bounds/pull/2126), and Jeremy Diviney (`jeremydiviney`), [PR2203](https://github.com/CrocSwap/integer-mult-bounds/pull/2203):** paired-plane scalar identity fit and native payload accounting. Their distinction between coefficient blocks, independent payloads and native occurrences is retained. +- **Sagar Thakrar, [PR2484](https://github.com/CrocSwap/integer-mult-bounds/pull/2484), head `4823273c8163e4c72472bdf7d42202e2c12d2e46`, following ywz65's PR2471:** exact scalar minimum rank 49 on a different, fixed paired-plane mask, including disjoint-support upper and submatrix lower certificates. Those proof methods are prior work. This package supplies a different three-plane cover, its exact rank and full charge; rank 57 versus 49 does not compare complete supplier costs. + +At the scientific base the central ledger marks PR1889, PR2041, PR2126 and PR2203 incorporated as scoped results, which does not admit a new supplier. PR2532 and PR2484 are pinned pending sources for context and overlap. The selected PR1094 lineage, including Rohan Arun and Jeremy Kothe, retains credit for the labels. Native frame-distance work by icekylinx and its independent check by woklerx retain their credit through the predecessors. + +Prepared by flyingviper with substantial OpenAI Codex assistance in search, proof development, implementation and separate-agent checking. No independent human review, formal verification of the full theorem, selected-result change or new exponent is claimed. New work is Apache-2.0. + +## Open next questions + +1. **Can a different rational factorization exploit this mask to lower the full port-space bill?** Start with asymmetric factors, possibly more than 57 terms and mixing different orthogonal pairs. Enforce every diagonal and forbidden entry exactly before pricing whole source and reader spaces. A useful first gate is `C < 2672/9`; a selected-bound candidate needs a full moment below one near the incumbent saving, requiring roughly `C<=261` even in the favorable rank-9 relaxation. Stop a factorization family when its favorable complete invoice misses that gate. Diagonal rescaling of the saved factors costs 334 and does not reopen it. +2. **Can a different block or native contract realize useful sharing with every independent payload charged?** First supply the complete operator identity, dirty-input behavior and actual occurrences, rather than charging a geometric rank once for a multi-array block. Before another construction round, update the family budget and consumer boundary: source preparation, chart conversion, routing, hosting, chronological ownership, storage, erasure/restoration, precision, all-size recursion and a compatible bit supplier remain unproved here. Their costs are unknown, not zero. This finite certificate supplies neither physical compilation nor the selected cold replay. From 183c9506e9d5d4d1ffb219339a4b1ea5796a218b Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 22:27:18 +0200 Subject: [PATCH 03/22] Add P112 rank-57 fit TASK.json --- research/p112-rational-decoder-gate/TASK.json | 121 ++++++++++++++++++ 1 file changed, 121 insertions(+) create mode 100644 research/p112-rational-decoder-gate/TASK.json diff --git a/research/p112-rational-decoder-gate/TASK.json b/research/p112-rational-decoder-gate/TASK.json new file mode 100644 index 0000000000..9845ce4639 --- /dev/null +++ b/research/p112-rational-decoder-gate/TASK.json @@ -0,0 +1,121 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 5, + "base_commit": "7ef5f7150476fdf995b286b9cdbed262c631939c", + "original_card": { + "id": "coverage-law-change", + "question": "Can a template or call contract leave two or more unpaid coordinates per live family?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/idle-axis-hosting/PROOF.md", + "certificates/selected-result.json" + ], + "methods": [ + "State a replacement for the coverage identity (mass = 72W + 64N) and the contract change that realizes it, with its implementation cost.", + "Find an obstruction: show which data-endpoint obligation forces exactly one unpaid coordinate in the current template." + ], + "acceptance_gate": "An explicit replacement identity, verified on a small complete instance with dirty inputs, priced with ceiling.ceiling(unpaid=...). A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Explain where the single unpaid coordinate per family comes from in the hosted template; propose one change and price it. Ideal budget: two unpaid coordinates per family is 3.77x (levers.py).", + "bottleneck_link": "The deficit is one coordinate per family minus the centre charge; doubling unpaid coordinates per family scales it directly.", + "allowed_variations": [ + "One template change or one endpoint-contract change.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Counting a coordinate as unpaid while leaving it unadvanced in the data endpoint.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "coverage identity", + "unpaid coordinate", + "deficit law", + "W - 64N" + ] + }, + "scope_status": "changed", + "actual_scope": "Construct and independently certify a changed 37-triad/one-line P112 mask with exact scalar fitting rank57, compare the old rank99 mask, and fully price the explicit scalar factors.", + "scope_change_reason": "User selected rational/block P112 decoder research after PR2532 invalidated the original binary lift. The old cover obstructs natural fractional routes; change the cover to expand actual orthogonal-group freedom instead of optimizing the invalid binary invoice.", + "bottleneck_link": "Provides a correct lower-rank scalar mask benchmark for cross-group fractional decoding. The explicit334 copy bill still fails the favorable coverage screen, so no native implementation campaign or improved bound is claimed.", + "budget_minutes": 60, + "stop_rule": "Retain one verified mask/cost result after exact endpoint and independent checks. Reject the explicit supplier target at zero saving; do not infer a universal rational-decoder or cover obstruction from bounded motif searches.", + "outcome": "partial", + "evidence": "CANDIDATE.json, exact identity-minor and disjoint-support proof in README, primary RESULT.json and independently implemented checker. Both original and new masks are certified.", + "author": "flyingviper (with OpenAI Codex)", + "ai_assistance": "Substantial OpenAI Codex assistance in algebra, search, implementation, writing and testing. Three AI agents split independent scalar checks, cost/mask research, and fractional/operator exploration. No independent human or proof-assistant review is claimed.", + "open_questions": [ + { + "question": "Can a genuinely shared fractional decoder improve the new mask's334 port-space charge?", + "why_it_matters": "The scalar rank obstacle has fallen99 to57, but break-even requires C<2672/9 and the selected-target optimistic allowance is smaller.", + "first_step": "Give explicit rational source/reader factors across distinct paired components, check every constrained coefficient, then price all full port-space support pairings before native work.", + "blocked_by": "The supplied indicator fit and its rational diagonal gauges have charge334. No favorable full bill or actual native word is supplied." + }, + { + "question": "Can a different mask or operator contract supply genuinely cheaper payload transport?", + "why_it_matters": "A scalar channel count is not a physical copy invoice; lower-rank matrices can retain the same total cost.", + "first_step": "Specify source/target frames, independent array payloads, storage and cleanup. Prove the exact arbitrary-dirty endpoint and an optimistic full budget.", + "blocked_by": "Routes, application multiplicity, ownership, precision and full supplier integration remain unproved." + } + ], + "selection": "Explicit user choice of new rational/block P112 decoder; no random task reassignment.", + "upstream_refresh": { + "checked_at_utc": "2026-10-15T19:54:00Z", + "canonical_main": "7ef5f7150476fdf995b286b9cdbed262c631939c", + "priority_revision": 5, + "decision": "Guidance and selected record unchanged; new isolated branch from canonical main.", + "final_checked_at_utc": "2026-10-15T20:19:11Z", + "final_canonical_main": "e93f2ebd9c60b79e564b07acffdbbb99b477c28c", + "final_decision": "Fast-forwarded isolated publication branch. Guidance, selected record and consumed source inputs are unchanged; scientific pins retained." + }, + "overlap": { + "checked_at_utc": "2026-10-15T20:19:11Z", + "latest_updated_open_pr_bodies": 100, + "complete_pagination": false, + "discussions": [ + 1587, + 2024, + 1166, + 1167 + ], + "nearest": "PR2532 scalar-mask audit, PR2041 triad cover, PR1889 mask semantics, PR2126/2203 payload and native accounting, PR2484 exact minrank49 for a different paired-plane mask.", + "limits": "Latest100 updated open PR bodies, relevant live discussion pages and local README/TASK search; not exhaustive remote pagination or arbitrary diffs. No public claim posted." + }, + "search": { + "initial_seed": 2026101501, + "repack_seed": 2026101502, + "method": "Pack disjoint orthogonal six-label sets and split each into two triads; complete the residual cover. Locally repack22 labels from a17-pair cover to obtain18pairs, one triad and one residual line.", + "status": "Heuristic discovery; certificate replay is exact and does not trust or rerun the heuristic search. No optimum over covers claimed." + }, + "family_gate": { + "decision": "narrow", + "proved": "Exact minimum scalar fitting rank57 for the new mask, rank99 comparison, complete334 port-space charge of the displayed factors, and failure of the favorable coverage screen already at a=0.", + "unknown": [ + "native caller", + "routes and chronological ownership", + "storage", + "dirty helper cleanup", + "precision", + "all-size admission", + "bit-side transfer" + ], + "next": "A cross-component rational/operator identity with a favorable fully charged budget; no expansion into physical construction for the supplied334-cost fit." + }, + "validation": { + "environment": "3.12.14", + "primary": "verify.py -I -O -B", + "independent": "independent_check.py -I -O -B", + "formal_kernel": false, + "human_review": false + } +} From ec515674bfb68a8848ba5786efb94b38c58ab4cf Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 22:27:27 +0200 Subject: [PATCH 04/22] Add P112 rank-57 fit SOURCES.json --- .../p112-rational-decoder-gate/SOURCES.json | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 research/p112-rational-decoder-gate/SOURCES.json diff --git a/research/p112-rational-decoder-gate/SOURCES.json b/research/p112-rational-decoder-gate/SOURCES.json new file mode 100644 index 0000000000..f36ae5f780 --- /dev/null +++ b/research/p112-rational-decoder-gate/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7ef5f7150476fdf995b286b9cdbed262c631939c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/tri-plane-port-p112-seeddb093026/CANDIDATE.json", + "usage": "input", + "git_blob": "438d5c4b1564495bbfeaca2cffa42453c455b3ad", + "sha256": "92b5f2f835e9f226bba2d936b7bf9ba9300462a9112492bcb70229eb63a84901" + } + ] +} From 243e68173c69c948cea9919250683e290d123d22 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 22:27:32 +0200 Subject: [PATCH 05/22] Add P112 rank-57 fit VERIFY.json --- .../p112-rational-decoder-gate/VERIFY.json | 34 +++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 research/p112-rational-decoder-gate/VERIFY.json diff --git a/research/p112-rational-decoder-gate/VERIFY.json b/research/p112-rational-decoder-gate/VERIFY.json new file mode 100644 index 0000000000..f094cbbe87 --- /dev/null +++ b/research/p112-rational-decoder-gate/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/tri-plane-port-p112-seeddb093026/CANDIDATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate source bytes; exact original/new mask rank certificates, rational scalar endpoint and full port-space cost; eight semantic controls; receipt equality." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 120, + "checks": "Independent source-bound reconstruction with a distinct elimination method; both exact ranks, every rational endpoint coefficient and dirty source column; nine controls." + } + ] +} From 5201704ff74fa17fdf21a71ecd999eb43e1e21a5 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 22:27:43 +0200 Subject: [PATCH 06/22] Add P112 rank-57 fit RESULT.json --- .../p112-rational-decoder-gate/RESULT.json | 93 +++++++++++++++++++ 1 file changed, 93 insertions(+) create mode 100644 research/p112-rational-decoder-gate/RESULT.json diff --git a/research/p112-rational-decoder-gate/RESULT.json b/research/p112-rational-decoder-gate/RESULT.json new file mode 100644 index 0000000000..3e6f938d21 --- /dev/null +++ b/research/p112-rational-decoder-gate/RESULT.json @@ -0,0 +1,93 @@ +{ + "candidate_sha256": "dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b", + "payload_sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "ports": 112, + "free_ordered_pairs": 420, + "scalar_minrank": 57, + "clique_ports": [ + 21, + 40, + 53, + 6, + 13, + 15, + 28, + 32, + 38, + 16, + 43, + 56, + 8, + 51, + 85, + 19, + 37, + 50, + 4, + 10, + 22, + 9, + 23, + 33, + 0, + 5, + 34, + 48, + 58, + 70, + 26, + 27, + 65, + 3, + 78, + 79, + 12, + 29, + 36, + 14, + 18, + 30, + 7, + 11, + 41, + 1, + 31, + 52, + 2, + 20, + 44, + 17, + 25, + 45, + 54, + 60, + 69 + ], + "copy_profile": { + "3": 3, + "6": 53, + "7": 1 + }, + "copy_mass": 334, + "rational_endpoint_entries": 12544, + "zero_saving_allowance": "2672/9", + "centre_excess": "334/9", + "favorable_M0": "32871/32704", + "historical_scalar_minrank": 99, + "historical_copy_profile": { + "3": 86, + "4": 1, + "6": 12 + }, + "controls": [ + "duplicate/missing port", + "orthogonal pair in clique", + "forbidden rational coefficient", + "wrong diagonal", + "missing factor", + "binary pairing as scalar endpoint", + "residual undercharge rejected", + "cross-rank-zero undercharge rejected" + ], + "scope": "finite scalar fit; no native word, supplier or exponent improvement" +} From 9f313af55834548a3183f4566023e2b5f9ccd777 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 22:28:01 +0200 Subject: [PATCH 07/22] Add P112 rank-57 fit verify.py --- research/p112-rational-decoder-gate/verify.py | 179 ++++++++++++++++++ 1 file changed, 179 insertions(+) create mode 100644 research/p112-rational-decoder-gate/verify.py diff --git a/research/p112-rational-decoder-gate/verify.py b/research/p112-rational-decoder-gate/verify.py new file mode 100644 index 0000000000..1d6e20037f --- /dev/null +++ b/research/p112-rational-decoder-gate/verify.py @@ -0,0 +1,179 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact changed-mask certificate. Standard library; no predecessor code imports.""" +import argparse +from collections import Counter +from fractions import Fraction as F +import hashlib +import io +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ARCHIVE = 'research/community-frontier1094-audit/selected-replay.tar.gz' +OLD = 'research/tri-plane-port-p112-seeddb093026/CANDIDATE.json' +MEMBER = 'candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' +MEMBER_SHA = 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa' + +def need(ok, message): + if not ok: raise ValueError(message) + +def strict_json(raw): + def unique(items): + result={} + for key,value in items: + need(key not in result,'duplicate JSON key: '+key) + result[key]=value + return result + def bad_constant(value): + raise ValueError('nonfinite JSON constant: '+value) + return json.loads(raw,object_pairs_hook=unique,parse_constant=bad_constant) + +def canonical(value): + return json.dumps(value,sort_keys=True,separators=(',',':'),allow_nan=False) + +def load(): + pins = strict_json((HERE/'SOURCES.json').read_text()) + pin = {x['path']:x for x in pins['files'] if x['usage']=='input'} + raw = {} + for path in (ARCHIVE, OLD): + data = (ROOT/path).read_bytes() + need(hashlib.sha256(data).hexdigest()==pin[path]['sha256'], 'source sha256 '+path) + need(hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest()==pin[path]['git_blob'], 'source blob '+path) + raw[path]=data + with tarfile.open(fileobj=io.BytesIO(raw[ARCHIVE]),mode='r:gz') as arc: + payload=arc.extractfile(MEMBER).read() + need(hashlib.sha256(payload).hexdigest()==MEMBER_SHA,'phase payload') + rows=sorted(json.loads(payload)['recipes'],key=lambda x:x['port']) + need([r['port'] for r in rows]==list(range(112)),'port order') + q=[r['q'] for r in rows] + need(len(set(q))==112 and all(01,'coverage screen') + # Subtract only free off-diagonal entries: exact final scalar identity. + corrected=[[b[i][j] if i==j or table[owner[i]][owner[j]] else F(0) for j in range(112)] for i in range(112)] + need(all(corrected[i][j]==int(i==j) for i in range(112) for j in range(112)),'corrected scalar identity') + old_spaces,old_owner,old_table=geometry(q,old_groups) + old_ports=clique([g for g in range(1,38) if g not in (12,13,19,25)],old_groups,old_table) + old_supports=[[i,j] for x,y in ((6,13),(7,12),(9,19),(22,25)) for i,j in zip(old_groups[x],old_groups[y])] + old_supports.append([old_groups[0][0],old_groups[1][0]]) + used={i for s in old_supports for i in s};old_supports.extend([[i] for i in range(112) if i not in used]) + need(len(old_ports)==len(old_supports)==99,'old rank certificates') + check(fit(old_supports,unit),old_owner,old_table) + old_profile=charge(old_supports,old_spaces,old_owner) + need(sum(r*n for r,n in old_profile.items())==334,'old copy mass') + controls=[] + wrong=[g[:] for g in groups];wrong[1][0]=wrong[2][0] + controls.append(rejects(lambda:geometry(q,wrong),'duplicate/missing port')) + controls.append(rejects(lambda:clique(c['clique_groups']+[2],groups,table),'orthogonal pair in clique')) + wrong=[row[:] for row in b];wrong[ports[0]][ports[1]]=F(1,2) + controls.append(rejects(lambda:check(wrong,owner,table),'forbidden rational coefficient')) + wrong_diagonal=[row[:] for row in b];wrong_diagonal[0][0]=2 + controls.append(rejects(lambda:check(wrong_diagonal,owner,table),'wrong diagonal')) + controls.append(rejects(lambda:check(fit(supports[:-1],unit),owner,table),'missing factor')) + binary=[[F(dot(q[i],q[j])) for j in range(112)] for i in range(112)] + controls.append(rejects(lambda:check(binary,owner,table),'binary pairing as scalar endpoint')) + line=next(s for s in supports if groups[0][0] in s) + need(charge([line],spaces,owner)=={7:1},'residual tariff must be seven') + need(table[1][2]==0 and charge([supports[0]],spaces,owner)=={6:1},'free cross pairing is not copy charge') + controls+=['residual undercharge rejected','cross-rank-zero undercharge rejected'] + return dict(candidate_sha256=hashlib.sha256(raw).hexdigest(),payload_sha256=MEMBER_SHA, + ports=112,free_ordered_pairs=free,scalar_minrank=57,clique_ports=ports, + copy_profile={str(r):n for r,n in profile.items()},copy_mass=mass, + rational_endpoint_entries=12544,zero_saving_allowance=str(allowance), + centre_excess=str(F(mass)-allowance),favorable_M0=str(moment), + historical_scalar_minrank=99,historical_copy_profile={str(r):n for r,n in old_profile.items()}, + controls=controls,scope='finite scalar fit; no native word, supplier or exponent improvement') + +def main(): + parser=argparse.ArgumentParser(description=__doc__);parser.add_argument('--write',type=Path);args=parser.parse_args() + result=compute() + if args.write: + with args.write.open('x',encoding='utf-8') as stream:stream.write(json.dumps(result,indent=2)+'\n') + else:need(canonical(result)==canonical(strict_json((HERE/'RESULT.json').read_text())),'receipt drift') + print('PASS_P112_TRIPLANE_FIT minrank=57 previous=99 free_pairs=420 profile=3H3+53H6+H7 mass=334 M0=32871/32704 controls=8 no_kappa') + +if __name__=='__main__':main() From c8216fca1ed2a301a95e7e0b1e5844d4cfda02c6 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 22:28:16 +0200 Subject: [PATCH 08/22] Add P112 rank-57 fit independent_check.py --- .../independent_check.py | 257 ++++++++++++++++++ 1 file changed, 257 insertions(+) create mode 100644 research/p112-rational-decoder-gate/independent_check.py diff --git a/research/p112-rational-decoder-gate/independent_check.py b/research/p112-rational-decoder-gate/independent_check.py new file mode 100644 index 0000000000..ab5e05054c --- /dev/null +++ b/research/p112-rational-decoder-gate/independent_check.py @@ -0,0 +1,257 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent exact P112 scalar fits and port-space tariff checks. + +No producer, package verifier, or predecessor executable is imported. Literal +cliques give lower bounds; independent disjoint support constructions give +matching upper bounds over every field. The separate rational gauge replay +is over Q only. This is not a native supplier or exponent certificate. +""" +from collections import Counter +from fractions import Fraction as F +from hashlib import sha1, sha256 +import json +from pathlib import Path +import sys +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = Path(sys.argv[1]) if len(sys.argv) > 1 else HERE.parents[1] +OLD = 'research/tri-plane-port-p112-seeddb093026/CANDIDATE.json' +ARCHIVE = 'research/community-frontier1094-audit/selected-replay.tar.gz' +PINS = { + OLD: ('92b5f2f835e9f226bba2d936b7bf9ba9300462a9112492bcb70229eb63a84901', + '438d5c4b1564495bbfeaca2cffa42453c455b3ad'), + ARCHIVE: ('f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6', + 'c24daf067f9c543421d89ca2eeaa4eb78a57fb6f'), +} +CANDIDATE_SHA = 'dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b' +MEMBER = 'candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' +PAYLOAD_SHA = 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa' +OLD_CLIQUE = (1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 14, 15, 16, + 17, 18, 20, 21, 22, 23, 24, 26, 27, 28, 29, 30, + 31, 32, 33, 34, 35, 36, 37) +NEW_CLIQUE = tuple(range(1, 38, 2)) + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def require_digest(data, expected, why): + need(sha256(data).hexdigest() == expected, why) + + +def authenticated(path): + data = (ROOT / path).read_bytes() + expected_sha, expected_blob = PINS[path] + require_digest(data, expected_sha, 'sha256 ' + path) + need(sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() == expected_blob, + 'git blob ' + path) + return data + + +def bit_rank(rows): + pivots = {} + for row in rows: + while row: + pivot = row.bit_length() - 1 + if pivot in pivots: + row ^= pivots[pivot] + else: + pivots[pivot] = row + break + return len(pivots) + + +def dot(x, y): + return (x & y).bit_count() % 2 + + +def pairing(left, right): + return bit_rank([sum(dot(x, y) << j for j, y in enumerate(right)) for x in left]) + + +def geometry(groups, labels): + need(len(groups) == 38 and len(groups[0]) == 1 + and all(len(g) == 3 for g in groups[1:]), 'one line and37 three-frames') + need(sorted(i for g in groups for i in g) == list(range(112)), 'scalar port partition') + spaces = [[labels[i] for i in g] for g in groups] + for frame in spaces: + need(all(dot(x, y) == int(i == j) for i, x in enumerate(frame) + for j, y in enumerate(frame)), 'orthonormal port space') + owners = {i: g for g, coords in enumerate(groups) for i in coords} + orth = [(i, j) for i in range(38) for j in range(i + 1, 38) + if pairing(spaces[i], spaces[j]) == 0] + free = {(i, j) for i in range(112) for j in range(112) if i != j + and pairing(spaces[owners[i]], spaces[owners[j]]) == 0} + return spaces, owners, orth, free + + +def valid_clique(indices, groups, spaces): + return (len(set(indices)) == len(indices) + and all(len(groups[i]) == 3 for i in indices) + and all(pairing(spaces[i], spaces[j]) > 0 for i in indices for j in indices)) + + +def tariff(support, spaces, owners): + vectors = [x for g in {owners[i] for i in support} for x in spaces[g]] + return pairing(vectors, vectors) + + +def matrix(supports, scale): + result = [[F(0) for _ in range(112)] for _ in range(112)] + for support in supports: + for i in support: + for j in support: + result[i][j] += scale[i] / scale[j] + return result + + +def valid_endpoint(K, free): + return (all(K[i][i] == 1 for i in range(112)) + and all(i == j or (i, j) in free or K[i][j] == 0 + for i in range(112) for j in range(112))) + + +def certify_fit(groups, labels, supports, clique, expected_rank, expected_profile, expected_free): + spaces, owners, orth, free = geometry(groups, labels) + need(len(free) == expected_free, 'exact free-pair count') + need(valid_clique(clique, groups, spaces), 'literal nonorthogonal clique') + principal = [i for g in clique for i in groups[g]] + need(len(principal) == expected_rank, 'identity minor size') + # Disjoint nonempty indicator columns are independent over EVERY field. + # Their sum of outer products has one all-ones block per support and hence + # rank exactly the number of supports, irrespective of characteristic. + need(len(supports) == expected_rank and all(supports) + and sorted(i for s in supports for i in s) == list(range(112)), + 'nonempty disjoint factor supports partition all scalar coordinates') + K = matrix(supports, [F(1)] * 112) + need(valid_endpoint(K, free), 'all12544 scalar coefficients fit the complete mask') + need(all(K[i][j] == int(i == j) for i in principal for j in principal), 'forced identity minor') + profile = Counter(tariff(s, spaces, owners) for s in supports) + need(profile == expected_profile, 'exact port-space copy profile') + need(sum(r * n for r, n in profile.items()) == 334, 'full copy mass') + return spaces, owners, orth, free, principal, K + + +def main(): + old_data = json.loads(authenticated(OLD)) + old_groups = old_data.get('candidate', old_data)['groups'] + authenticated(ARCHIVE) + with tarfile.open(ROOT / ARCHIVE, 'r:gz') as f: + payload = f.extractfile(MEMBER).read() + require_digest(payload, PAYLOAD_SHA, 'selected label member pin') + recipes = sorted(json.loads(payload)['recipes'], key=lambda r: r['port']) + need([r['port'] for r in recipes] == list(range(112)), 'selected port indexing') + labels = [r['q'] for r in recipes] + need(len(set(labels)) == 112 and all(0 < q < 512 and dot(q, q) for q in labels), 'selected odd labels') + need(all(r['terminal_Y_translation'] == r['q'] for r in recipes), 'selected translation labels') + candidate_bytes = (HERE / 'CANDIDATE.json').read_bytes() + require_digest(candidate_bytes, CANDIDATE_SHA, 'published candidate pin') + candidate = json.loads(candidate_bytes) + need(candidate['scientific_base'] == '7ef5f7150476fdf995b286b9cdbed262c631939c' + and candidate['source_payload_sha256'] == PAYLOAD_SHA, 'candidate source identity') + + # The old cover also has an exact99-factor fit. This construction is new + # comparison evidence here, not PR2041's invalid11-factor binary decoder. + old_pairs = [(6, 13), (7, 12), (9, 19), (22, 25)] + old_supports = [[i, j] for a, b in old_pairs for i, j in zip(old_groups[a], old_groups[b])] + old_supports.append([old_groups[0][0], old_groups[1][0]]) + old_used = {i for s in old_supports for i in s} + old_supports.extend([[i] for i in range(112) if i not in old_used]) + old_fit = certify_fit(old_groups, labels, old_supports, OLD_CLIQUE, 99, + {3: 86, 4: 1, 6: 12}, 102) + + groups = candidate['groups'] + new_pairs = [(g, g + 1) for g in range(1, 36, 2)] + supports = [[i, j] for a, b in new_pairs for i, j in zip(groups[a], groups[b])] + # The residual line joins the first paired coordinates of groups15/16. + residual_pair = next(s for s in supports if s == [groups[15][0], groups[16][0]]) + residual_pair.append(groups[0][0]) + supports.extend([[i] for i in groups[37]]) + new_fit = certify_fit(groups, labels, supports, NEW_CLIQUE, 57, + {3: 3, 6: 53, 7: 1}, 420) + spaces, owners, orth, free, principal, unit_K = new_fit + need(candidate['factor_supports'] == supports, 'published factors equal independent construction') + need(candidate['disjoint_free_triad_pairs'] == [list(p) for p in new_pairs] + and all(p in orth for p in new_pairs), '18 disjoint free triad pairs') + need(candidate['orthogonal_group_pairs'] == [list(p) for p in orth], 'complete published orthogonality table') + need(candidate['clique_groups'] == list(NEW_CLIQUE), 'published clique is independent literal clique') + need(candidate['claimed_minimum_scalar_rank'] == 57 + and candidate['claimed_copy_profile'] == {'3': 3, '6': 53, '7': 1} + and candidate['claimed_copy_mass'] == 334, 'published scalar rank and whole-space bill') + + # Gauge replay with halves: a_i=d_i and b_j=1/d_j on each support. This + # checks genuine rational scalar entries, but introduces no2-adic gain: + # undoing the diagonal gauge recovers the integral indicator fit above. + scale = [F(x) for x in candidate['rational_test_scalings']] + need(scale == [F(1 + (i % 2)) for i in range(112)], 'explicit rational gauge') + K = matrix(supports, scale) + need(valid_endpoint(K, free), 'all12544 rational-gauge endpoint coefficients') + need(any(x.denominator == 2 for row in K for x in row), 'nonintegral scalar entries occur') + need(all(K[i][j] * scale[j] / scale[i] == unit_K[i][j] + for i in range(112) for j in range(112)), 'exact diagonal-gauge equivalence') + need(all(K[i][j] == int(i == j) for i in principal for j in principal), 'rational identity minor') + # Every source basis column is replayed against distinct arbitrary target + # dirt. Forbidden outputs preserve it; the matching output receives one. + dirty = [F(1000 + i, 13) for i in range(112)] + for j in range(112): + output = [dirty[i] + K[i][j] for i in range(112)] + need(output[j] == dirty[j] + 1 + and all(output[i] == dirty[i] for i in range(112) if i != j and (i, j) not in free), + 'dirty target source-basis replay') + need(F(8, 9) * 334 == F(2672, 9) and F(334) - F(2672, 9) == F(334, 9), + 'exact mixed-cover allowance and positive deficit') + + controls = 0 + try: + require_digest(candidate_bytes + b' ', CANDIDATE_SHA, 'mutated source bytes') + except ValueError: + pass + else: + raise ValueError('source byte corruption was accepted') + controls += 1 + bad = [row[:] for row in K] + bad[principal[0]][principal[1]] = 1 + need(not valid_endpoint(bad, free), 'forbidden-entry corruption rejected') + controls += 1 + bad = [row[:] for row in K] + bad[groups[0][0]][groups[0][0]] = 0 + need(not valid_endpoint(bad, free), 'lost residual payload rejected') + controls += 1 + broken_clique = tuple(2 if g == 3 else g for g in NEW_CLIQUE) + need(not valid_clique(broken_clique, groups, spaces), 'orthogonal-pair clique corruption rejected') + controls += 1 + need(3 * 3 + 54 * 6 == 333, 'rank-six residual undercharge is one unit short') + need(tariff(residual_pair, spaces, owners) == 7, 'residual factor consumes all seven dimensions') + controls += 1 + label_only_mass = sum(pairing([labels[i] for i in s], [labels[i] for i in s]) for s in supports) + need(label_only_mass == 112 and label_only_mass != 334, 'label-only undercharge rejected') + controls += 1 + need(pairing(spaces[15], spaces[16]) == 0 + and pairing(spaces[15] + spaces[16], spaces[15] + spaces[16]) == 6, + 'free cross pairing is not full support self-pairing tariff') + controls += 1 + B0 = [[dot(labels[i], labels[j]) for j in range(112)] for i in range(112)] + need(not valid_endpoint(B0, free), 'literal binary pairing is not scalar mask identity') + need(sum(B0[i][j] != 0 for i in range(112) for j in range(112) + if i != j and (i, j) not in free) == 6608, 'binary pairing forbidden entries') + controls += 1 + bad = [[F(0) for _ in range(112)] for _ in range(112)] + for s in supports: + for i in s: + for j in s: + bad[i][j] += scale[i] * scale[j] + need(not valid_endpoint(bad, free), 'lost reciprocal factor rejected') + controls += 1 + need(old_fit[3] != free and 99 > 57, 'changed mask is not a rescaled old decoder') + print('PASS_INDEPENDENT_P112_RATIONAL_FIT old_minrank=99 new_minrank=57 ' + 'fields=all old_free=102 new_free=420 rational_entries=12544 dirty_columns=112 ' + 'profile=3H3+53H6+H7 mass=334 allowance=2672/9 deficit=334/9 ' + 'controls=%d no_native_or_exponent_claim' % controls) + + +if __name__ == '__main__': + main() From ae27e54efacc2b546948391d68756b5bc5fa3ca3 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 22:59:40 +0200 Subject: [PATCH 09/22] Prove P112 rational decoder cost floors of 334 and 308 Added a detailed proof for the P112 rational decoder cost floors, including statements, geometric premises, and consequences for factorization. --- .../RANK-TIGHT-PROOF.md | 238 ++++++++++++++++++ 1 file changed, 238 insertions(+) create mode 100644 research/p112-rational-decoder-gate/RANK-TIGHT-PROOF.md diff --git a/research/p112-rational-decoder-gate/RANK-TIGHT-PROOF.md b/research/p112-rational-decoder-gate/RANK-TIGHT-PROOF.md new file mode 100644 index 0000000000..11a0b94398 --- /dev/null +++ b/research/p112-rational-decoder-gate/RANK-TIGHT-PROOF.md @@ -0,0 +1,238 @@ +# P112 rational decoder cost floors: 334 at minimum length, 308 within both spans + +This is a sharp restriction on the fixed changed-triad mask of PR2757, not a universal rational-decoder obstruction. + +## Statement and scope + +Use PR2757 head `c8216fca1ed2a301a95e7e0b1e5844d4cfda02c6` and its fixed CANDIDATE.json, SHA256 `dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b`. Keep its 112 ports, 37 orthonormal triads G1,...,G37, residual line G0, and full-group scalar mask. Write E_g for each binary group space. Entries K_pq with p!=q are forced zero unless E_owner(p) is orthogonal to E_owner(q), and all diagonal entries equal one common nonzero rational c. + +For a nonzero rational rank-one term u_t v_t^T, charge rho(S_t,T_t), the F2 pairing rank between the sums of all complete group spaces touched by u_t and v_t. Absorb any nonzero scalar coefficient into u_t; this changes no supports or charge. + +**Theorem.** Every valid fitting decoder expressed as exactly 57 nonzero rational rank-one terms has total port-space charge at least 334. The indicator decomposition in PR2757 attains 334, so this lower bound is sharp within the exactly-57-term class. Therefore a decoder with total charge at most 296 needs at least 58 nonzero scalar rank-one terms. + +The 334 theorem alone does not exclude decompositions with more than 57 terms, even when their sum has matrix rank 57. Section 5 gives a separate 308 bound when both factor families remain in the rank-57 fitting matrix's spans. Neither result excludes fitting matrices of larger rank, altered covers, block-valued factors, or a changed physical tariff. No claim about a native supplier or exponent follows. + +## Exact geometric premises + +The source-bound standard-library checker `check_rank_tight_floor.py` imports no predecessor executable and recomputes the following from the pinned selected labels. It uses F2 only to compute spaces and their tariff; it never reduces rational decoder coefficients modulo two. + +Let I contain all three ports of each odd group G1,G3,...,G37. Every two groups in this list are nonorthogonal, so K_II=I57 after normalization c=1. Let R be the line and the even groups. Among the odd groups, the only allowed neighbors of an even group 2j are {2j-1}, except that group24 has {3,23}. The line has allowed odd neighbors {15,27}. In addition: + +- E4 is not orthogonal to E24, and group4 has only odd neighbor3. +- E28 is not orthogonal to E0, and group28 has only odd neighbor27. +- For j=1,...,18, let H_j=E_(2j-1)+E_(2j). The two summands are orthogonal nondegenerate three-spaces, so rho(H_j,H_j)=6. +- Let J=E37. For every ordered pair i,j in {1,...,18}, rho(J+H_i,J+H_j)>=6. The 324 exact ranks have histogram {6:11,7:93,8:171,9:49}. +- E0 is orthogonal to E15 and E16, so rho(E0+H_8,E0+H_8)=7. + +The lower bound for J+H_i cannot be replaced by a blanket bound rho(H_i,H_j)>=6. The latter is false: the bare pair ranks have histogram {4:20,5:178,6:126}. This is a useful scope control. + +## 1. Normal form of every rank-57 fit + +Normalize the common nonzero diagonal c to one by scaling the full fitting matrix and one factor side. Supports and tariffs are unchanged. Order coordinates as I,R and write + + K = [ I57 A ] + [ B D ]. + +The principal identity forces rank(K)>=57. An expression with 57 rank-one terms forces rank(K)<=57. Therefore rank(K)=57, and the Schur complement gives D=BA. + +The allowed-neighbor list determines the block supports of A and B. All even groups except24 can interact with only their matching odd group. At group4, + + I3 = D_4,4 = B_4,3 A_3,4, + +so B_4,3 and A_3,4 are invertible rational 3-by-3 matrices. The forbidden blocks D_4,24=D_24,4=0 imply + + B_4,3 A_3,24 = 0, B_24,3 A_3,4 = 0. + +Thus A_3,24=B_24,3=0. Group24 also interacts only with its matching odd group23. + +Likewise the identity at group28 makes B_28,27 and A_27,28 invertible. Since the line and group28 are not orthogonal, D_0,28=D_28,0=0. Hence + + B_0,27 A_27,28 = 0, B_28,27 A_27,0 = 0, + +and B_0,27=A_27,0=0. The line interacts only with odd group15. + +Consequently, for each matched pair (2j-1,2j), A and B contain inverse 3-by-3 maps between the odd and even coordinates. The line is described by a general rational row b=B_0,15 and column a=A_15,0 with ba=1. There is no need to make a or b coordinate vectors. Group37 has no R-neighbor and remains an isolated I3 block. The remaining entries of D are determined by BA. In particular, the extra allowed free edges cannot be used at matrix rank57. + +## 2. Consequences for an arbitrary 57-term factorization + +Write K=UV^T with U,V of size112-by-57, one column per nonzero term. Set P=U_I and Q=V_I. The identity minor gives + + P Q^T = I57, Q^T P = I57. + +Both P and Q are invertible. Comparing the I,R blocks gives + + U_R = B P, V_R = A^T Q. + +For every factor column, nonzero odd coordinates in any paired group are therefore equivalent to nonzero even coordinates in its partner, on each factor side separately: the associated maps are invertible. A factor vector whose retained coordinates are confined to group37 is physically supported only in group37. Conversely, every nonzero paired component touches both complete three-spaces in that pair for tariff purposes. + +For term t, the dual-basis identity gives q_t^T p_t=1. Thus there is at least one retained scalar coordinate where both factor vectors are nonzero. + +If a common nonzero retained coordinate lies in a paired group, both full supports include its entire H_j, and monotonicity of pairing rank under enlarging either space gives charge at least6. + +Otherwise, every common retained coordinate is in group37, so both factors have nonzero J components. If neither factor is supported only in group37, their supports include J+H_i and J+H_j for some i,j, so the certified 324-case bound again gives charge at least6. + +It follows that every term of charge below6 has at least one factor supported only in group37. Such a term has charge exactly3: one side is J, and the other includes J; its pairing rank is at least rho(J,J)=3 and at most dim(J)=3. + +## 3. At most three terms can cost below six + +Let L_U be the set of column indices for which p_t is supported in the three-coordinate subspace W corresponding to group37. Let L_V be the analogous set for q_t. The previous section places every term of charge below6 in L_U union L_V; conversely every index in that union has charge3. + +Put alpha=|L_U|, beta=|L_V|, gamma=|L_U intersection L_V|. Since P and Q are invertible, their indicated columns are independently linearly independent. The restricted pairing matrix Q_(L_V)^T P_(L_U) is the corresponding submatrix of I57, hence has rank gamma. + +The beta independent columns of Q_(L_V) lie in the nondegenerate three-coordinate space W. The common annihilator of these columns in W has dimension 3-beta. The kernel of their pairing on the alpha-dimensional span of P_(L_U) has dimension alpha-gamma, so + + alpha-gamma <= 3-beta. + +Therefore |L_U union L_V|=alpha+beta-gamma<=3. This uses rational linear algebra and does not assume positivity, symmetric factors, disjoint supports, or an integral reduction. + +## 4. The residual line supplies the last unit + +The scalar diagonal at the residual port is one, so at least one term has both u_(0,t) and v_(0,t) nonzero. From U_0=b P_15 and V_0=a^T Q_15, that term has nonzero components in odd group15 on both sides, and then in even group16 on both sides by the invertible partner maps. Its two support spaces both contain E0+E15+E16, whose pairing rank is7. + +This term is not one of the group37-only terms. If l<=3 terms have charge3, the other57-l terms cost at least6 and at least one costs at least7. Thus + + C >= 3l + 6(57-l) + 1 = 343-3l >= 334. + +The PR2757 indicator construction has exactly three group37 singleton terms of charge3, 53 ordinary paired terms of charge6, and one line-bearing term of charge7, attaining334. + +## 5. Any number of factors within the fitting matrix's spans costs at least 308 + +This is a scoped extension of the rank-57 argument for the pinned PR2757 mask. +It does not cover arbitrary higher-rank fitting matrices, or factorizations +whose source or reader factors have components outside the fitting matrix's +column or row space. + +Normalize the diagonal to one. Let K be any rank-57 fit on this mask, with +the normal form `K = [I, A; B, BA]` proved above. Assume the columns of U lie +in col(K), and the columns of V lie in col(K^T), for a factorization K=UV^T. +Write P=U_I and Q=V_I. The two span assumptions give + + U = [ P ], V = [ Q ], P Q^T = I57. + [ BP] [ A^T Q] + +Thus the retained rank-one terms satisfy + + sum_{t=1}^m p_t q_t^T = I57, m = 57+s, s >= 0. + +The invertible paired maps force the same paired group support on each side. +The residual coefficients are b p_(15,t) and a^T q_(15,t); a and b need not be +coordinate vectors. No change of basis or reduction of coefficients modulo two +is needed for this extension. + +We charge every term by the full port-space pairing tariff. Scalar entries +and even denominators are unrestricted. Zero terms are discarded before m is +counted. + +### Finite geometry premises + +Partition the 57 latent coordinates into 19 blocks of size three: eighteen +paired components and J=G37. A nonzero paired component touches its entire +nondegenerate six-space H_i. A nonzero physical residual coefficient also +touches G0; ignoring that extra line only decreases the tariff. A nonzero J +component touches the nondegenerate three-space J. + +The independent closure checker reconstructs the pinned labels and proves: + +- rho(J,J)=3 and rho(J,H_i)=rho(H_i,J)=3 for every i. +- rho(H_i,H_j)>=4 for all 324 ordered pairs. +- rho(J+H_i,J+H_j)>=6 for all 324 ordered pairs. +- All spans generated by the 19 component spaces form an explicitly closed + set of 40 subspaces. Among pairs of these spans that each contain a paired + component and have pairing rank below six, the maximal component-support + rectangle sizes are as follows: + + rank 4: 1 by 1 only (20 ordered span pairs) + rank 5: 1 by 1 (178), 1 by 2 and 2 by 1 (33 each), + 1 by 3 and 3 by 1 (4 each). + + No such rectangle has a component on both sides. Taking the maximal closure + supports is conservative: an actual term can touch fewer components. +- The residual's actual support G0+G15+G16 is nondegenerate of rank seven. + +### Discount bound from an acyclic subset + +Call a term pure if at least one of p_t,q_t is supported entirely in J. Each +nonzero pure term has tariff exactly three, including when the other side has +no J coordinate. This uses the separate rho(J,H_i)=3 premise; diagonal overlap +is not assumed. + +Every nonpure term has tariff at least four. Let L4 and L5 count its terms of +actual tariff four and five. Their component support rectangles are disjoint: +a common paired component would force tariff at least six, and J on both sides +would force at least six by the enlarged-pairing premise. + +Choose a uniformly random order of the 19 components, and select a low-tariff +term if every component in its left support precedes every component in its +right support. Its probability is 1/binomial(a+b,a). The finite census shows +this probability is exactly 1/2 for a tariff-four term and at least 1/4 for a +tariff-five term. The census ignores the residual line, so a tariff-five term +may have underlying rank four; that only increases its selection probability. + +For any fixed order, the selected terms sum to a strictly block upper triangular +matrix N. Thus I_57-N is invertible, without any positivity or coefficient-size +hypothesis. If k terms were selected, the remaining m-k rank-one terms still +sum to I_57-N, so m-k>=57 and k<=s. Taking expectations yields + + L4/2 + L5/4 <= s, hence 2 L4 + L5 <= 4s. + +### Pure terms and the invoice + +Let P be the number of pure terms. Restrict the identity to the other 54 latent +coordinates. Every pure term vanishes in this principal restriction, so its +rank 54 forces m-P>=54 and P<=s+3. + +The residual diagonal is one, so some term has nonzero residual entry on both +sides. It is nonpure and has tariff at least seven. Therefore + + C >= 6m - 3P - 2L4 - L5 + 1 >= 334-s. + +A second bound uses only the minimum nonpure tariff four and the same residual +term: + + C >= 3P + 4(m-P) + 3 >= 228+3s. + +Consequently + + C >= max(334-s, 228+3s) >= 308 for integer s>=0. + +The integer minimum of the displayed bound is 308, at s=26. This already +exceeds the necessary positive-saving allowance 2672/9 (integer C<=296). +The weaker first inequality alone would require m>=95 to reach that allowance; +the second inequality eliminates that possibility within this model. + +This closes overcomplete scalar decompositions only when BOTH factor spans +remain canonical. The ambient 112-coordinate problem can introduce exterior +components, including components that cancel between terms; those are outside +this proof. Higher-rank fitting matrices are also outside the proof. The +finite geometry check is not a native implementation or a supplier theorem. + +## What this changes + +Minimum scalar rank57 and a low-charge decoder are different optimization goals. All exactly57-term rational factorizations fail the favorable positive-saving requirement C<2672/9. Any target C<=296 must use at least58 terms, with actual extra directions/cancellation; arbitrary diagonal gauges, groupwise rational changes of basis and asymmetric rank-tight factors cannot suffice. The additional bound of 308 applies to any term count when both factor families remain in the rank-57 fitting matrix's column and row spaces. There is no bound here for arbitrary exterior factors or higher-rank fitting matrices. + +The finite geometry was separately recomputed by another AI agent, including the complete 324-case histogram; that agent also audited the normal-form elimination and the pure-factor dimension argument. This is independent AI checking, not independent human review or proof-assistant formalization. + +## Replay and credit + +From the repository root, Python 3.12 standard library only: + +```sh +python3 -I -O -B research/p112-rational-decoder-gate/check_rank_tight_floor.py +python3 -I -O -B research/p112-rational-decoder-gate/independent_cost_floor.py +python3 -I -O -B research/p112-rational-decoder-gate/check_overcomplete_closure.py +``` + +The first checker authenticates the candidate, selected archive and payload, +then recomputes every finite geometric premise. The second uses independent +binary elimination, checks all 324 pairings, and replays dense rational fixtures +with non-coordinate residual maps and uncancelled even denominators. It rejects +granting either critical forbidden edge, replacing full groups with original +labels for pricing, and corrupting the residual diagonal. These finite checks +support the symbolic proofs above; they do not formally verify its universal +quantifiers. The separate closure checker reconstructs all 40 component spans and rejects both a missing seed and a missing generated span. Its echelon representation is independent of the first checker's explicit vector-set closure. + +This proof extends the pending PR2757 construction, whose earlier head is pinned +above. The selected P112 labels, tri-plane endpoint, strict mask and full-space +tariff retain their predecessor attribution in the package [README](README.md). +Prepared by flyingviper with substantial OpenAI Codex assistance and separate +AI-agent checking. New work is Apache-2.0; no independent human review is claimed. From 08ad9f998cd61769ca31636cabda4bb2938a919b Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 23:00:31 +0200 Subject: [PATCH 10/22] Add P112 finite-premise checker for cost floors 334 and 308 --- .../check_rank_tight_floor.py | 177 ++++++++++++++++++ 1 file changed, 177 insertions(+) create mode 100644 research/p112-rational-decoder-gate/check_rank_tight_floor.py diff --git a/research/p112-rational-decoder-gate/check_rank_tight_floor.py b/research/p112-rational-decoder-gate/check_rank_tight_floor.py new file mode 100644 index 0000000000..7927f7accb --- /dev/null +++ b/research/p112-rational-decoder-gate/check_rank_tight_floor.py @@ -0,0 +1,177 @@ +#!/usr/bin/env python3 +"""Finite premises for the rank-tight 57-term port-space lower bound. +No rational reduction modulo two: F2 is used only for the support tariff. +""" +from collections import Counter +from hashlib import sha256 +import json +from math import comb +from pathlib import Path +import tarfile + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +CANDIDATE_SHA = 'dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b' +ARCHIVE_SHA = 'f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6' +PAYLOAD_SHA = 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa' +MEMBER = 'candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' + +def need(ok, message): + if not ok: + raise ValueError(message) + +def rank(rows): + # Explicit low-column Gaussian elimination, distinct from the independent + # checker's highest-pivot dictionary. Rows are bit-packed binary vectors. + rows = list(rows) + ncols = max((row.bit_length() for row in rows), default=0) + pivot_row = 0 + for column in range(ncols): + found = next((i for i in range(pivot_row, len(rows)) + if (rows[i] >> column) & 1), None) + if found is None: + continue + rows[pivot_row], rows[found] = rows[found], rows[pivot_row] + for i in range(pivot_row+1, len(rows)): + if (rows[i] >> column) & 1: + rows[i] ^= rows[pivot_row] + pivot_row += 1 + return pivot_row + +def dot(a,b): + return (a&b).bit_count()%2 + +def rho(a,b): + return rank([sum(dot(x,y)<= 4, 'nonpure tariff at least4') + if charge >= 6: + continue + A, B = closures[left], closures[right] + need(not set(A).intersection(B), 'low-tariff component supports disjoint') + probability_denominator = comb(len(A)+len(B), len(A)) + need(probability_denominator <= (2 if charge == 4 else 4), + 'acyclic sampling probability bound') + rectangles[(len(A),len(B),charge)] += 1 + need(rectangles == {(1,1,4):20, (1,1,5):178, (1,2,5):33, + (1,3,5):4, (2,1,5):33, (3,1,5):4}, + 'exact low-tariff rectangle census') + # For integer s>=0, s<=26 gives334-s>=308, while s>=27 + # gives228+3s>=309. The value308 occurs at s=26. + need(334-26 == 308 and 228+3*27 == 309, 'integer envelope floor308') + return {'component_span_count':len(spans), + 'nonpure_component_span_count':len(nonpure), + 'low_tariff_rectangles':{','.join(map(str,k)):v for k,v in sorted(rectangles.items())}, + 'pure_J_pairings':{'3':18}, + 'canonical_span_copy_lower_bound':308, + 'scope':'Any term count, rank57 fitting matrix, BOTH factor families confined to its column and row spaces. Exterior directions and higher matrix ranks excluded.'} + +def main(): + raw = (PACKAGE/'CANDIDATE.json').read_bytes() + need(sha256(raw).hexdigest()==CANDIDATE_SHA, 'candidate pin') + candidate = json.loads(raw) + archive = ROOT/'research/community-frontier1094-audit/selected-replay.tar.gz' + need(sha256(archive.read_bytes()).hexdigest()==ARCHIVE_SHA, 'archive pin') + with tarfile.open(archive, 'r:gz') as t: + payload=t.extractfile(MEMBER).read() + need(sha256(payload).hexdigest()==PAYLOAD_SHA, 'payload pin') + data=json.loads(payload) + recipes=sorted(data['recipes'],key=lambda r:r['port']) + need([r['port'] for r in recipes]==list(range(112)), 'ports') + labels=[r['q'] for r in recipes] + groups=candidate['groups'] + need(len(groups)==38 and len(groups[0])==1 and all(len(g)==3 for g in groups[1:]), 'dimensions') + need(sorted(p for g in groups for p in g)==list(range(112)), 'partition') + spaces=[[labels[p] for p in g] for g in groups] + need(all(dot(x,y)==int(i==j) for basis in spaces for i,x in enumerate(basis) for j,y in enumerate(basis)), 'orthonormal frames') + pairing=[[rho(a,b) for b in spaces] for a in spaces] + retained=list(range(1,38,2)) + need(all(pairing[i][j]>0 for i in retained for j in retained), 'I57 principal minor') + outside=[0]+list(range(2,37,2)) + allowed={g:[h for h in retained if pairing[g][h]==0] for g in outside} + expected={g:[g-1] for g in outside if g!=0} + expected[24]=[3,23] + expected[0]=[15,27] + need(allowed==expected, 'all outside-to-clique free supports') + # K4,4=I gives inverse maps at the unique neighbor3. K4,24 and + # K24,4 are forced zero, so both group24-to-3 maps vanish. + need(allowed[4]==[3] and pairing[4][24]>0, 'group24 extra maps eliminated') + # Likewise the invertible group28 maps at27 eliminate line0-to-27. + need(allowed[28]==[27] and pairing[0][28]>0, 'residual extra maps eliminated') + pairs=[(g,g+1) for g in range(1,36,2)] + H=[spaces[a]+spaces[b] for a,b in pairs] + need(all(pairing[a][b]==0 and rho(h,h)==6 for (a,b),h in zip(pairs,H)), 'paired six-spaces') + J=spaces[37] + combined=[[rho(J+a,J+b) for b in H] for a in H] + histogram=Counter(x for row in combined for x in row) + need(min(histogram)==6 and histogram=={6:11,7:93,8:171,9:49}, 'all324 mixed support bounds') + residual=spaces[0]+H[7] + need(rho(residual,residual)==7, 'residual pair span seven') + bare=Counter(rho(a,b) for a in H for b in H) + # The stronger universal bound on arbitrary paired spaces would be false. + need(min(bare)<6, 'negative control: pure cross-pair terms can cost below six') + canonical = canonical_span_premises(H, J) + receipt={ + 'source_head':'c8216fca1ed2a301a95e7e0b1e5844d4cfda02c6', + 'candidate_sha256':CANDIDATE_SHA, + 'archive_sha256':ARCHIVE_SHA, + 'payload_sha256':PAYLOAD_SHA, + 'retained_clique_groups':retained, + 'outside_allowed_clique_groups':allowed, + 'pair_plus_G37_rho_table':combined, + 'pair_plus_G37_rho_histogram':dict(sorted(histogram.items())), + 'bare_pair_rho_histogram':dict(sorted(bare.items())), + 'residual_pair_self_rank':7, + 'rank_tight_terms':57, + 'maximum_terms_below_six':3, + 'tariff_lower_bound':334, + 'canonical_span_extension':canonical, + 'scope':'All rational 57-term rank-one fitting decompositions of this fixed mask. Written proof required; not an arbitrary-term bound.', + } + print(json.dumps(receipt,indent=2)) + print('PASS_RANK_TIGHT_57_TERM_COST_FLOOR_334_FINITE_PREMISES') + +if __name__=='__main__': main() From 676b51157bf94a376a60f70f036179ddec311f6d Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 23:00:52 +0200 Subject: [PATCH 11/22] Add P112 cost-floor checker independent_cost_floor.py --- .../independent_cost_floor.py | 189 ++++++++++++++++++ 1 file changed, 189 insertions(+) create mode 100644 research/p112-rational-decoder-gate/independent_cost_floor.py diff --git a/research/p112-rational-decoder-gate/independent_cost_floor.py b/research/p112-rational-decoder-gate/independent_cost_floor.py new file mode 100644 index 0000000000..abf66b9e48 --- /dev/null +++ b/research/p112-rational-decoder-gate/independent_cost_floor.py @@ -0,0 +1,189 @@ +#!/usr/bin/env python3 +"""Independent finite premises and rational fixtures for the rank-tight P112 cost floor. + +No predecessor executable imports. The universal argument is +symbolic: Schur complement, groupwise change of basis, duality in a 3-space. +This checker independently authenticates and checks its finite premises. +""" +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path +import hashlib +import json +import tarfile + +ROOT = Path(__file__).resolve().parents[2] +CANDIDATE = ROOT / 'research/p112-rational-decoder-gate/CANDIDATE.json' +CANDIDATE_LF_SHA = 'dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b' +PAYLOAD_SHA = 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa' +MEMBER = 'candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' + +def require(test, label): + if not test: + raise ValueError(label) + +def rejects(fn, label): + try: + fn() + except ValueError: + return label + raise ValueError('mutation accepted: ' + label) + +def parity(x): + return x.bit_count() % 2 + +def binary_rank(words): + # Highest-pivot dictionary, independent of the retained low-pivot row code. + pivots = {} + for word in words: + while word: + high = word.bit_length() - 1 + if high in pivots: + word ^= pivots[high] + else: + pivots[high] = word + break + return len(pivots) + +def pairing(left, right): + return binary_rank(sum(parity(x & y) << j for j, y in enumerate(right)) for x in left) + +def mm(a, b): + bt = list(zip(*b)) + return [[sum(x*y for x, y in zip(row, col)) for col in bt] for row in a] + +def transpose(a): + return [list(x) for x in zip(*a)] + +def identity(n): + return [[Q(i == j) for j in range(n)] for i in range(n)] + +def inverse(a): + n = len(a) + rows = [[Q(x) for x in row] + extra for row, extra in zip(a, identity(n))] + for k in range(n): + pivot = next((i for i in range(k, n) if rows[i][k]), None) + require(pivot is not None, 'singular rational fixture') + rows[k], rows[pivot] = rows[pivot], rows[k] + divisor = rows[k][k] + rows[k] = [x/divisor for x in rows[k]] + for i in range(n): + if i != k and rows[i][k]: + scalar = rows[i][k] + rows[i] = [x-scalar*y for x, y in zip(rows[i], rows[k])] + return [row[n:] for row in rows] + +def graph_premises(free): + odd = list(range(1, 38, 2)); even = list(range(2, 37, 2)) + require(not any((i,j) in free for i in odd for j in odd), 'odd principal identity') + require({(i,j) for i in odd for j in even if (i,j) in free} == + {(i,i+1) for i in odd[:-1]} | {(3,24)}, 'odd-even mask') + require({i for i in odd if (0,i) in free} == {15,27}, 'line odd mask') + # These forbidden entries force the two exceptional couplings to vanish. + for i,j in ((4,24),(24,4),(0,28),(28,0)): + require((i,j) not in free, 'required Schur zero %d,%d' % (i,j)) + require((0,15) in free and (0,16) in free, 'line compatible paired block') + +def price(a, b, spaces, owner): + total = Counter() + for ca, cb in zip(zip(*a), zip(*b)): + ga = {owner[p] for p,x in enumerate(ca) if x} + gb = {owner[p] for p,x in enumerate(cb) if x} + total[pairing([x for g in ga for x in spaces[g]], [x for g in gb for x in spaces[g]])] += 1 + return dict(sorted(total.items())) + +def endpoint(k, owner, free): + require(all(k[i][i] == 1 for i in range(112)), 'normalized diagonal') + require(all(k[i][j] == 0 for i in range(112) for j in range(112) + if i != j and (owner[i],owner[j]) not in free), 'forbidden scalar entry') + +def block(a, rows, cols): + return [[a[i][j] for j in cols] for i in rows] + +def fixture_schur(k, groups): + retained = [p for g in range(1,38,2) for p in groups[g]] + other = [p for p in range(112) if p not in retained] + require(block(k,retained,retained) == identity(57), 'fixture principal identity') + require(block(k,other,other) == mm(block(k,other,retained),block(k,retained,other)), 'fixture Schur residual') + for even in range(2,37,2): + odd = even-1 + a = block(k,groups[odd],groups[even]); b = block(k,groups[even],groups[odd]) + require(mm(a,b) == identity(3) and mm(b,a) == identity(3), 'fixture matching inverses') + for a,b in ((3,24),(24,3),(0,27),(27,0)): + require(all(x == 0 for row in block(k,groups[a],groups[b]) for x in row), 'fixture exceptional block killed') + require(mm(block(k,groups[0],groups[15]),block(k,groups[15],groups[0])) == [[Q(1)]], 'fixture line duality') + +def main(): + raw = CANDIDATE.read_bytes() + require(b'\r' not in raw, 'candidate newline format') + require(hashlib.sha256(raw).hexdigest() == CANDIDATE_LF_SHA, 'candidate LF pin') + candidate = json.loads(raw) + with tarfile.open(ROOT/'research/community-frontier1094-audit/selected-replay.tar.gz') as archive: + payload = archive.extractfile(MEMBER).read() + require(hashlib.sha256(payload).hexdigest() == PAYLOAD_SHA, 'selected payload pin') + recipes = sorted(json.loads(payload)['recipes'],key=lambda x:x['port']) + require([r['port'] for r in recipes] == list(range(112)), 'label port ordering') + q = [r['q'] for r in recipes]; groups = candidate['groups']; supports = candidate['factor_supports'] + require(len(q) == len(set(q)) == 112 and all(0=6, '324 enlarged pairings') + residual = spaces[0]+spaces[15]+spaces[16] + require(pairing(residual,residual)==7, 'residual whole-space rank seven') + require(len(supports)==57 and sorted(p for s in supports for p in s)==list(range(112)), 'saved factor partition') + v0 = [[Q(p in support) for support in supports] for p in range(112)] + k0 = mm(v0,transpose(v0)); endpoint(k0,owner,free); fixture_schur(k0,groups) + require(price(v0,v0,spaces,owner)=={3:3,6:53,7:1}, 'direct exact tariff') + + # Dense rational changes within each physical group preserve whole-group support. + u0 = [row[:] for row in v0]; w0 = [row[:] for row in v0] + for g,ports in enumerate(groups): + n = len(ports) + change = [[Q(i==j)+Q(g+1,2) for j in range(n)] for i in range(n)] + dual = transpose(inverse(change)) + uu = mm(change,[v0[p] for p in ports]); ww = mm(dual,[v0[p] for p in ports]) + for p,row,dualrow in zip(ports,uu,ww): u0[p]=row; w0[p]=dualrow + k = mm(u0,transpose(w0)); endpoint(k,owner,free); fixture_schur(k,groups) + require(price(u0,w0,spaces,owner)=={3:3,6:53,7:1}, 'group GL3 fixture tariff') + require(all(x for row in block(k,groups[15],groups[0]) for x in row), 'line fixture is not coordinate-aligned') + + # T=I+J has determinant58; T^-1=I-J/58. These are genuinely even-denominator + # products, not a cancelling diagonal column gauge. Every factor is dense. + u = [[x+sum(row) for x in row] for row in u0] + w = [[x-sum(row)/58 for x in row] for row in w0] + require(all(x for row in u for x in row) and all(x for row in w for x in row), 'dense basis fixture') + require(mm(u,transpose(w)) == k, 'dense even-denominator endpoint') + require(any((a*b).denominator%2==0 for a,b in zip(u[0],w[0])), 'uncancelled even denominator') + dense_profile = price(u,w,spaces,owner) + require(dense_profile == {9:57}, 'dense fixture complete tariff') + controls = [] + controls.append(rejects(lambda:graph_premises(free|{(4,24),(24,4)}),'grant formerly forced E4-E24 entry')) + controls.append(rejects(lambda:graph_premises(free|{(0,28),(28,0)}),'grant formerly forced line-E28 entry')) + def original_labels(): + pair = next(s for s in supports if len(s)==2) + require(pairing([q[p] for p in pair],[q[p] for p in pair])==6,'original-label undercharge') + controls.append(rejects(original_labels,'replace complete groups by original labels')) + bad = [row[:] for row in k];bad[groups[0][0]][groups[0][0]]=Q(0) + controls.append(rejects(lambda:endpoint(bad,owner,free),'alter residual endpoint')) + require(54*6+3*3+1==334,'symbolic invoice arithmetic') + result = {'candidate_lf_sha256':CANDIDATE_LF_SHA,'selected_payload_sha256':PAYLOAD_SHA, + 'groups':38,'fitting_rank':57,'enlarged_pairing_histogram':dict(sorted(tariffs.items())), + 'residual_rank':7,'pure_factor_index_union_bound':3,'rank_tight_copy_floor':334, + 'zero_saving_allowance':'2672/9','direct_profile':{3:3,6:53,7:1}, + 'dense_even_denominator_profile':dense_profile,'dense_basis_determinant':58, + 'controls':controls,'scope':'Every exactly57-term rational scalar fit on the pinned mask, under complete port-space one-total pricing. Overcomplete fits and changed contracts are excluded.'} + print(json.dumps(result,sort_keys=True)) + print('PASS_INDEPENDENT_P112_57_TERM_COST_FLOOR') + +if __name__ == '__main__': + main() From d84407ecf83311a0fdeb0fb3b3f99dc691ea5774 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 23:00:58 +0200 Subject: [PATCH 12/22] Add P112 cost-floor checker check_overcomplete_closure.py --- .../check_overcomplete_closure.py | 90 +++++++++++++++++++ 1 file changed, 90 insertions(+) create mode 100644 research/p112-rational-decoder-gate/check_overcomplete_closure.py diff --git a/research/p112-rational-decoder-gate/check_overcomplete_closure.py b/research/p112-rational-decoder-gate/check_overcomplete_closure.py new file mode 100644 index 0000000000..c47a45e862 --- /dev/null +++ b/research/p112-rational-decoder-gate/check_overcomplete_closure.py @@ -0,0 +1,90 @@ +#!/usr/bin/env python3 +"""Self-contained exact geometry audit for the canonical-span overcomplete bound.""" +from pathlib import Path +from collections import Counter +from fractions import Fraction +import hashlib,json,math,tarfile +ROOT=Path(__file__).resolve().parents[2] +CANDIDATE_SHA='dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b' +PAYLOAD_SHA='c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa' +def need(x,s): + if not x:raise ValueError(s) +def basis(vectors): + pivots={} + for x in vectors: + while x: + j=x.bit_length()-1 + if j in pivots:x^=pivots[j] + else:pivots[j]=x;break + for j in sorted(pivots): + for k in pivots: + if k>j and ((pivots[k]>>j)&1):pivots[k]^=pivots[j] + return tuple(pivots[j] for j in sorted(pivots)) +def rho(a,b): + return len(basis(sum(((x&y).bit_count()%2)<=4,'nonpure tariff floor') + expanded_hist=Counter(rho(J+a,J+b) for a in H for b in H);need(min(expanded_hist)>=6,'bothJ cross floor') + need(rho(E[0]+E[15]+E[16],E[0]+E[15]+E[16])==7,'residual rank') + # Induction on subset size: start with zero, repeatedly add each generator. + # Closure of the resulting set proves every component-support span is present. + allspaces={()};pending=[()] + while pending: + a=pending.pop() + for b in base: + z=basis(a+b) + if z not in allspaces:allspaces.add(z);pending.append(z) + need(len(allspaces)==40,'forty-space closure') + closure_premises(allspaces,base) + controls=[rejects(lambda:closure_premises(allspaces-{H[0]},base),'drop paired-space generator')] + derived=next(x for x in allspaces if len(x)==8 and x not in base) + controls.append(rejects(lambda:closure_premises(allspaces-{derived},base),'drop generated non-seed span')) + closures={a:tuple(i for i,b in enumerate(base) if basis(a+b)==a) for a in allspaces} + rectangles=Counter();selection_discounts=[] + for a in allspaces: + for b in allspaces: + A=closures[a];B=closures[b] + if not any(i<18 for i in A) or not any(i<18 for i in B):continue + rank=rho(a,b) + if rank>=6:continue + need(rank in (4,5),'low nonpure rank') + need(not set(A)&set(B),'disjoint rectangle supports') + probability=Fraction(1,math.comb(len(A)+len(B),len(A))) + need(Fraction(6-rank)<=4*probability,'acyclic discount inequality') + rectangles[(len(A),len(B),rank)]+=1 + selection_discounts.append({'left':A,'right':B,'rank':rank,'probability':str(probability)}) + expected={(1,1,4):20,(1,1,5):178,(1,2,5):33,(2,1,5):33,(1,3,5):4,(3,1,5):4} + need(dict(rectangles)==expected,'exact cheap-rectangle census') + # Beyond s=27 the increasing second line is >=309; no unbounded scan needed. + bounds=[max(334-s,228+3*s) for s in range(28)] + need(min(bounds)==308 and bounds.index(308)==26 and 228+3*27==309,'integer floor308') + need(Fraction(308)>Fraction(2672,9),'zero-saving gate rejected') + out={'candidate_lf_sha256':CANDIDATE_SHA,'payload_sha256':PAYLOAD_SHA,'generated_spaces':40,'seed_spaces':base,'span_closure':sorted(allspaces,key=lambda x:(len(x),x)),'controls':controls, + 'space_dimension_histogram':dict(sorted(Counter(map(len,allspaces)).items())), + 'paired_space_pairing_histogram':dict(sorted(pair_hist.items())), + 'J_enlarged_pairing_histogram':dict(sorted(expanded_hist.items())), + 'pureJ_pairing_rank':3,'low_rectangles':{str(k):v for k,v in sorted(rectangles.items())}, + 'bound':'C >= max(334-s,228+3s) >= 308','integer_minimizer_s':26, + 'scope':'Rank57 fitting matrix; BOTH factor sides retained in its canonical row/column spaces; m=57+s nonzero scalar terms. Exterior-factor and higher-rank fits excluded.'} + print(json.dumps(out,sort_keys=True)) + print('PASS_P112_CANONICAL_SPAN_COST_FLOOR_308') +if __name__=='__main__':main() From 51df1d4d05d0747cec9ab3b7bf90f62cd50997f0 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 23:01:44 +0200 Subject: [PATCH 13/22] Include scoped rational decoder cost floors in README.md --- research/p112-rational-decoder-gate/README.md | 42 +++++++++++++++++-- 1 file changed, 38 insertions(+), 4 deletions(-) diff --git a/research/p112-rational-decoder-gate/README.md b/research/p112-rational-decoder-gate/README.md index 0390229996..7335d1b143 100644 --- a/research/p112-rational-decoder-gate/README.md +++ b/research/p112-rational-decoder-gate/README.md @@ -1,8 +1,8 @@ -# A changed P112 three-plane cover with exact scalar fitting rank 57 +# A P112 cover with minimum scalar rank 57 and sharp minimum-length cost 334 **Constructive finite result and cost audit; no new supplier or kappa.** For the same 112 selected labels used by PR2041, this package supplies a different cover by 37 orthonormal triads and one residual line. Its strict scalar endpoint mask has minimum fitting rank **exactly 57**, with an explicit 57-term integral fit and a matching principal-submatrix lower bound. For the fixed cover in PR2041, PR2532 identified a rank-at-least-99 obstruction; this package also supplies a matching 99-term fit. Thus the exact fixed-mask minimum changes from **99 to 57** when the cover changes. This opens more scalar sharing without reusing the invalid binary decoder target. -This is a partial result toward a rational decoder. Charging the full port spaces gives the displayed fit the profile `3 H3 + 53 H6 + H7`, of mass **334**. Even with the proposed coverage law and all additional costs set to zero, its zero-saving moment is **32871/32704 > 1**. Rational diagonal rescaling preserves the fit but does not reduce that bill. The number 57 counts rank-one scalar terms; it is not a verified number of physical child calls. +This is a partial result toward a rational decoder. Charging the full port spaces gives the displayed fit the profile `3 H3 + 53 H6 + H7`, of mass **334**. Even with the proposed coverage law and all additional costs set to zero, its zero-saving moment is **32871/32704 > 1**. A follow-up theorem proves that **every exactly-57-term rational fit on this mask costs at least 334**, including asymmetric factors and arbitrary nonzero common normalization. Moreover, at **any factor count**, a rank-57 fit costs at least **308** if both factor families remain in its column and row spaces. Both floors exceed the necessary charge of at most 296. The number 57 counts rank-one scalar terms; it is not a verified number of physical child calls. ## Exact object and contract @@ -56,7 +56,7 @@ Here both spans are equal. Each ordinary pair support touches two orthogonal non n_3=3,\qquad n_6=53,\qquad n_7=1,\qquad C=3\cdot3+53\cdot6+7=334. \] -This remains true after any diagonal conjugation above. It prices these factors; it is not a lower bound for arbitrary rational decoders under this mask. The integral construction does not evade the earlier 2-integral floor of 334 for this 37-triad/one-line contract. +This remains true after any diagonal conjugation above. The [minimum-length cost theorem](RANK-TIGHT-PROOF.md) extends this floor to every exactly-57-term rational scalar fit on this mask. This 334 bound does not bound decompositions with more terms, including overcomplete decompositions of rank-57 matrices. The additional 308 bound below has a different scope. The integral construction does not evade the earlier 2-integral floor of 334 for this 37-triad/one-line contract. The exact average unpaid dimension is @@ -81,6 +81,37 @@ M(0)=\frac{5522+C+I}{73w} Every child rank is below 73, so `(r/73)^(1-a)` is nondecreasing for `a>=0`. Failure at zero rules out positive saving for the displayed profile before extra costs. This conditional screen does not establish a native implementation of the coverage law. Its necessary centre budget for any positive saving is `C < 2672/9`, hence `C<=296` for an integer invoice. Reaching the selected saving requires a substantially smaller bill, around 261 even under favorable rank-1-through-9 packing; PR2532's incumbent-tie screen is planning context, not a feasibility certificate. +## Sharp cost floor for every minimum-length rational fit + +The follow-up starts from canonical main `936fac15b1b1b59dc5285c713a77f9f3c07b2906` +and pins the published construction at PR2757 head +`c8216fca1ed2a301a95e7e0b1e5844d4cfda02c6`. Its source inputs are unchanged. + +[RANK-TIGHT-PROOF.md](RANK-TIGHT-PROOF.md) proves a sharp floor of 334 for +**exactly 57 nonzero rational rank-one terms**, over all fitting matrices on +this fixed mask. The principal identity forces a zero Schur complement. Two +additional forbidden blocks eliminate the exceptional couplings, leaving 18 +inverse paired blocks, the isolated final triad and the residual line. +Biorthogonality and 324 checked support-pairing ranks then force every term to +cost at least six, except at most three terms costing three. The residual +diagonal requires a separate term costing at least seven. Hence the total is +at least `54*6 + 3*3 + 1 = 334`, attained by the saved construction. + +The argument does not reduce rational coefficients modulo two and covers +nonintegral, nonsymmetric and nongauge factorizations. It closes optimization +at minimum factor count. For any number `m=57+s` of terms, an additional argument gives +`C >= max(334-s, 228+3s) >= 308` if both factor families remain in the rank-57 +matrix's column and row spaces. An exact closure of 40 binary component spaces +bounds the support patterns of discounted terms; an acyclic-subset argument +then bounds how many discounts the extra factors can buy. The floor 308 is a +lower bound, with no claim that it is attainable. + +Thus **more factors and a change of span or fitting rank are necessary for +charge <=296**, not sufficient. Exterior factor directions may cancel in the +sum, and fitting matrices of larger rank remain open. Changed covers and +operator contracts also remain open. Neither theorem establishes physical +implementation or an improved multiplication bound. + ## Discovery and replay Discovery optimized the actual free mask. A bounded randomized exact-cover search, seed `2026101501`, packed orthogonal six-label sets and split each into two triads, obtaining 17 disjoint orthogonal triad pairs. A local repair, seed `2026101502`, repacked 22 ports: two six-label blocks plus ten remaining ports became three six-label blocks, one triad and one line. This produced the 18-pair cover. Attaching the residual line as above gives rank 57. @@ -92,6 +123,9 @@ From the repository root, standard library only: ```sh python3 -I -O -B research/p112-rational-decoder-gate/verify.py python3 -I -O -B research/p112-rational-decoder-gate/independent_check.py +python3 -I -O -B research/p112-rational-decoder-gate/check_rank_tight_floor.py +python3 -I -O -B research/p112-rational-decoder-gate/independent_cost_floor.py +python3 -I -O -B research/p112-rational-decoder-gate/check_overcomplete_closure.py python3 scripts/research_package.py --package research/p112-rational-decoder-gate --check-only python3.12 scripts/research_package.py --package research/p112-rational-decoder-gate ``` @@ -112,5 +146,5 @@ Prepared by flyingviper with substantial OpenAI Codex assistance in search, proo ## Open next questions -1. **Can a different rational factorization exploit this mask to lower the full port-space bill?** Start with asymmetric factors, possibly more than 57 terms and mixing different orthogonal pairs. Enforce every diagonal and forbidden entry exactly before pricing whole source and reader spaces. A useful first gate is `C < 2672/9`; a selected-bound candidate needs a full moment below one near the incumbent saving, requiring roughly `C<=261` even in the favorable rank-9 relaxation. Stop a factorization family when its favorable complete invoice misses that gate. Diagonal rescaling of the saved factors costs 334 and does not reopen it. +1. **Can a different rational factorization exploit this mask to lower the full port-space bill?** Start with at least 58 nonzero terms, and either introduce factor directions outside the fitting matrix's column/row spaces or increase the fitting rank. The cost theorems exclude every exactly-57-term rational fit and all overcomplete decompositions of rank-57 fitting matrices that retain both spans, including asymmetric ones. Enforce every diagonal and forbidden entry exactly before pricing whole source and reader spaces. A useful first gate is `C < 2672/9`; a selected-bound candidate needs a full moment below one near the incumbent saving, requiring roughly `C<=261` even in the favorable rank-9 relaxation. Stop a factorization family when its favorable complete invoice misses that gate. Diagonal rescaling of the saved factors costs 334 and does not reopen it. 2. **Can a different block or native contract realize useful sharing with every independent payload charged?** First supply the complete operator identity, dirty-input behavior and actual occurrences, rather than charging a geometric rank once for a multi-array block. Before another construction round, update the family budget and consumer boundary: source preparation, chart conversion, routing, hosting, chronological ownership, storage, erasure/restoration, precision, all-size recursion and a compatible bit supplier remain unproved here. Their costs are unknown, not zero. This finite certificate supplies neither physical compilation nor the selected cold replay. From 54b04dcbe6b072d1fc0c42807650da22eff3fe55 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 23:01:50 +0200 Subject: [PATCH 14/22] Include scoped rational decoder cost floors in TASK.json --- research/p112-rational-decoder-gate/TASK.json | 65 +++++++++++++++++-- 1 file changed, 58 insertions(+), 7 deletions(-) diff --git a/research/p112-rational-decoder-gate/TASK.json b/research/p112-rational-decoder-gate/TASK.json index 9845ce4639..3128432e6a 100644 --- a/research/p112-rational-decoder-gate/TASK.json +++ b/research/p112-rational-decoder-gate/TASK.json @@ -45,21 +45,21 @@ ] }, "scope_status": "changed", - "actual_scope": "Construct and independently certify a changed 37-triad/one-line P112 mask with exact scalar fitting rank57, compare the old rank99 mask, and fully price the explicit scalar factors.", + "actual_scope": "Construct and independently certify a changed 37-triad/one-line P112 mask with exact scalar fitting rank57, compare the old rank99 mask, and fully price the explicit scalar factors. Prove the sharp334 whole-port-space floor for every exactly57-term rational fit on the changed mask. Prove a308 lower bound for any-length decompositions of rank57 fits whose factors retain both column/row spans.", "scope_change_reason": "User selected rational/block P112 decoder research after PR2532 invalidated the original binary lift. The old cover obstructs natural fractional routes; change the cover to expand actual orthogonal-group freedom instead of optimizing the invalid binary invoice.", - "bottleneck_link": "Provides a correct lower-rank scalar mask benchmark for cross-group fractional decoding. The explicit334 copy bill still fails the favorable coverage screen, so no native implementation campaign or improved bound is claimed.", + "bottleneck_link": "The changed cover attains scalar rank57, but every57-term fit costs334. At any factor count, rank57 fits retaining both factor spans cost at least308. Both exceed2672/9, so successful scalar sharing must use exterior factor directions or higher fitting rank.", "budget_minutes": 60, "stop_rule": "Retain one verified mask/cost result after exact endpoint and independent checks. Reject the explicit supplier target at zero saving; do not infer a universal rational-decoder or cover obstruction from bounded motif searches.", "outcome": "partial", - "evidence": "CANDIDATE.json, exact identity-minor and disjoint-support proof in README, primary RESULT.json and independently implemented checker. Both original and new masks are certified.", + "evidence": "CANDIDATE.json, exact identity-minor and disjoint-support proof in README, primary RESULT.json and independently implemented checker. Both original and new masks are certified. RANK-TIGHT-PROOF.md plus two independent finite-premise/fixture checkers establish the scoped minimum-length cost floor. Independently implemented40-space closures support the additional any-length, both-spans cost theorem.", "author": "flyingviper (with OpenAI Codex)", "ai_assistance": "Substantial OpenAI Codex assistance in algebra, search, implementation, writing and testing. Three AI agents split independent scalar checks, cost/mask research, and fractional/operator exploration. No independent human or proof-assistant review is claimed.", "open_questions": [ { "question": "Can a genuinely shared fractional decoder improve the new mask's334 port-space charge?", "why_it_matters": "The scalar rank obstacle has fallen99 to57, but break-even requires C<2672/9 and the selected-target optimistic allowance is smaller.", - "first_step": "Give explicit rational source/reader factors across distinct paired components, check every constrained coefficient, then price all full port-space support pairings before native work.", - "blocked_by": "The supplied indicator fit and its rational diagonal gauges have charge334. No favorable full bill or actual native word is supplied." + "first_step": "Use at least58 terms and exterior factor directions or a higher-rank fitting matrix. Check every constrained coefficient, then price complete group-space pairings.", + "blocked_by": "The exact57-term floor is334; at arbitrary term count, rank57 fits retaining both canonical factor spans cost at least308. Exterior directions and higher fitting ranks remain open." }, { "question": "Can a different mask or operator contract supply genuinely cheaper payload transport?", @@ -99,7 +99,7 @@ }, "family_gate": { "decision": "narrow", - "proved": "Exact minimum scalar fitting rank57 for the new mask, rank99 comparison, complete334 port-space charge of the displayed factors, and failure of the favorable coverage screen already at a=0.", + "proved": "Exact minimum scalar fitting rank57 for the new mask, rank99 comparison, complete334 port-space charge of the displayed factors, and failure of the favorable coverage screen already at a=0. Sharp334 floor for all exactly57-term rational fits on this mask. Any-length rank57 decompositions retaining both factor spans cost at least308.", "unknown": [ "native caller", "routes and chronological ownership", @@ -109,7 +109,7 @@ "all-size admission", "bit-side transfer" ], - "next": "A cross-component rational/operator identity with a favorable fully charged budget; no expansion into physical construction for the supplied334-cost fit." + "next": "An explicit rational fit with exterior factor directions or higher fitting rank, with full-group charge<=296; no physical expansion before that screen." }, "validation": { "environment": "3.12.14", @@ -117,5 +117,56 @@ "independent": "independent_check.py -I -O -B", "formal_kernel": false, "human_review": false + }, + "cost_followup": { + "task_id": "coverage-law-change", + "scope_status": "changed", + "base_commit": "936fac15b1b1b59dc5285c713a77f9f3c07b2906", + "priority_revision": 5, + "dependency_pr": 2757, + "dependency_head": "c8216fca1ed2a301a95e7e0b1e5844d4cfda02c6", + "candidate_sha256": "dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b", + "selected_by": "Explicit user choice: cheaper rational decoder sharing across paired groups", + "target": "Exact fit of fixed changed triad mask with full group-space pairing charge <=296; this is only a zero-saving screen, not incumbent improvement", + "decision": "Retain both scoped obstructions in existing focused PR2757; narrow constructive work to exterior directions or higher-rank fitting matrices.", + "baseline": "Published source-bound rank57 fit cost334, independently reproduced, pending maintainer review", + "boundary": "112 scalar data ports, full source/target group spaces; all diagonal coefficients1 and forbidden off-diagonals0; free off-diagonals algebraically corrected without claiming native realization", + "proved_costs": { + "published_factor_copy_mass": 334, + "break_even": "2672/9", + "all_exactly_57_term_fits_minimum": 334, + "any_length_both_canonical_spans_lower_bound": 308 + }, + "unknown_costs": [ + "source preparation", + "native scalar scheduling and hosting", + "routing", + "dirty cleanup", + "storage", + "precision", + "all-size recursion", + "bit supplier transfer" + ], + "next_test": "At least58 terms with exterior factor directions, or a higher-rank fitting matrix. Both-canonical-span families fail the zero-saving gate.", + "stop_rule": "One bounded research session; retain an exact new construction or decision-changing obstruction, otherwise concise negative search handoff. Do not represent a bounded search as a universal barrier.", + "overlap": { + "open_pr_snapshot": "2026-10-15T20:57:50Z", + "scope": "latest100 updated open PR bodies, current-main notes and earlier pinned PR2532; no overlapping same-mask cost theorem found in bounded coverage", + "limitation": "Live discussion refresh stopped at HTTP406 after discussion1587; remaining cached Discussions from20:19UTC. No retry/bypass.", + "nearest": [ + "PR2757 (own starting point)", + "PR2532 strict mask/cost audit", + "PR2484 other-mask rank49", + "PR2277 rank-T root-code floors, different contract", + "PR2724 nine-term rank8 realization, different contract" + ] + }, + "started_at_utc": "2026-10-15T20:42:04.228659+00:00", + "upstream_refresh": { + "checked_at_utc": "2026-10-15T20:57:50Z", + "canonical_main": "8e22a9d9f621c72ab5b299061c2be4c7f638fd3c", + "priority_revision": 5, + "decision": "Fast-forwarded isolated follow-up worktree; guidance, selected record and consumed inputs unchanged. Updated registered runner replayed. Existing PR retains construction source pins." + } } } From 1c7bdd4575137b3334adb185ec8f7efb63584b9e Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 23:01:56 +0200 Subject: [PATCH 15/22] Include scoped rational decoder cost floors in VERIFY.json --- .../p112-rational-decoder-gate/VERIFY.json | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/research/p112-rational-decoder-gate/VERIFY.json b/research/p112-rational-decoder-gate/VERIFY.json index f094cbbe87..642d4f7127 100644 --- a/research/p112-rational-decoder-gate/VERIFY.json +++ b/research/p112-rational-decoder-gate/VERIFY.json @@ -29,6 +29,39 @@ ], "timeout_seconds": 120, "checks": "Independent source-bound reconstruction with a distinct elimination method; both exact ranks, every rational endpoint coefficient and dirty source column; nine controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/check_rank_tight_floor.py" + ], + "timeout_seconds": 120, + "checks": "Source-bound finite premises of the written57-term cost theorem: Schur mask, all324 enlarged pairings, residual and false-generalization control. Does not formally check the symbolic proof. Also reconstruct all40 component spans using explicit binary vector sets and certify the308 floor premises." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent_cost_floor.py" + ], + "timeout_seconds": 120, + "checks": "Independent binary elimination and exact rational fixtures, including dense even denominators, whole-group pricing, and four semantic mutation controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/check_overcomplete_closure.py" + ], + "timeout_seconds": 120, + "checks": "Independent exact40-space closure using echelon tuples; all272 discounted rectangles, sampling inequality, missing-seed and missing-generated-span controls. Supports written both-canonical-spans proof, not unrestricted decoders." } ] } From 79eb698c7a59d98ca740823896ec5904ecedef20 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 23:32:48 +0200 Subject: [PATCH 16/22] Prove P112 cost floor for every decoder with at most 58 terms --- .../EXTERIOR-58-PROOF.md | 274 ++++++++++++++++++ 1 file changed, 274 insertions(+) create mode 100644 research/p112-rational-decoder-gate/EXTERIOR-58-PROOF.md diff --git a/research/p112-rational-decoder-gate/EXTERIOR-58-PROOF.md b/research/p112-rational-decoder-gate/EXTERIOR-58-PROOF.md new file mode 100644 index 0000000000..eb02557539 --- /dev/null +++ b/research/p112-rational-decoder-gate/EXTERIOR-58-PROOF.md @@ -0,0 +1,274 @@ +# Exterior-factor floor for decoders with at most 58 scalar terms + +Fix the full-group scalar mask and physical tariff of this package's changed +P112 cover. The candidate's normalized LF SHA256 is +`dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b`. + +**Theorem.** Every rational fitting decoder expressed using at most 58 nonzero +scalar rank-one terms has total full-group port-space charge at least 297. +Consequently it cannot meet the necessary positive-saving allowance +`C < 2672/9`, equivalently integer `C <= 296`. This bound is not claimed sharp. +A successful scalar decoder on this mask therefore needs at least 59 terms. + +The theorem permits arbitrary rational denominators and exterior factor +components. It covers fitting matrices of either possible rank, 57 or 58. +It does not cover 59 or more terms, changed covers, block-valued messages, or +changed tariffs, and proves no native supplier or exponent improvement. + +The [preceding proof](RANK-TIGHT-PROOF.md) establishes the principal identity +minor of order 57 and the sharp charge 334 for exactly 57 terms. Fewer than +57 terms are impossible. It therefore remains to prove the claim for 58 terms. +We use its 40-space tariff lemma, but impose neither of its canonical-span +hypotheses on the original 58-term factors. + +## Setup and a compression lemma + +Normalize the fitting diagonal to one, which changes no supports or tariffs. +Let I contain all ports of odd groups G1,G3,...,G37, and let R contain the even +groups and the residual group G0. Write + + K = [ I57 A ] = U V^T, P=U_I, Q=V_I, P Q^T=I57. + [ B D ] + +The retained coordinates form 19 blocks of size three. For paired component i, +write `H_i=E_(2i-1)+E_(2i)`; write `J=E37`. Every term is charged using the sums +of all complete physical group spaces it touches. Ignoring residual support +can only lower that charge. + +Suppose dual blockwise coordinate maps produce a compressed identity of +dimension d, retain all three J coordinates, and have this property: any +nonzero compressed paired component forces its original physical factor to +touch the whole corresponding H_i. Components may retain one, two, or three +coordinates, or be deleted. Discard Z terms that become zero after compression. +The other `m'=58-Z` terms have excess `e=m'-d >= 0` over the identity's rank. + +The preceding 40-space lemma applies to these component supports regardless +of their internal dimensions. A pure term, with one compressed factor confined +to J, costs at least three; restricting the identity to its other d-3 coordinates +bounds their count by `Ppure <= e+3`. Nonpure terms cost at least four. If L4,L5 +count their actual charges four and five, the random-order, strictly triangular +subset argument gives `2 L4+L5 <= 4e`. This remains valid when actual charge five +has compressed tariff four: its selection probability is only larger. +Consequently + + C >= 6m' - 3Ppure - 2L4 - L5 + >= 6m' - 7e - 9 = 7d - 67 + Z >= 7d - 67. (1) + +No residual bonus is claimed. In particular, retaining d>=52 proves C>=297. +This is a dual compression of an identity, not necessarily a principal minor. + +## Rank-57 fits: one canonical factor side and one exterior direction + +If rank(K)=57, Sylvester's inequality gives +`rank(U)+rank(V) <= 57+58=115`. Both ranks are at least 57, so at least one +factor side has rank 57. Transpose if necessary and suppose rank(U)=57. +The preceding normal-form proof then gives + + D=BA, U=[P;BP], V=[Q;A^T Q+f z^T], + +where z spans the one-dimensional kernel of P and f is an arbitrary rational +55-vector. The last formula follows because every row of `V_R-A^T Q` lies in +ker(P). Also `Q^T P=I58-z w^T` for a vector w with `w^T z=1`. + +All paired maps in A,B are invertible inverse maps; the residual row and column +may use arbitrary vectors b,a with ba=1. No alignment of these vectors to a +coordinate is assumed. In paired component i, the reader blocks are + + q_i,t, M_i q_i,t+f_i z_t + +for an invertible M_i. Call t active when z_t is nonzero. Let F be the paired +components where f_i is nonzero; residual f_0 is unrestricted and excluded +from F. An active reader touches at least one complete triad in every pair F. + +For each i in F, delete the reader direction `M_i^-1 f_i` and one dual source +coordinate. A nonzero retained reader component cannot be canceled by the +exterior shift, so both physical triads remain touched. Source components +already touch both triads. This gives the compression hypothesis with +`d=57-|F|`; by (1), `C>=332-7|F|`. Thus |F|<=5 implies C>=297. + +### Finite geometry for six or more affected pairs + +Generate all binary spans of E1,...,E37, omitting the residual line. There are +exactly 1750, with dimension histogram + + {0:1, 3:37, 4:2, 5:59, 6:599, 7:657, 8:394, 9:1}. + +For each reader span T put + + M(T)={i: E_(2i-1) is contained in T or E_(2i) is contained in T}. + +The source-pinned checker proves: + +1. If |M(T)|>=6 then `rho(H_i,T)>=5` for every i and `rho(J,T)>=2`. +2. For any fixed subset F of at least six pairs, the union + + L(F)={i: some generated T has F subset M(T) and rho(H_i,T)<6} + + has size at most 10. The union is over **all** compatible reader spans for + the same F, not a separate bound for each reader. + +Only 121 reader spans have |M(T)|>=6 and a paired tariff below six. Enumerating +every subset F of their coverage sets gives 2318 nonempty F-to-L cases; all +omitted F have empty L(F). The maximum union size 10 occurs at +`F={1,4,7,11,12,14}`, with `L={1,4,5,6,7,8,10,11,13,18}`. +Closure under all 37 generators certifies completeness. Adding actual residual +support can only raise every tariff used here. + +### The large-F invoice + +Assume |F|>=6. An active term with a paired source component costs at least +five. If it costs below six, every paired component of its source lies in +L(F). Such source columns lie in a space of dimension at most `3*10+3=33`, +including J. Since P has nullity one, there are at most 34 such columns. + +For an inactive index, `q_t^T p_t=1` and its reader is canonical. The preceding +common-component argument gives tariff at least six unless the source or +reader is supported only in J. Let A be all pure-J source indices and B the +inactive pure-J reader indices. Put alpha=|A|, beta=|B|, gamma=|A intersect B|. +The rows `Q_B^T P` are the corresponding rows of I58, so Q_B consists of beta +independent vectors in J and its pairing on P_A has rank gamma. Also +`rank(P_A)>=alpha-1`. The annihilator of these beta independent covectors in J +has dimension 3-beta, giving + + alpha-1-gamma <= 3-beta, |A union B|<=4. + +Every exceptional term costs at least two: active pure-J sources use the +finite geometry lemma, and inactive ones cost three. Other than these four +possible exceptions and the 34 possible active cheap terms, every term costs +at least six. Thus + + C >= 6*58 - 34 - 4*4 = 298. (2) + +This finishes rank-57 fits. This argument also tolerates arbitrary additional +physical residual entries on the source side: they only raise the lower bounds. +The source columns used in the count must have nonzero retained vectors; a +possible zero retained column in the next case is handled separately below. + +## Rank-58 fits: a rank-one Schur complement + +Now rank(K)=58. Choose z spanning ker(P) and w spanning ker(Q), normalized by +`w^T z=1`. The projection `Q^T P` has image im(Q^T) and kernel ker(P), so this +normalization exists and + + Q^T P=I58-z w^T, + U_R=BP+g w^T, V_R=A^T Q+f z^T, + D=BA+g f^T. + +Both g and f are nonzero; their outer product is the rank-one Schur complement. +Here A,B have only the original mask restrictions. The rank-57 normal form is +not assumed. + +### The Schur-support forest + +A block `(BA)_ij` can be nonzero only when the R-groups i,j share an allowed +odd neighbor. A fitting off-diagonal block K_ij can be nonzero only when those +full group spaces are orthogonal. These two tests show that `(g f^T)_ij` must +vanish except on diagonal blocks and the following nine undirected edges: + + 0-2, 0-8, 0-10, 0-16, 0-20, 0-28, 4-24, 8-22, 12-30. + +This graph is a forest. If G and F are the nonzero group supports of g and f, +then G times F is a nonempty rectangle in the forest with loops. If both sets +have at least two vertices, they must both equal one edge's two endpoints: +two distinct vertices have at least two common closed neighbors only when +adjacent, and those neighbors are exactly the endpoints. Otherwise one set is +a singleton and the other is in its closed neighborhood. + +The checker enumerates all 314 ordered nonempty rectangles: 8 touch group4, +53 are ordinary, and 253 have one side supported only on residual group0. +The ordinary cases have at most four nonzero even blocks across g and f. +Only four rectangles have more than five: up to transposition, g is residual-only +and f touches all six even neighbors `{2,8,10,16,20,28}`, optionally also G0. + +### A local dual compression allowing singular paired maps + +For an ordinary paired block, suppose + + B_i A_i+g_i f_i^T=I3. + +Define its bad source and reader subspaces by + + X_i={p: B_i p lies in span(g_i)}, + Y_i={q: A_i^T q lies in span(f_i)}. + +If g_i=0, X_i is zero; otherwise `[B_i,g_i]` has row rank three by the identity, +so X_i has dimension one. Likewise Y_i has dimension zero or one according as +f_i is zero or nonzero. This works even when A_i or B_i is singular. + +The standard pairing between `X_i^perp` and `Y_i^perp` has rank at least +`3-dim(X_i)-dim(Y_i)`. Choose dual row maps L_i,R_i of that size, with +`L_i R_i^T=I`, whose kernels contain X_i,Y_i. A nonzero compressed source +`L_i p` cannot have its even block canceled by `g_i w_t`; a nonzero compressed +reader `R_i q` cannot be canceled by `f_i z_t`. Thus the compression implication +for the complete H_i holds. At most one coordinate is lost for each nonzero +even block of g and for each nonzero even block of f. + +### Ordinary and exceptional branches + +If neither g nor f touches group4, the diagonal at group4 gives +`B_4,3 A_3,4=I3`. Its maps are invertible; the forbidden 4/24 blocks, with zero +Schur corrections, force `A_3,24=B_24,3=0`. Every even group now has only its +matching odd contribution, so the local compression applies to every pair. +When at most five even blocks of g,f are nonzero, it retains d>=52, proving +C>=297 by (1). Residual row and column formulas are irrelevant to this estimate. + +If either g or f touches group4, the forest rectangle property puts both +supports inside `{4,24}`. This includes a Schur complement supported only on +the diagonal block4, where its maps can be singular. Do not discard the extra +odd3/group24 couplings. Instead delete all three odd23 coordinates, and apply +the local compression to odd3/group4, which still has only its matching odd +neighbor and satisfies `B_4,3 A_3,4+g_4 f_4^T=I3`. This loses at most two more +coordinates. Every other pair retains all three, and J retains three; again +d>=52. Any group24 support of the surviving factors only increases cost. + +### The residual-only six-neighbor branch + +The only remaining case has, up to transposition, g residual-only and f nonzero +in all six even neighbors of G0. Every paired A_i,B_i is now invertible and the +4/24 extra coupling is zero. Sources touch both triads exactly when their +retained paired component is nonzero; their residual entries may be arbitrary. + +If no retained source column is zero, the large-F argument (2) applies and +gives C>=298. It used only these paired support implications, the identity +`P Q^T=I57`, and the unique reader shift; additional source residual support +cannot lower its tariff estimates. + +If a retained source column is zero, there is exactly one, because P has rank +57 and 58 columns. Then z is supported only on that index. The other 57 retained +source/reader columns are square dual bases, with canonical paired physical +supports. Ignoring all residual entries, the preceding 57-term argument allows +at most three pure-J exceptions of cost at least three and has 54 other terms +of cost at least six. Their subtotal is 333; the last term has nonnegative +cost. This finishes rank-58 fits and the theorem. + +## Replay, limits, and credit + +Run from the repository root, using Python 3.12 standard library only: + +```sh +python3 -I -O -B research/p112-rational-decoder-gate/check_exterior_58.py +python3 -I -O -B research/p112-rational-decoder-gate/independent_exterior_58.py +``` + +The checker is read-only and prints JSON. It authenticates this candidate, +the selected replay archive and its payload, reconstructs the 1750 physical +reader spaces, enumerates all 2318 affected-set unions, and derives all 314 +Schur support rectangles directly from the original mask. Semantic controls +reject missing closure spaces, weakening whole-triad containment to nonzero +intersection, and adding an edge that destroys the Schur forest. Replay the +preceding [rank-tight checks](RANK-TIGHT-PROOF.md#replay-and-credit) as well for +the principal identity and 40-space acyclic lemma used here. + +A separate AI agent audited this proof and independently reconstructed the +finite geometry using explicit vector sets and annihilator-intersection ranks; +its Schur check independently enumerates all 314 rectangles. The two +implementations agree. These are scoped symbolic proofs supported by finite +checks, not proof-assistant +formalization or independent human review. + +The selected P112 labels, changed cover, strict mask and physical tariff retain +the predecessor attribution in the [README](README.md). Prepared by flyingviper +with substantial OpenAI Codex assistance and separate AI-agent checking. New +work is Apache-2.0. The next constructive question remains a full-group scalar +decoder with at least 59 terms and charge at most 296, or a changed interface +outside this fixed scalar mask. From 097308dbf23bae083e49f87d3a546f3ca5e6c985 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 23:33:17 +0200 Subject: [PATCH 17/22] Check P112 exterior-factor geometry and Schur support forest --- .../check_exterior_58.py | 281 ++++++++++++++++++ 1 file changed, 281 insertions(+) create mode 100644 research/p112-rational-decoder-gate/check_exterior_58.py diff --git a/research/p112-rational-decoder-gate/check_exterior_58.py b/research/p112-rational-decoder-gate/check_exterior_58.py new file mode 100644 index 0000000000..d1c40b97e8 --- /dev/null +++ b/research/p112-rational-decoder-gate/check_exterior_58.py @@ -0,0 +1,281 @@ +#!/usr/bin/env python3 +"""Read-only finite premises for the full-group exterior 58-term cost floor. + +F2 is used only for physical group spaces and tariffs. Rational decoder +coefficients are never reduced modulo two. Standard library only. +""" +from collections import Counter +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path +import tarfile + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +CANDIDATE_SHA = 'dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b' +ARCHIVE_SHA = 'f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6' +PAYLOAD_SHA = 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa' +MEMBER = 'candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def basis(vectors): + pivots = {} + for vector in vectors: + while vector: + column = vector.bit_length() - 1 + if column in pivots: + vector ^= pivots[column] + else: + pivots[column] = vector + break + for column in sorted(pivots): + for higher in pivots: + if higher > column and ((pivots[higher] >> column) & 1): + pivots[higher] ^= pivots[column] + return tuple(pivots[column] for column in sorted(pivots)) + + +def rho(left, right): + rows = [sum(((x & y).bit_count() % 2) << j + for j, y in enumerate(right)) for x in left] + return len(basis(rows)) + + +def contained(small, large): + return basis(small + large) == large + + +def rejected(action, label): + try: + action() + except ValueError: + return label + raise ValueError('negative control accepted: ' + label) + + +def load_spaces(): + candidate = (PACKAGE / 'CANDIDATE.json').read_bytes().replace(b'\r\n', b'\n') + need(sha256(candidate).hexdigest() == CANDIDATE_SHA, 'candidate pin') + groups = json.loads(candidate)['groups'] + archive = ROOT / 'research/community-frontier1094-audit/selected-replay.tar.gz' + need(sha256(archive.read_bytes()).hexdigest() == ARCHIVE_SHA, 'archive pin') + with tarfile.open(archive) as stream: + payload = stream.extractfile(MEMBER).read() + need(sha256(payload).hexdigest() == PAYLOAD_SHA, 'payload pin') + recipes = sorted(json.loads(payload)['recipes'], key=lambda row: row['port']) + need([row['port'] for row in recipes] == list(range(112)), 'port order') + labels = [row['q'] for row in recipes] + need(sorted(port for group in groups for port in group) == list(range(112)), + 'complete group partition') + raw_spaces = [tuple(labels[port] for port in group) for group in groups] + need(len(groups) == 38 and len(groups[0]) == 1 + and all(len(group) == 3 for group in groups[1:]), 'one line and37 triads') + need(all((x & y).bit_count() % 2 == (i == j) + for group in raw_spaces for i, x in enumerate(group) + for j, y in enumerate(group)), 'orthonormal physical groups') + return [basis(group) for group in raw_spaces] + + +def check_closure(spaces, seeds): + need(() in spaces and all(seed in spaces for seed in seeds), 'missing generator') + need(all(basis(space + seed) in spaces for space in spaces for seed in seeds), + 'not closed under physical triad generators') + + +def check_large_coverage(spaces, coverage, paired, singleton): + for space in spaces: + if len(coverage[space]) >= 6: + need(all(rho(component, space) >= 5 for component in paired), + 'six affected pairs require paired tariff at least5') + need(rho(singleton, space) >= 2, + 'six affected pairs require J tariff at least2') + + +def reader_geometry(physical): + paired = [basis(physical[2*i+1] + physical[2*i+2]) for i in range(18)] + singleton = physical[37] + need(all(len(space) == rho(space, space) == 6 for space in paired), + 'paired spaces are nondegenerate of rank6') + seeds = physical[1:] + spaces, pending = {()}, [()] + while pending: + space = pending.pop() + for seed in seeds: + larger = basis(space + seed) + if larger not in spaces: + spaces.add(larger) + pending.append(larger) + check_closure(spaces, seeds) + need(len(spaces) == 1750, 'complete physical reader closure has1750 spaces') + dimension_histogram = Counter(map(len, spaces)) + need(dict(dimension_histogram) == {0:1, 3:37, 4:2, 5:59, 6:599, 7:657, 8:394, 9:1}, + 'exact reader-space dimension histogram') + controls = [rejected(lambda: check_closure(spaces - {physical[1]}, seeds), + 'missing physical triad generator')] + generated = next(space for space in spaces if len(space) == 8) + controls.append(rejected(lambda: check_closure(spaces - {generated}, seeds), + 'missing generated eight-space')) + + # Every active reader must touch at least one full triad of each affected + # pair. Containment in its physical span is necessary, not merely overlap. + coverage = {space: tuple(i for i in range(18) + if contained(physical[2*i+1], space) + or contained(physical[2*i+2], space)) for space in spaces} + check_large_coverage(spaces, coverage, paired, singleton) + weak_coverage = {space: tuple(i for i in range(18) + if len(basis(space + physical[2*i+1])) + < len(space) + 3 + or len(basis(space + physical[2*i+2])) + < len(space) + 3) for space in spaces} + controls.append(rejected(lambda: check_large_coverage( + spaces, weak_coverage, paired, singleton), + 'replacing whole-triad containment with nonzero intersection')) + + # OR across ALL reader spans compatible with the SAME affected set F. + # Every absent F has an empty union: its appearance would require one of + # the eligible readers enumerated here and would have been generated. + allowed, eligible = {}, 0 + for space in spaces: + covered = coverage[space] + if len(covered) < 6: + continue + source_mask = sum(1 << i for i, component in enumerate(paired) + if rho(component, space) < 6) + if not source_mask: + continue + eligible += 1 + for size in range(6, len(covered) + 1): + for affected in combinations(covered, size): + affected_mask = sum(1 << i for i in affected) + allowed[affected_mask] = allowed.get(affected_mask, 0) | source_mask + need(eligible == 121 and len(allowed) == 2318, 'eligible reader and affected-set census') + need(max(mask.bit_count() for mask in allowed.values()) == 10, + 'uniform cheap-source union has at most10 paired components') + histogram = Counter((affected.bit_count(), sources.bit_count()) + for affected, sources in allowed.items()) + expected = {(6,1):308, (6,2):765, (6,3):243, (6,4):170, (6,5):28, + (6,6):24, (6,7):7, (6,8):1, (6,9):2, (6,10):1, + (7,1):103, (7,2):351, (7,3):85, (7,4):39, (7,5):3, + (7,6):7, (7,7):1, (8,1):21, (8,2):108, (8,3):19, + (8,4):4, (8,6):1, (9,1):2, (9,2):21, (9,3):2, (10,2):2} + need(dict(histogram) == expected, 'exact affected-set/source-union histogram') + table = [{'F': affected, 'L': sources} for affected, sources in sorted(allowed.items())] + table_digest = sha256(json.dumps(table, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + need(table_digest == 'fdcf97070f3a70f994651dcfa81bd7d87757d266b6c1e7c6d969f31d5aed24ae', + 'exact affected-set union table agrees with independent certificate') + worst = next(affected for affected, sources in allowed.items() + if sources.bit_count() == 10) + return {'reader_spaces': len(spaces), + 'dimension_histogram': dict(sorted(dimension_histogram.items())), + 'eligible_reader_spans': eligible, 'nonempty_affected_set_unions': len(allowed), + 'maximum_cheap_source_pair_union': 10, + 'affected_set_union_table_sha256': table_digest, + 'affected_size_source_union_size_histogram': { + str(key): value for key, value in sorted(histogram.items())}, + 'worst_affected_pairs': [i+1 for i in range(18) if worst >> i & 1], + 'worst_source_pair_union': [i+1 for i in range(18) if allowed[worst] >> i & 1], + 'controls': controls} + + +def nonempty_subsets(vertices): + vertices = tuple(sorted(vertices)) + for mask in range(1, 1 << len(vertices)): + yield frozenset(vertices[i] for i in range(len(vertices)) if mask >> i & 1) + + +def check_forest(neighbors): + visited = set() + def visit(vertex, parent): + need(vertex not in visited, 'Schur graph contains a cycle') + visited.add(vertex) + for other in neighbors[vertex] - {vertex, parent}: + visit(other, vertex) + for vertex in neighbors: + if vertex not in visited: + visit(vertex, None) + + +def schur_geometry(physical): + remainder = [0] + list(range(2, 37, 2)) + retained = list(range(1, 38, 2)) + odd_neighbors = {i: {j for j in retained if rho(physical[i], physical[j]) == 0} + for i in remainder} + # Original K freedom OR a possible BA two-step path. No rank57 normal + # form is used when determining this rank58 Schur support restriction. + neighbors = {i: {j for j in remainder if i == j + or rho(physical[i], physical[j]) == 0 + or odd_neighbors[i] & odd_neighbors[j]} for i in remainder} + edges = sorted((i, j) for i in remainder for j in neighbors[i] if i < j) + expected = [(0,2), (0,8), (0,10), (0,16), (0,20), (0,28), + (4,24), (8,22), (12,30)] + need(edges == expected, 'exact nine-edge Schur support forest') + check_forest(neighbors) + mutated = {i: set(values) for i, values in neighbors.items()} + mutated[0].add(22) + mutated[22].add(0) + control = rejected(lambda: check_forest(mutated), + 'granting an extra0/22 Schur edge creates a triangle') + + # Every nonempty rectangle has a column vertex v, so its entire row set + # lies in N(v). Enumerating these row sets and every nonempty subset of + # their common column neighbors is a complete, deduplicated census. + left_sets = set() + for vertex in remainder: + left_sets.update(nonempty_subsets(neighbors[vertex])) + rectangles = set() + for left in left_sets: + common = set.intersection(*(neighbors[vertex] for vertex in left)) + for right in nonempty_subsets(common): + rectangles.add((left, right)) + classification, six_even = Counter(), [] + for left, right in rectangles: + if len(left) >= 2 and len(right) >= 2: + need(left == right and len(left) == 2, 'forest rectangle property') + even_count = len(left - {0}) + len(right - {0}) + if 4 in left or 4 in right: + need(left | right <= {4,24}, 'exceptional4/24 support localization') + classification['exceptional4/24'] += 1 + elif left == {0} or right == {0}: + need(even_count <= 6, 'residual-only six-neighbor limit') + classification['residual-only'] += 1 + if even_count == 6: + need((left - {0}) | (right - {0}) == {2,8,10,16,20,28}, + 'exact six-neighbor support') + six_even.append((sorted(left), sorted(right))) + else: + need(even_count <= 4, 'ordinary compression loses at most4 coordinates') + classification['ordinary'] += 1 + need(len(rectangles) == 314 and dict(classification) == { + 'exceptional4/24':8, 'ordinary':53, 'residual-only':253}, 'exact rectangle census') + need(len(six_even) == 4, 'four oriented six-even-block rectangles') + return {'edges': edges, 'nonempty_ordered_rectangles': len(rectangles), + 'classification': dict(sorted(classification.items())), + 'six_even_block_rectangles': sorted(six_even), 'controls': [control]} + + +def main(): + physical = load_spaces() + reader = reader_geometry(physical) + schur = schur_geometry(physical) + need(7 * 52 - 67 == 297 and 6 * 58 - 34 - 4 * 4 == 298, + 'compression and large-affected-support invoices') + need(297 * 9 > 2672, 'excludes the positive-saving allowance') + result = {'candidate_lf_sha256': CANDIDATE_SHA, 'archive_sha256': ARCHIVE_SHA, + 'payload_sha256': PAYLOAD_SHA, 'reader_geometry': reader, + 'schur_geometry': schur, 'lower_bound': 297, + 'scope': 'At most58 nonzero rational scalar rank-one terms on the pinned full-group mask; no sharpness claim.', + 'symbolic_proof': 'EXTERIOR-58-PROOF.md', + 'predecessor_premises': 'RANK-TIGHT-PROOF.md: principal I57 and40-space acyclic tariff lemma', + 'exclusions': ['59 or more terms', 'changed mask or tariff', + 'block-valued messages', 'native supplier or exponent claims']} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() From 57ea369d994f56f302ac1f190d12a72f1bb221d6 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 23:33:30 +0200 Subject: [PATCH 18/22] Independently verify the P112 58-term cost-floor premises --- .../independent_exterior_58.py | 232 ++++++++++++++++++ 1 file changed, 232 insertions(+) create mode 100644 research/p112-rational-decoder-gate/independent_exterior_58.py diff --git a/research/p112-rational-decoder-gate/independent_exterior_58.py b/research/p112-rational-decoder-gate/independent_exterior_58.py new file mode 100644 index 0000000000..902ee176ed --- /dev/null +++ b/research/p112-rational-decoder-gate/independent_exterior_58.py @@ -0,0 +1,232 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent exact finite checks for the at-most-58-term exterior floor. + +Subspaces are explicit sets of binary vectors; pairing ranks are calculated +through annihilator intersections. No primary/predecessor executable imports, +generated receipts, Git, third-party modules, or output-file writes are used. +The rational linear-algebra argument is in EXTERIOR-58-PROOF.md. +""" +from collections import Counter +from hashlib import sha256 +from itertools import combinations +from pathlib import Path +import io +import json +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +CANDIDATE_SHA = 'dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b' +ARCHIVE_SHA = 'f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6' +PAYLOAD_SHA = 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa' +MEMBER = 'candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def rejects(fn, message): + try: + fn() + except ValueError: + return message + raise ValueError('negative control accepted: ' + message) + + +def extend(space, vectors): + result = set(space) + for v in vectors: + if v not in result: + result.update([x ^ v for x in result]) + return frozenset(result) + + +def dimension(space): + n = len(space) + need(n > 0 and n & (n - 1) == 0, 'binary subspace cardinality') + return n.bit_length() - 1 + + +def perpendicular(space): + # Independent directions are extracted by vector-set membership. + generated = frozenset({0}) + directions = [] + for v in sorted(space): + if v not in generated: + directions.append(v) + generated = extend(generated, [v]) + need(generated == space, 'annihilator input span') + return frozenset(a for a in range(512) + if all((a & v).bit_count() % 2 == 0 for v in directions)) + + +def closure_check(spaces, seeds): + need(frozenset({0}) in spaces, 'missing zero space') + need(all(extend({0}, g) in spaces for g in seeds), 'missing generator') + need(all(extend(s, g) in spaces for s in spaces for g in seeds), + 'missing generated join') + + +def forest_check(neighbors): + need(all(v in neighbors[v] for v in neighbors), 'missing loop') + need(all(v in neighbors[u] for v in neighbors for u in neighbors[v]), + 'asymmetric support graph') + visited = set() + + def visit(v, parent): + need(v not in visited, 'support graph contains cycle') + visited.add(v) + for u in neighbors[v] - {v, parent}: + visit(u, v) + + for v in neighbors: + if v not in visited: + visit(v, None) + + +def main(): + raw = (HERE / 'CANDIDATE.json').read_bytes().replace(b'\r\n', b'\n') + need(sha256(raw).hexdigest() == CANDIDATE_SHA, 'candidate LF pin') + groups = json.loads(raw)['groups'] + archive = (ROOT / 'research/community-frontier1094-audit/selected-replay.tar.gz').read_bytes() + need(sha256(archive).hexdigest() == ARCHIVE_SHA, 'archive pin') + with tarfile.open(fileobj=io.BytesIO(archive), mode='r:gz') as source: + payload = source.extractfile(MEMBER).read() + need(sha256(payload).hexdigest() == PAYLOAD_SHA, 'payload pin') + recipes = sorted(json.loads(payload)['recipes'], key=lambda row: row['port']) + need([r['port'] for r in recipes] == list(range(112)), 'port order') + q = [r['q'] for r in recipes] + need(len(groups) == 38 and len(groups[0]) == 1 + and all(len(g) == 3 for g in groups[1:]), 'group dimensions') + need(sorted(i for g in groups for i in g) == list(range(112)), 'partition') + seeds = [[q[i] for i in g] for g in groups] + need(all((a & b).bit_count() % 2 == int(i == j) + for g in seeds for i, a in enumerate(g) for j, b in enumerate(g)), + 'orthonormal group bases') + E = [extend({0}, g) for g in seeds] + H = [extend(E[2*i+1], seeds[2*i+2]) for i in range(18)] + J = E[37] + need(all(dimension(h) == 6 and h & perpendicular(h) == {0} for h in H), + 'paired six-spaces') + + empty = frozenset({0}) + spaces, pending = {empty}, [empty] + while pending: + a = pending.pop() + for g in seeds[1:]: + s = extend(a, g) + if s not in spaces: + spaces.add(s) + pending.append(s) + closure_check(spaces, seeds[1:]) + need(len(spaces) == 1750, 'physical reader closure size') + expected_dimensions = {0: 1, 3: 37, 4: 2, 5: 59, 6: 599, 7: 657, 8: 394, 9: 1} + need(Counter(map(dimension, spaces)) == expected_dimensions, + 'reader dimension census') + controls = [rejects(lambda: closure_check(spaces - {E[1]}, seeds[1:]), + 'missing physical generator rejected')] + eight = next(s for s in spaces if dimension(s) == 8) + controls.append(rejects(lambda: closure_check(spaces - {eight}, seeds[1:]), + 'missing generated eight-space rejected')) + + allowed, eligible = {}, 0 + minimum_paired, minimum_J = 9, 9 + for T in spaces: + covered = [i for i in range(18) if E[2*i+1] <= T or E[2*i+2] <= T] + if len(covered) < 6: + continue + annihilator = perpendicular(T) + ranks = [dimension(h) - dimension(h & annihilator) for h in H] + jrank = dimension(J) - dimension(J & annihilator) + minimum_paired = min(minimum_paired, min(ranks)) + minimum_J = min(minimum_J, jrank) + need(min(ranks) >= 5 and jrank >= 2, 'large affected support tariff') + cheap_sources = sum(1 << i for i, r in enumerate(ranks) if r < 6) + if not cheap_sources: + continue + eligible += 1 + for n in range(6, len(covered) + 1): + for subset in combinations(covered, n): + f = sum(1 << i for i in subset) + allowed[f] = allowed.get(f, 0) | cheap_sources + need(eligible == 121 and len(allowed) == 2318, 'reader and affected-set census') + maximum_union = max(mask.bit_count() for mask in allowed.values()) + need(maximum_union == 10, 'uniform cheap-source union') + table = [{'F': f, 'L': allowed[f]} for f in sorted(allowed)] + table_hash = sha256(json.dumps(table, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + + def free(i, j): + return all((a & b).bit_count() % 2 == 0 for a in seeds[i] for b in seeds[j]) + + retained = list(range(1, 38, 2)) + outside = [0] + list(range(2, 37, 2)) + schur_edges = [] + neighbors = {i: {i} for i in outside} + for n, i in enumerate(outside): + for j in outside[n+1:]: + if free(i, j) or any(free(i, k) and free(k, j) for k in retained): + schur_edges.append([i, j]) + neighbors[i].add(j) + neighbors[j].add(i) + need(schur_edges == [[0, 2], [0, 8], [0, 10], [0, 16], [0, 20], [0, 28], + [4, 24], [8, 22], [12, 30]], 'exact Schur support graph') + forest_check(neighbors) + altered = {i: set(v) for i, v in neighbors.items()} + altered[0].add(22) + altered[22].add(0) + controls.append(rejects(lambda: forest_check(altered), + 'extra zero-to-22 edge creates rejected cycle')) + + # Any nonempty support rectangle has its row set within the closed + # neighborhood of any one column. Enumerate all such row sets, then every + # nonempty subset of their common columns: this covers all rectangles. + rowsets = set() + for adjacent in neighbors.values(): + adjacent = sorted(adjacent) + for n in range(1, len(adjacent) + 1): + rowsets.update(frozenset(c) for c in combinations(adjacent, n)) + rectangles, six_rectangles = Counter(), [] + for rows in rowsets: + columns = set(outside) + for i in rows: + columns.intersection_update(neighbors[i]) + need(bool(columns), 'rectangle common neighbors') + for n in range(1, len(columns) + 1): + for subset in combinations(sorted(columns), n): + cols = set(subset) + if len(rows) >= 2 and len(cols) >= 2: + need(rows == cols and len(rows) == 2, 'looped forest rectangle rule') + if 4 in rows or 4 in cols: + need(rows | cols <= {4, 24}, 'exceptional localization') + rectangles['exceptional4/24'] += 1 + elif rows == {0} or cols == {0}: + count = len(rows - {0}) + len(cols - {0}) + need(count <= 6, 'residual six-neighbor bound') + rectangles['residual-only'] += 1 + if count == 6: + need((rows | cols) - {0} == {2, 8, 10, 16, 20, 28}, 'six neighbors') + six_rectangles.append([sorted(rows), sorted(cols)]) + else: + need(len(rows - {0}) + len(cols - {0}) <= 4, 'ordinary compression bound') + rectangles['ordinary'] += 1 + need(rectangles == {'exceptional4/24': 8, 'residual-only': 253, 'ordinary': 53}, + 'complete ordered rectangle census') + need(len(six_rectangles) == 4, 'four six-neighbor rectangles') + print(json.dumps(dict(candidate_lf_sha256=CANDIDATE_SHA, archive_sha256=ARCHIVE_SHA, + payload_sha256=PAYLOAD_SHA, reader_spaces=len(spaces), + dimension_histogram=expected_dimensions, eligible_readers=eligible, + affected_sets=len(allowed), maximum_cheap_source_union=maximum_union, + allowed_table_sha256=table_hash, minimum_paired_tariff=minimum_paired, + minimum_J_tariff=minimum_J, schur_edges=schur_edges, + support_rectangles=sum(rectangles.values()), + rectangle_classification=dict(rectangles), + six_neighbor_rectangles=sorted(six_rectangles), controls=controls, + scope='Independent finite premises for the fixed-mask at-most-58-term scalar floor; no native or exponent claim.'), + sort_keys=True)) + + +if __name__ == '__main__': + main() From 07af3274a9aa784a7cb18443cc1b62a924bd0f7c Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 23:33:36 +0200 Subject: [PATCH 19/22] Document the P112 cost gate for all decoders with at most 58 terms --- research/p112-rational-decoder-gate/README.md | 46 +++++++++++++++++-- 1 file changed, 42 insertions(+), 4 deletions(-) diff --git a/research/p112-rational-decoder-gate/README.md b/research/p112-rational-decoder-gate/README.md index 7335d1b143..d3547cf2a8 100644 --- a/research/p112-rational-decoder-gate/README.md +++ b/research/p112-rational-decoder-gate/README.md @@ -2,7 +2,7 @@ **Constructive finite result and cost audit; no new supplier or kappa.** For the same 112 selected labels used by PR2041, this package supplies a different cover by 37 orthonormal triads and one residual line. Its strict scalar endpoint mask has minimum fitting rank **exactly 57**, with an explicit 57-term integral fit and a matching principal-submatrix lower bound. For the fixed cover in PR2041, PR2532 identified a rank-at-least-99 obstruction; this package also supplies a matching 99-term fit. Thus the exact fixed-mask minimum changes from **99 to 57** when the cover changes. This opens more scalar sharing without reusing the invalid binary decoder target. -This is a partial result toward a rational decoder. Charging the full port spaces gives the displayed fit the profile `3 H3 + 53 H6 + H7`, of mass **334**. Even with the proposed coverage law and all additional costs set to zero, its zero-saving moment is **32871/32704 > 1**. A follow-up theorem proves that **every exactly-57-term rational fit on this mask costs at least 334**, including asymmetric factors and arbitrary nonzero common normalization. Moreover, at **any factor count**, a rank-57 fit costs at least **308** if both factor families remain in its column and row spaces. Both floors exceed the necessary charge of at most 296. The number 57 counts rank-one scalar terms; it is not a verified number of physical child calls. +This is a partial result toward a rational decoder. Charging the full port spaces gives the displayed fit the profile `3 H3 + 53 H6 + H7`, of mass **334**. Even with the proposed coverage law and all additional costs set to zero, its zero-saving moment is **32871/32704 > 1**. A follow-up theorem proves that **every exactly-57-term rational fit on this mask costs at least 334**, including asymmetric factors and arbitrary nonzero common normalization. Moreover, at **any factor count**, a rank-57 fit costs at least **308** if both factor families remain in its column and row spaces. A further [exterior-factor theorem](EXTERIOR-58-PROOF.md) proves that **every rational fit using at most 58 nonzero rank-one terms costs at least 297**, whether its matrix rank is 57 or 58. These floors exceed the necessary charge of at most 296. The number 57 counts rank-one scalar terms; it is not a verified number of physical child calls. ## Exact object and contract @@ -106,12 +106,46 @@ bounds the support patterns of discounted terms; an acyclic-subset argument then bounds how many discounts the extra factors can buy. The floor 308 is a lower bound, with no claim that it is attainable. -Thus **more factors and a change of span or fitting rank are necessary for -charge <=296**, not sufficient. Exterior factor directions may cancel in the +Thus **at least 59 factors and a change of span or fitting rank are necessary for +charge <=296**, not sufficient; the 59-term necessity follows from the extension below. Exterior factor directions may cancel in the sum, and fitting matrices of larger rank remain open. Changed covers and operator contracts also remain open. Neither theorem establishes physical implementation or an improved multiplication bound. +## Exterior factors: every decoder with at most 58 terms misses the gate + +[EXTERIOR-58-PROOF.md](EXTERIOR-58-PROOF.md) closes both matrix-rank cases +possible with 58 terms. It permits arbitrary rational coefficients, asymmetric +factors, exterior directions that cancel, and changes of fitting matrix: + +\[ + m\le58\quad\Longrightarrow\quad C\ge297>2672/9. +\] + +This floor is not claimed sharp. For rank 57, Sylvester's rank inequality forces +one factor family to remain in the fitting matrix's span. The other has one +exterior direction. Compressing the affected coordinates handles a sparse +direction; a complete closure of **1,750 physical-triad spans** and **2,318 +affected-set unions** handles a dense direction. The key bound uses the union +of every compatible cheap-source support for the same affected set. + +For rank 58, the Schur complement has rank one. Its permitted group blocks +form a forest. All **314 nonempty support rectangles** localize the defect to +either a small compression, the exceptional groups 4/24, or a residual-only +six-neighbor case. The proof handles singular paired maps and a zero retained +source column explicitly. It invokes the prior 40-space acyclic cost argument +after compression; it does not reduce rational coefficients modulo two. + +The new [primary checker](check_exterior_58.py) and +[independent checker](independent_exterior_58.py) reconstruct these finite +premises using echelon bases and explicit vector sets, respectively. They do +not execute or import one another. Separate AI agents also audited the written +algebra. This is not independent human review or formal proof verification. + +Consequently the next scalar construction must use **at least 59 nonzero terms**, +and must still escape the earlier rank-57/both-spans floor. No cheaper decoder, +native implementation, or improved exponent is supplied by this obstruction. + ## Discovery and replay Discovery optimized the actual free mask. A bounded randomized exact-cover search, seed `2026101501`, packed orthogonal six-label sets and split each into two triads, obtaining 17 disjoint orthogonal triad pairs. A local repair, seed `2026101502`, repacked 22 ports: two six-label blocks plus ten remaining ports became three six-label blocks, one triad and one line. This produced the 18-pair cover. Attaching the residual line as above gives rank 57. @@ -126,6 +160,8 @@ python3 -I -O -B research/p112-rational-decoder-gate/independent_check.py python3 -I -O -B research/p112-rational-decoder-gate/check_rank_tight_floor.py python3 -I -O -B research/p112-rational-decoder-gate/independent_cost_floor.py python3 -I -O -B research/p112-rational-decoder-gate/check_overcomplete_closure.py +python3 -I -O -B research/p112-rational-decoder-gate/check_exterior_58.py +python3 -I -O -B research/p112-rational-decoder-gate/independent_exterior_58.py python3 scripts/research_package.py --package research/p112-rational-decoder-gate --check-only python3.12 scripts/research_package.py --package research/p112-rational-decoder-gate ``` @@ -140,11 +176,13 @@ The primary and separately implemented checker reconstruct labels, the cover, th - **Cinna Davis, [PR2126](https://github.com/CrocSwap/integer-mult-bounds/pull/2126), and Jeremy Diviney (`jeremydiviney`), [PR2203](https://github.com/CrocSwap/integer-mult-bounds/pull/2203):** paired-plane scalar identity fit and native payload accounting. Their distinction between coefficient blocks, independent payloads and native occurrences is retained. - **Sagar Thakrar, [PR2484](https://github.com/CrocSwap/integer-mult-bounds/pull/2484), head `4823273c8163e4c72472bdf7d42202e2c12d2e46`, following ywz65's PR2471:** exact scalar minimum rank 49 on a different, fixed paired-plane mask, including disjoint-support upper and submatrix lower certificates. Those proof methods are prior work. This package supplies a different three-plane cover, its exact rank and full charge; rank 57 versus 49 does not compare complete supplier costs. +- **Hanson Sun (`bbMisk`), [decoder-excess-rank](../decoder-excess-rank/README.md), following joaqcoo/PR1224:** the general Sylvester excess-rank and projection framework is prior work. The new contribution here is the source-bound cost consequence for this different full-group mask, not that rank inequality. + At the scientific base the central ledger marks PR1889, PR2041, PR2126 and PR2203 incorporated as scoped results, which does not admit a new supplier. PR2532 and PR2484 are pinned pending sources for context and overlap. The selected PR1094 lineage, including Rohan Arun and Jeremy Kothe, retains credit for the labels. Native frame-distance work by icekylinx and its independent check by woklerx retain their credit through the predecessors. Prepared by flyingviper with substantial OpenAI Codex assistance in search, proof development, implementation and separate-agent checking. No independent human review, formal verification of the full theorem, selected-result change or new exponent is claimed. New work is Apache-2.0. ## Open next questions -1. **Can a different rational factorization exploit this mask to lower the full port-space bill?** Start with at least 58 nonzero terms, and either introduce factor directions outside the fitting matrix's column/row spaces or increase the fitting rank. The cost theorems exclude every exactly-57-term rational fit and all overcomplete decompositions of rank-57 fitting matrices that retain both spans, including asymmetric ones. Enforce every diagonal and forbidden entry exactly before pricing whole source and reader spaces. A useful first gate is `C < 2672/9`; a selected-bound candidate needs a full moment below one near the incumbent saving, requiring roughly `C<=261` even in the favorable rank-9 relaxation. Stop a factorization family when its favorable complete invoice misses that gate. Diagonal rescaling of the saved factors costs 334 and does not reopen it. +1. **Can a different rational factorization exploit this mask to lower the full port-space bill?** Start with at least 59 nonzero terms, and either introduce factor directions outside the fitting matrix's column/row spaces or increase the fitting rank. The cost theorems exclude every rational fit with at most 58 terms and all overcomplete decompositions of rank-57 fitting matrices that retain both spans, including asymmetric ones. Enforce every diagonal and forbidden entry exactly before pricing whole source and reader spaces. A useful first gate is `C < 2672/9`; a selected-bound candidate needs a full moment below one near the incumbent saving, requiring roughly `C<=261` even in the favorable rank-9 relaxation. Stop a factorization family when its favorable complete invoice misses that gate. Diagonal rescaling of the saved factors costs 334 and does not reopen it. 2. **Can a different block or native contract realize useful sharing with every independent payload charged?** First supply the complete operator identity, dirty-input behavior and actual occurrences, rather than charging a geometric rank once for a multi-array block. Before another construction round, update the family budget and consumer boundary: source preparation, chart conversion, routing, hosting, chronological ownership, storage, erasure/restoration, precision, all-size recursion and a compatible bit supplier remain unproved here. Their costs are unknown, not zero. This finite certificate supplies neither physical compilation nor the selected cold replay. From 80fcf5dad26c2d91aa8993cc120e702f75efc5cf Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 23:33:50 +0200 Subject: [PATCH 20/22] Record P112 exterior-factor result and next constructive boundary --- research/p112-rational-decoder-gate/TASK.json | 69 ++++++++++++++++--- 1 file changed, 60 insertions(+), 9 deletions(-) diff --git a/research/p112-rational-decoder-gate/TASK.json b/research/p112-rational-decoder-gate/TASK.json index 3128432e6a..790f6c68a9 100644 --- a/research/p112-rational-decoder-gate/TASK.json +++ b/research/p112-rational-decoder-gate/TASK.json @@ -45,21 +45,21 @@ ] }, "scope_status": "changed", - "actual_scope": "Construct and independently certify a changed 37-triad/one-line P112 mask with exact scalar fitting rank57, compare the old rank99 mask, and fully price the explicit scalar factors. Prove the sharp334 whole-port-space floor for every exactly57-term rational fit on the changed mask. Prove a308 lower bound for any-length decompositions of rank57 fits whose factors retain both column/row spans.", + "actual_scope": "Construct and independently certify a changed 37-triad/one-line P112 mask with exact scalar fitting rank57, compare the old rank99 mask, and fully price the explicit scalar factors. Prove the sharp334 whole-port-space floor for every exactly57-term rational fit on the changed mask. Prove a308 lower bound for any-length decompositions of rank57 fits whose factors retain both column/row spans. Prove that every rational scalar fit with at most58 terms costs at least297, including exterior factors and rank58 matrices.", "scope_change_reason": "User selected rational/block P112 decoder research after PR2532 invalidated the original binary lift. The old cover obstructs natural fractional routes; change the cover to expand actual orthogonal-group freedom instead of optimizing the invalid binary invoice.", - "bottleneck_link": "The changed cover attains scalar rank57, but every57-term fit costs334. At any factor count, rank57 fits retaining both factor spans cost at least308. Both exceed2672/9, so successful scalar sharing must use exterior factor directions or higher fitting rank.", + "bottleneck_link": "The changed cover attains scalar rank57. Exactly57 terms cost334; every fit with at most58 terms costs at least297. At any factor count, rank57 fits retaining both factor spans cost at least308. All exceed2672/9; a candidate needs at least59 terms and exterior directions or higher fitting rank.", "budget_minutes": 60, "stop_rule": "Retain one verified mask/cost result after exact endpoint and independent checks. Reject the explicit supplier target at zero saving; do not infer a universal rational-decoder or cover obstruction from bounded motif searches.", "outcome": "partial", - "evidence": "CANDIDATE.json, exact identity-minor and disjoint-support proof in README, primary RESULT.json and independently implemented checker. Both original and new masks are certified. RANK-TIGHT-PROOF.md plus two independent finite-premise/fixture checkers establish the scoped minimum-length cost floor. Independently implemented40-space closures support the additional any-length, both-spans cost theorem.", + "evidence": "CANDIDATE.json, exact identity-minor and disjoint-support proof in README, primary RESULT.json and independently implemented checker. Both original and new masks are certified. RANK-TIGHT-PROOF.md plus two independent finite-premise/fixture checkers establish the scoped minimum-length cost floor. Independently implemented40-space closures support the additional any-length, both-spans cost theorem. EXTERIOR-58-PROOF.md and two independent finite-premise implementations extend the gate to all58-term fits.", "author": "flyingviper (with OpenAI Codex)", "ai_assistance": "Substantial OpenAI Codex assistance in algebra, search, implementation, writing and testing. Three AI agents split independent scalar checks, cost/mask research, and fractional/operator exploration. No independent human or proof-assistant review is claimed.", "open_questions": [ { "question": "Can a genuinely shared fractional decoder improve the new mask's334 port-space charge?", "why_it_matters": "The scalar rank obstacle has fallen99 to57, but break-even requires C<2672/9 and the selected-target optimistic allowance is smaller.", - "first_step": "Use at least58 terms and exterior factor directions or a higher-rank fitting matrix. Check every constrained coefficient, then price complete group-space pairings.", - "blocked_by": "The exact57-term floor is334; at arbitrary term count, rank57 fits retaining both canonical factor spans cost at least308. Exterior directions and higher fitting ranks remain open." + "first_step": "Use at least59 terms with exterior factor directions or a higher-rank fitting matrix. Enforce every constrained coefficient exactly, then price complete group-space pairings.", + "blocked_by": "Every fit with at most58 terms costs at least297. Rank57 fits retaining both factor spans cost at least308 at arbitrary term count. The unrestricted59-or-more-term case remains open." }, { "question": "Can a different mask or operator contract supply genuinely cheaper payload transport?", @@ -99,7 +99,7 @@ }, "family_gate": { "decision": "narrow", - "proved": "Exact minimum scalar fitting rank57 for the new mask, rank99 comparison, complete334 port-space charge of the displayed factors, and failure of the favorable coverage screen already at a=0. Sharp334 floor for all exactly57-term rational fits on this mask. Any-length rank57 decompositions retaining both factor spans cost at least308.", + "proved": "Exact minimum scalar fitting rank57 for the new mask, rank99 comparison, complete334 port-space charge of the displayed factors, and failure of the favorable coverage screen already at a=0. Sharp334 floor for all exactly57-term rational fits on this mask. Any-length rank57 decompositions retaining both factor spans cost at least308. Every fit with at most58 nonzero rational terms costs at least297.", "unknown": [ "native caller", "routes and chronological ownership", @@ -109,7 +109,7 @@ "all-size admission", "bit-side transfer" ], - "next": "An explicit rational fit with exterior factor directions or higher fitting rank, with full-group charge<=296; no physical expansion before that screen." + "next": "At least59 nonzero terms, exterior directions or higher fitting rank, exact full-group charge<=296. No physical expansion before that screen." }, "validation": { "environment": "3.12.14", @@ -147,7 +147,7 @@ "all-size recursion", "bit supplier transfer" ], - "next_test": "At least58 terms with exterior factor directions, or a higher-rank fitting matrix. Both-canonical-span families fail the zero-saving gate.", + "next_test": "Historical next test from the prior cost round: at least58 terms with exterior directions or higher fitting rank. Superseded by exterior_followup: every at-most58-term fit fails, so the current target needs at least59 terms.", "stop_rule": "One bounded research session; retain an exact new construction or decision-changing obstruction, otherwise concise negative search handoff. Do not represent a bounded search as a universal barrier.", "overlap": { "open_pr_snapshot": "2026-10-15T20:57:50Z", @@ -161,12 +161,63 @@ "PR2724 nine-term rank8 realization, different contract" ] }, - "started_at_utc": "2026-10-15T20:42:04.228659+00:00", + "started_at_utc": "2026-10-15T22:42:04.228659+02:00", "upstream_refresh": { "checked_at_utc": "2026-10-15T20:57:50Z", "canonical_main": "8e22a9d9f621c72ab5b299061c2be4c7f638fd3c", "priority_revision": 5, "decision": "Fast-forwarded isolated follow-up worktree; guidance, selected record and consumed inputs unchanged. Updated registered runner replayed. Existing PR retains construction source pins." } + }, + "exterior_followup": { + "task": "Continue P112 cheaper rational decoder, with exterior factor directions or changed fitting rank", + "status": "independently checked contribution", + "canonical_investigation": "https://github.com/CrocSwap/integer-mult-bounds/pull/2757", + "published_head": "1c7bdd4575137b3334adb185ec8f7efb63584b9e", + "round_started_utc": "2026-10-15T21:06:20Z", + "fresh_main": "31452ecd309f32a97e2e84214719b21297a59018", + "priority_revision": 5, + "selected_kappa": "0.001672660197076918", + "source_compatibility": "Relevant guidance, selected input archive and P112 geometry unchanged at fresh main", + "decision": "Retain one focused all58-term cost obstruction in PR2757. Preserve bounded coordinate-motif searches and the failed signed-lift shortcut as local handoff evidence; no cheaper candidate.", + "target": "An exact rational strict-mask fit with full group-space charge at most296; this is only a necessary optimistic supplier gate", + "boundary": { + "inputs": "112 independent scalar port payloads, grouped by the PR2757 cover of37 triads and one line", + "outputs": "Common nonzero scalar diagonal and zero at every nonfree offdiagonal endpoint", + "free_entries": "Only pairs of orthogonal whole group spaces", + "cost": "Sum of binary bilinear pairing ranks of whole source/reader group spans for each nonzero rational rank-one term" + }, + "obligation_ledger": { + "saved_scalar_fit_rank57_cost334": "independently reproduced finite certificate", + "all_exactly57_terms_floor334": "published scoped proof and independently checked geometry", + "rank57_both_factor_spans_floor308": "published scoped proof and independently checked geometry", + "exterior_or_higher_rank_fit_under297": "unknown", + "native_preparation_chart_conversion": "unknown", + "routing_hosting_chronological_ownership": "unknown", + "storage_waiting_dirty_compensation_restoration": "unknown", + "precision_all_size_recursion_compatible_bit_supplier": "unknown" + }, + "bounded_tests": [ + "Exact rational reader synthesis over a declared projective source library, leaving free mask entries adjustable", + "Coefficient-independent support cancellation closure for one-coordinate two-pair motifs", + "One-sided exterior normal form and cost audit at58 terms", + "Rational signed-root annihilating lift and its tariff defects" + ], + "stop_rule": "Do not repeat a disproved local family or extend random seeds. Reserve final quarter of approximately60-minute session for independent checks and a discriminating handoff. Publish only a useful independently reviewable result, not an unverified candidate or narrow stop theorem alone.", + "overlap": { + "open_pr_snapshot_utc": "2026-10-15T21:08:48Z", + "coverage": "100 most recently updated open PRs plus1963 local records; not a novelty guarantee", + "own_pr_feedback": "No reviews, inline comments or discussion comments at refresh", + "discussion_limitation": "Prior HTTP406 stopped live discussion requests. Reused cached1166/1167/2024 from20:19Z and1587 from20:39Z; no retry or bypass of blocked discussion routes." + }, + "result": "Every rational scalar fit with at most58 nonzero terms costs at least297, so any charge<=296 candidate needs at least59 terms.", + "verification": "check_exterior_58.py and independent_exterior_58.py reconstruct1750 reader spans,2318 cheap-source unions and314 Schur support rectangles. Written proof independently audited by separate AI agents; no formal kernel or human review.", + "final_refresh": { + "canonical_main": "a571dfa6e21bbe2d3b9cac48e5b078df59e49b68", + "checked_at_utc": "2026-10-15T21:29:10Z", + "decision": "Fast-forwarded isolated worktree. Guidance, selected record and consumed inputs unchanged. Newly integrated reviews cover different decoder contracts; no conflicting same-mask theorem found in bounded overlap.", + "open_pr_coverage": "latest100 updated open PR bodies", + "discussion_limitation": "Prior HTTP406 remains; cached discussion evidence retained without retry or bypass." + } } } From 2c54b99055aaa21d0bd3c8c8e4c48ce3c7fb1dd9 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Thu, 15 Oct 2026 23:33:57 +0200 Subject: [PATCH 21/22] Register independent P112 exterior-factor cost-floor replays --- .../p112-rational-decoder-gate/VERIFY.json | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/research/p112-rational-decoder-gate/VERIFY.json b/research/p112-rational-decoder-gate/VERIFY.json index 642d4f7127..392d651232 100644 --- a/research/p112-rational-decoder-gate/VERIFY.json +++ b/research/p112-rational-decoder-gate/VERIFY.json @@ -62,6 +62,28 @@ ], "timeout_seconds": 120, "checks": "Independent exact40-space closure using echelon tuples; all272 discounted rectangles, sampling inequality, missing-seed and missing-generated-span controls. Supports written both-canonical-spans proof, not unrestricted decoders." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/check_exterior_58.py" + ], + "timeout_seconds": 120, + "checks": "Pinned full-group geometry; complete1750 physical-triad closure,2318 affected-set unions, Schur forest and314 support rectangles; semantic mutation controls. Supports the written all58-term cost proof, not a formal proof kernel." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent_exterior_58.py" + ], + "timeout_seconds": 120, + "checks": "Independent explicit-vector-set reconstruction and annihilator ranks; independently derive1750 spans,2318 affected-set unions and314 Schur rectangles with source/geometry controls. Does not import the primary checker." } ] } From 18da668a4f248f5c0cf3fc94355068ead4db3476 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Fri, 16 Oct 2026 00:41:57 +0200 Subject: [PATCH 22/22] Prove the sharp P112 canonical-span decoder cost floor Retain the same pure-J count in the full57 and restricted54 acyclic budgets to prove C >=334+2s for every both-canonical-span decomposition with57+s terms. Add an independent exact checker and receipt; all eight registered replays pass. No cheaper decoder or supplier claim. --- .../CANONICAL-SHARP-PROOF.md | 96 ++++++++++++++ .../CANONICAL-SHARP-RESULT.json | 54 ++++++++ .../RANK-TIGHT-PROOF.md | 8 ++ research/p112-rational-decoder-gate/README.md | 33 +++-- research/p112-rational-decoder-gate/TASK.json | 24 +++- .../p112-rational-decoder-gate/VERIFY.json | 11 ++ .../check_canonical_sharp.py | 120 ++++++++++++++++++ 7 files changed, 333 insertions(+), 13 deletions(-) create mode 100644 research/p112-rational-decoder-gate/CANONICAL-SHARP-PROOF.md create mode 100644 research/p112-rational-decoder-gate/CANONICAL-SHARP-RESULT.json create mode 100644 research/p112-rational-decoder-gate/check_canonical_sharp.py diff --git a/research/p112-rational-decoder-gate/CANONICAL-SHARP-PROOF.md b/research/p112-rational-decoder-gate/CANONICAL-SHARP-PROOF.md new file mode 100644 index 0000000000..6143e856b5 --- /dev/null +++ b/research/p112-rational-decoder-gate/CANONICAL-SHARP-PROOF.md @@ -0,0 +1,96 @@ +# Sharp minimum cost across all canonical-span decompositions + +For any rank57 fitting matrix on the pinned PR2757 mask, assume both factor +families lie in that matrix's column and row spaces. If there are m=57+s +nonzero rational rank-one terms, then + + C >=334+2s. + +The saved57-term construction attains334. Thus allowing arbitrary extra terms +within both spans cannot lower the invoice. The statement excludes exterior +factor directions, higher-rank fitting matrices, changed covers and changed +physical contracts. It is a finite decoder-cost result, not supplier admission. + +## Common definitions and inherited normal form + +Normalize the common diagonal to1. The existing normal-form proof gives +K=[I,A;B,BA] and factors U=[P;BP], V=[Q;A^T Q], with PQ^T=I57. The57 latent +coordinates consist of eighteen three-coordinate paired components H_i and +the three-coordinate component J. Invertible paired maps make each nonzero +paired component touch both physical triads, so its full port space is H_i. +The residual coefficients remain general linear functionals of component8. + +Call a term pure when either latent factor is supported entirely in J, and +let p_J count these terms. This is the same definition in both inequalities +below. Each pure term costs3; each nonpure term costs at least4. Let L4,L5 +count nonpure terms of actual tariff4 and5, and write D=2L4+L5. Since the +residual diagonal is nonzero, some nonpure term costs at least7. Consequently + + C >=6m-3p_J-D+1. (1) + +The extra1 is charged to a term outside both low-price classes. The pure +terms, the actual-price classes and this residual term are unchanged when +the identity is subsequently restricted. + +## Full and restricted acyclic budgets + +The existing complete40-space closure checks all272 ordered low-rank span +rectangles. Their maximal component supports are disjoint. A rank4 rectangle +has size1 by1; rank5 rectangles have size1 byk or k by1, k<=3. Each actual +term's supports are subsets of these maximal supports. Replacing a maximal +support by a nonempty subset only increases the probability that all source +components precede all reader components in a random order. The geometric +rank may be below the actual price because the closure omits the residual +line; this also only increases the discount available from the probability. + +For a random order of all19 components, select each low-price term when its +source support entirely precedes its reader support. Selected terms sum to +a strictly block triangular N. Therefore I57-N remains invertible, so at +most m-57 terms were selected. The exact census probabilities give + + D <=4(m-57). (2) + +Now remove the p_J pure terms and restrict to the54 ordinary coordinates. +The remaining m-p_J terms sum to I54, and every one has nonzero projections +on both sides. Delete J from each low-price support rectangle. The supports +are still nonempty and disjoint, and selection probabilities cannot decrease. +Repeating the same argument for a random order of these18 components yields + + D <=4(m-p_J-54). (3) + +This second argument requires no minimality of the remaining factorization: +the only rank assertion is that I54-N is invertible and a sum of its remaining +rank-one terms. The first argument has the identical property for I57. + +## Combine without discarding the pure-term count + +Substituting(2) and(3) separately into(1) gives + + C >=2m-3p_J+229, + C >=2m+ p_J+217. + +One quarter of the first lower bound plus three quarters of the second +cancels p_J, proving + + C >=2m+220 =334+2s. + +In particular m=58 costs at least336. The apparent333 possibility came from +retaining p_J in only the restricted inequality while discarding it in the +full inequality; it is not an unresolved construction after the two bounds +are combined. + +## Exact replay and review scope + +`check_canonical_sharp.py` authenticates the candidate, selected archive and +payload, reconstructs the40 spaces using explicit vector sets and +annihilators, and checks both selection probabilities on all272 rectangles. +It also verifies the exact affine combination, rejects missing closure +members and duplicate JSON keys, and prints a receipt without changing files. +The old checker uses an independent echelon representation. The proof was +separately audited by another AI agent; no human review or formal proof +assistant verification is claimed. + + python -I -O -B check_canonical_sharp.py --repo PATH_TO_REPOSITORY + +Receipt: `CANONICAL-SHARP-RESULT.json`. Its low-rectangle table SHA256 is +`12858a508b318f62a568fe5205d16a399fc4e3e7fdc9cb7e8ea413f0a444832e`. diff --git a/research/p112-rational-decoder-gate/CANONICAL-SHARP-RESULT.json b/research/p112-rational-decoder-gate/CANONICAL-SHARP-RESULT.json new file mode 100644 index 0000000000..6bdefe3126 --- /dev/null +++ b/research/p112-rational-decoder-gate/CANONICAL-SHARP-RESULT.json @@ -0,0 +1,54 @@ +{ + "archive_sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "candidate_lf_sha256": "dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b", + "combined_bound_coefficients": [ + 2, + 0, + 220 + ], + "controls": [ + "removed paired generator", + "removed generated span", + "duplicate JSON key" + ], + "full_bound_coefficients": [ + 2, + -3, + 229 + ], + "full_low_rectangles": { + "(1, 1, 4)": 20, + "(1, 1, 5)": 178, + "(1, 2, 5)": 33, + "(1, 3, 5)": 4, + "(2, 1, 5)": 33, + "(3, 1, 5)": 4 + }, + "generated_spaces": 40, + "ordinary_bound_coefficients": [ + 2, + 1, + 217 + ], + "ordinary_low_rectangles": { + "(1, 1, 4)": 20, + "(1, 1, 5)": 222, + "(1, 2, 5)": 13, + "(1, 3, 5)": 2, + "(2, 1, 5)": 13, + "(3, 1, 5)": 2 + }, + "payload_sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "rectangle_count": 272, + "rectangle_table_sha256": "12858a508b318f62a568fe5205d16a399fc4e3e7fdc9cb7e8ea413f0a444832e", + "result": "C >= 2m+220 = 334+2s, m=57+s", + "scope": "Any rank57 fit on the fixed mask with BOTH factor families in its column/row spaces; arbitrary rational coefficients and term count. Exterior factors and larger fitting rank excluded.", + "space_dimension_histogram": { + "0": 1, + "3": 1, + "6": 18, + "7": 2, + "8": 17, + "9": 1 + } +} diff --git a/research/p112-rational-decoder-gate/RANK-TIGHT-PROOF.md b/research/p112-rational-decoder-gate/RANK-TIGHT-PROOF.md index 11a0b94398..68d7545255 100644 --- a/research/p112-rational-decoder-gate/RANK-TIGHT-PROOF.md +++ b/research/p112-rational-decoder-gate/RANK-TIGHT-PROOF.md @@ -236,3 +236,11 @@ above. The selected P112 labels, tri-plane endpoint, strict mask and full-space tariff retain their predecessor attribution in the package [README](README.md). Prepared by flyingviper with substantial OpenAI Codex assistance and separate AI-agent checking. New work is Apache-2.0; no independent human review is claimed. + +## Sharp any-length refinement + +The valid 308 lower bound above is superseded, in exactly the same +both-canonical-spans scope, by [CANONICAL-SHARP-PROOF.md](CANONICAL-SHARP-PROOF.md): +`C >= 334+2s` for `m=57+s`. Keeping the identical pure-J count in the full +and ordinary-coordinate acyclic bounds closes the gap without new geometry. +The historical derivation and its checkers are retained as independent premises. diff --git a/research/p112-rational-decoder-gate/README.md b/research/p112-rational-decoder-gate/README.md index d3547cf2a8..6aa7ed3b07 100644 --- a/research/p112-rational-decoder-gate/README.md +++ b/research/p112-rational-decoder-gate/README.md @@ -1,8 +1,8 @@ -# A P112 cover with minimum scalar rank 57 and sharp minimum-length cost 334 +# A P112 cover with scalar rank 57 and sharp canonical-span cost 334 **Constructive finite result and cost audit; no new supplier or kappa.** For the same 112 selected labels used by PR2041, this package supplies a different cover by 37 orthonormal triads and one residual line. Its strict scalar endpoint mask has minimum fitting rank **exactly 57**, with an explicit 57-term integral fit and a matching principal-submatrix lower bound. For the fixed cover in PR2041, PR2532 identified a rank-at-least-99 obstruction; this package also supplies a matching 99-term fit. Thus the exact fixed-mask minimum changes from **99 to 57** when the cover changes. This opens more scalar sharing without reusing the invalid binary decoder target. -This is a partial result toward a rational decoder. Charging the full port spaces gives the displayed fit the profile `3 H3 + 53 H6 + H7`, of mass **334**. Even with the proposed coverage law and all additional costs set to zero, its zero-saving moment is **32871/32704 > 1**. A follow-up theorem proves that **every exactly-57-term rational fit on this mask costs at least 334**, including asymmetric factors and arbitrary nonzero common normalization. Moreover, at **any factor count**, a rank-57 fit costs at least **308** if both factor families remain in its column and row spaces. A further [exterior-factor theorem](EXTERIOR-58-PROOF.md) proves that **every rational fit using at most 58 nonzero rank-one terms costs at least 297**, whether its matrix rank is 57 or 58. These floors exceed the necessary charge of at most 296. The number 57 counts rank-one scalar terms; it is not a verified number of physical child calls. +This is a partial result toward a rational decoder. Charging the full port spaces gives the displayed fit the profile `3 H3 + 53 H6 + H7`, of mass **334**. Even with the proposed coverage law and all additional costs set to zero, its zero-saving moment is **32871/32704 > 1**. A follow-up theorem proves that **every exactly-57-term rational fit on this mask costs at least 334**, including asymmetric factors and arbitrary nonzero common normalization. Moreover, at **any factor count**, a rank-57 fit costs at least **334** if both factor families remain in its column and row spaces: with `m=57+s` nonzero terms, the sharper bound is `C >= 334+2s`. The saved construction attains this minimum at `s=0`. A further [exterior-factor theorem](EXTERIOR-58-PROOF.md) proves that **every rational fit using at most 58 nonzero rank-one terms costs at least 297**, whether its matrix rank is 57 or 58. These floors exceed the necessary charge of at most 296. The number 57 counts rank-one scalar terms; it is not a verified number of physical child calls. ## Exact object and contract @@ -56,7 +56,7 @@ Here both spans are equal. Each ordinary pair support touches two orthogonal non n_3=3,\qquad n_6=53,\qquad n_7=1,\qquad C=3\cdot3+53\cdot6+7=334. \] -This remains true after any diagonal conjugation above. The [minimum-length cost theorem](RANK-TIGHT-PROOF.md) extends this floor to every exactly-57-term rational scalar fit on this mask. This 334 bound does not bound decompositions with more terms, including overcomplete decompositions of rank-57 matrices. The additional 308 bound below has a different scope. The integral construction does not evade the earlier 2-integral floor of 334 for this 37-triad/one-line contract. +This remains true after any diagonal conjugation above. The [minimum-length cost theorem](RANK-TIGHT-PROOF.md) extends this floor to every exactly-57-term rational scalar fit on this mask. The minimum-length theorem alone does not bound decompositions with more terms. The [canonical-span refinement](CANONICAL-SHARP-PROOF.md) does: every overcomplete decomposition retaining both spans costs at least `334+2s`. Exterior directions and larger fitting ranks remain outside that refinement. The integral construction does not evade the earlier 2-integral floor of 334 for this 37-triad/one-line contract. The exact average unpaid dimension is @@ -99,12 +99,16 @@ at least `54*6 + 3*3 + 1 = 334`, attained by the saved construction. The argument does not reduce rational coefficients modulo two and covers nonintegral, nonsymmetric and nongauge factorizations. It closes optimization -at minimum factor count. For any number `m=57+s` of terms, an additional argument gives -`C >= max(334-s, 228+3s) >= 308` if both factor families remain in the rank-57 -matrix's column and row spaces. An exact closure of 40 binary component spaces -bounds the support patterns of discounted terms; an acyclic-subset argument -then bounds how many discounts the extra factors can buy. The floor 308 is a -lower bound, with no claim that it is attainable. +at minimum factor count. For any number `m=57+s` of terms retaining both canonical spans, the +[sharp refinement](CANONICAL-SHARP-PROOF.md) proves `C >= 334+2s`. It keeps the +same pure-J term count in two acyclic-subset inequalities: one for all 57 +latent coordinates and one for the 54 ordinary coordinates. Their exact +convex combination cancels that count. The same complete 40-space closure +and 272 low-price rectangles suffice. This supersedes the earlier valid but +weaker lower bound of 308; no new geometry or minimality assumption is added. +The new independent vector-set checker validates both probability budgets, +source pins and the affine combination; [its receipt](CANONICAL-SHARP-RESULT.json) +is retained. The symbolic argument remains a written proof, not a proof-assistant certificate. Thus **at least 59 factors and a change of span or fitting rank are necessary for charge <=296**, not sufficient; the 59-term necessity follows from the extension below. Exterior factor directions may cancel in the @@ -162,6 +166,7 @@ python3 -I -O -B research/p112-rational-decoder-gate/independent_cost_floor.py python3 -I -O -B research/p112-rational-decoder-gate/check_overcomplete_closure.py python3 -I -O -B research/p112-rational-decoder-gate/check_exterior_58.py python3 -I -O -B research/p112-rational-decoder-gate/independent_exterior_58.py +python3 -I -O -B research/p112-rational-decoder-gate/check_canonical_sharp.py python3 scripts/research_package.py --package research/p112-rational-decoder-gate --check-only python3.12 scripts/research_package.py --package research/p112-rational-decoder-gate ``` @@ -186,3 +191,13 @@ Prepared by flyingviper with substantial OpenAI Codex assistance in search, proo 1. **Can a different rational factorization exploit this mask to lower the full port-space bill?** Start with at least 59 nonzero terms, and either introduce factor directions outside the fitting matrix's column/row spaces or increase the fitting rank. The cost theorems exclude every rational fit with at most 58 terms and all overcomplete decompositions of rank-57 fitting matrices that retain both spans, including asymmetric ones. Enforce every diagonal and forbidden entry exactly before pricing whole source and reader spaces. A useful first gate is `C < 2672/9`; a selected-bound candidate needs a full moment below one near the incumbent saving, requiring roughly `C<=261` even in the favorable rank-9 relaxation. Stop a factorization family when its favorable complete invoice misses that gate. Diagonal rescaling of the saved factors costs 334 and does not reopen it. 2. **Can a different block or native contract realize useful sharing with every independent payload charged?** First supply the complete operator identity, dirty-input behavior and actual occurrences, rather than charging a geometric rank once for a multi-array block. Before another construction round, update the family budget and consumer boundary: source preparation, chart conversion, routing, hosting, chronological ownership, storage, erasure/restoration, precision, all-size recursion and a compatible bit supplier remain unproved here. Their costs are unknown, not zero. This finite certificate supplies neither physical compilation nor the selected cold replay. + +## Canonical-span refinement checkpoint + +This refinement extends PR2757 head `2c54b99055aaa21d0bd3c8c8e4c48ce3c7fb1dd9`. +Canonical main was refreshed to `28f54620ff770dd051d5df35882bd84303d13c6f`; +guidance, the selected record and consumed inputs were unchanged. Two separate +AI agents checked the proof and exact geometry, followed by the parent replay. +The sharp 334 result closes optimization inside both canonical spans. It is +a partial research result; the search for an exterior or changed-cover decoder +of charge at most 296 continues under the user's explicit persistent budget. diff --git a/research/p112-rational-decoder-gate/TASK.json b/research/p112-rational-decoder-gate/TASK.json index 790f6c68a9..36cf4c5ded 100644 --- a/research/p112-rational-decoder-gate/TASK.json +++ b/research/p112-rational-decoder-gate/TASK.json @@ -45,9 +45,9 @@ ] }, "scope_status": "changed", - "actual_scope": "Construct and independently certify a changed 37-triad/one-line P112 mask with exact scalar fitting rank57, compare the old rank99 mask, and fully price the explicit scalar factors. Prove the sharp334 whole-port-space floor for every exactly57-term rational fit on the changed mask. Prove a308 lower bound for any-length decompositions of rank57 fits whose factors retain both column/row spans. Prove that every rational scalar fit with at most58 terms costs at least297, including exterior factors and rank58 matrices.", + "actual_scope": "Construct and independently certify a changed 37-triad/one-line P112 mask with exact scalar fitting rank57, compare the old rank99 mask, and fully price the explicit scalar factors. Prove the sharp334 whole-port-space floor for every exactly57-term rational fit on the changed mask. Prove a sharp334+2s lower bound for any-length decompositions of rank57 fits whose factors retain both column/row spans. Prove that every rational scalar fit with at most58 terms costs at least297, including exterior factors and rank58 matrices.", "scope_change_reason": "User selected rational/block P112 decoder research after PR2532 invalidated the original binary lift. The old cover obstructs natural fractional routes; change the cover to expand actual orthogonal-group freedom instead of optimizing the invalid binary invoice.", - "bottleneck_link": "The changed cover attains scalar rank57. Exactly57 terms cost334; every fit with at most58 terms costs at least297. At any factor count, rank57 fits retaining both factor spans cost at least308. All exceed2672/9; a candidate needs at least59 terms and exterior directions or higher fitting rank.", + "bottleneck_link": "The changed cover attains scalar rank57. Exactly57 terms cost334; every fit with at most58 terms costs at least297. At any factor count, rank57 fits retaining both factor spans cost at least334. All exceed2672/9; a candidate needs at least59 terms and exterior directions or higher fitting rank.", "budget_minutes": 60, "stop_rule": "Retain one verified mask/cost result after exact endpoint and independent checks. Reject the explicit supplier target at zero saving; do not infer a universal rational-decoder or cover obstruction from bounded motif searches.", "outcome": "partial", @@ -59,7 +59,7 @@ "question": "Can a genuinely shared fractional decoder improve the new mask's334 port-space charge?", "why_it_matters": "The scalar rank obstacle has fallen99 to57, but break-even requires C<2672/9 and the selected-target optimistic allowance is smaller.", "first_step": "Use at least59 terms with exterior factor directions or a higher-rank fitting matrix. Enforce every constrained coefficient exactly, then price complete group-space pairings.", - "blocked_by": "Every fit with at most58 terms costs at least297. Rank57 fits retaining both factor spans cost at least308 at arbitrary term count. The unrestricted59-or-more-term case remains open." + "blocked_by": "Every fit with at most58 terms costs at least297. Rank57 fits retaining both factor spans cost at least334+2s for m=57+s at arbitrary term count. The unrestricted59-or-more-term case remains open." }, { "question": "Can a different mask or operator contract supply genuinely cheaper payload transport?", @@ -99,7 +99,7 @@ }, "family_gate": { "decision": "narrow", - "proved": "Exact minimum scalar fitting rank57 for the new mask, rank99 comparison, complete334 port-space charge of the displayed factors, and failure of the favorable coverage screen already at a=0. Sharp334 floor for all exactly57-term rational fits on this mask. Any-length rank57 decompositions retaining both factor spans cost at least308. Every fit with at most58 nonzero rational terms costs at least297.", + "proved": "Exact minimum scalar fitting rank57 for the new mask, rank99 comparison, complete334 port-space charge of the displayed factors, and failure of the favorable coverage screen already at a=0. Sharp334 floor for all exactly57-term rational fits on this mask. Any-length rank57 decompositions retaining both factor spans cost at least334+2s for m=57+s. Every fit with at most58 nonzero rational terms costs at least297.", "unknown": [ "native caller", "routes and chronological ownership", @@ -219,5 +219,21 @@ "open_pr_coverage": "latest100 updated open PR bodies", "discussion_limitation": "Prior HTTP406 remains; cached discussion evidence retained without retry or bypass." } + }, + "canonical_sharp_followup": { + "dependency_head": "2c54b99055aaa21d0bd3c8c8e4c48ce3c7fb1dd9", + "canonical_main": "28f54620ff770dd051d5df35882bd84303d13c6f", + "checked_at_utc": "2026-10-15T22:33:00Z", + "priority_revision": 5, + "source_compatibility": "Guidance, selected record and consumed inputs unchanged", + "result": "C >=334+2s for all m=57+s both-canonical-span decompositions of any rank57 fit on the fixed mask", + "supersedes": "The earlier308 floor in cost_followup is retained as historical provenance; the sharp minimum is334", + "proof": "CANONICAL-SHARP-PROOF.md", + "independent_checker": "check_canonical_sharp.py", + "receipt": "CANONICAL-SHARP-RESULT.json", + "review": "Two separate AI agents audited the shared classification and exact budgets; parent replay passed. No human or formal-kernel review claimed.", + "cost_improvement": false, + "selected_frontier_change": false, + "continuous_research": "User explicitly authorized continuing until a cheaper target is reached or stopped; this partial proof does not end the ongoing constructive search." } } diff --git a/research/p112-rational-decoder-gate/VERIFY.json b/research/p112-rational-decoder-gate/VERIFY.json index 392d651232..521659768e 100644 --- a/research/p112-rational-decoder-gate/VERIFY.json +++ b/research/p112-rational-decoder-gate/VERIFY.json @@ -84,6 +84,17 @@ ], "timeout_seconds": 120, "checks": "Independent explicit-vector-set reconstruction and annihilator ranks; independently derive1750 spans,2318 affected-set unions and314 Schur rectangles with source/geometry controls. Does not import the primary checker." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/check_canonical_sharp.py" + ], + "timeout_seconds": 120, + "checks": "Independent explicit-vector-set and annihilator audit of all40 spans and272 cheap rectangles, full57/restricted54 selection probabilities, exact pure-count cancellation giving334+2s, source pins and three mutation controls. Supports the written proof; not a formal kernel." } ] } diff --git a/research/p112-rational-decoder-gate/check_canonical_sharp.py b/research/p112-rational-decoder-gate/check_canonical_sharp.py new file mode 100644 index 0000000000..0e44a48375 --- /dev/null +++ b/research/p112-rational-decoder-gate/check_canonical_sharp.py @@ -0,0 +1,120 @@ +#!/usr/bin/env python3 +"""Read-only exact premises and affine combination for C>=334+2s. + +Explicit vector-set spaces and annihilators independently replay the existing +echelon-based closure. The universal rank argument is in the accompanying proof. +""" +from pathlib import Path +from fractions import Fraction +from collections import Counter +import argparse,hashlib,json,math,tarfile + +CANDIDATE='dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b' +ARCHIVE='f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6' +PAYLOAD='c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa' +MEMBER='candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' + +def need(condition,message): + if not condition:raise ValueError(message) + +def strict_pairs(pairs): + result={} + for key,value in pairs: + need(key not in result,'duplicate JSON key') + result[key]=value + return result + +def parse(raw):return json.loads(raw,object_pairs_hook=strict_pairs) +def dot(x,y):return (x&y).bit_count()&1 +def space(vectors): + result={0} + for v in vectors:result|={x^v for x in result} + return frozenset(result) +def join(a,b):return frozenset(x^y for x in a for y in b) +def dimension(a): + need(len(a)>0 and len(a)&(len(a)-1)==0,'space cardinality') + return len(a).bit_length()-1 +def annihilator(a):return frozenset(x for x in range(512) if all(not dot(x,y) for y in a)) +def rejects(callback,label): + try:callback() + except ValueError:return label + raise ValueError('mutation accepted: '+label) +def closure_premises(spaces,seeds): + need(frozenset({0}) in spaces and all(s in spaces for s in seeds),'missing generator') + need(all(join(a,b) in spaces for a in spaces for b in seeds),'not closed under generators') + +def main(): + parser=argparse.ArgumentParser();parser.add_argument('--repo',type=Path,default=Path(__file__).resolve().parents[2]);args=parser.parse_args() + repo=args.repo + raw=(repo/'research/p112-rational-decoder-gate/CANDIDATE.json').read_bytes().replace(b'\r\n',b'\n') + need(hashlib.sha256(raw).hexdigest()==CANDIDATE,'candidate LF pin');candidate=parse(raw) + archive=repo/'research/community-frontier1094-audit/selected-replay.tar.gz' + need(hashlib.sha256(archive.read_bytes()).hexdigest()==ARCHIVE,'archive pin') + with tarfile.open(archive) as a: + member=a.extractfile(MEMBER);need(member is not None,'payload member');raw=member.read() + need(hashlib.sha256(raw).hexdigest()==PAYLOAD,'payload pin') + recipes=sorted(parse(raw)['recipes'],key=lambda x:x['port']) + need([x['port'] for x in recipes]==list(range(112)),'port enumeration') + q=[x['q'] for x in recipes] + need(all(type(x) is int and 0=4 for a in H for b in H),'nonpure tariff floor') + need(all(rho(join(J,a),join(J,b))>=6 for a in H for b in H),'both-J floor') + residual=space(E[0]+E[15]+E[16]) + need(dimension(residual)==7 and dimension(residual)-dimension(residual&annihilator(residual))==7,'residual surcharge') + supports={a:tuple(i for i,h in enumerate(seeds) if h<=a) for a in allspaces} + full_hist=Counter();ordinary_hist=Counter();table=[] + for a in allspaces: + for b in allspaces: + A=supports[a];B=supports[b];A0=tuple(i for i in A if i<18);B0=tuple(i for i in B if i<18) + if not A0 or not B0:continue + r=rho(a,b) + if r>=6:continue + need(r in (4,5) and not set(A)&set(B),'low rectangle classes and disjointness') + full=Fraction(1,math.comb(len(A)+len(B),len(A))) + ordinary=Fraction(1,math.comb(len(A0)+len(B0),len(A0))) + need(6-r<=4*full and 6-r<=4*ordinary,'both discount bounds') + full_hist[(len(A),len(B),r)]+=1;ordinary_hist[(len(A0),len(B0),r)]+=1 + table.append({'left':list(A),'right':list(B),'rank':r,'full_probability':str(full),'ordinary_probability':str(ordinary)}) + expected={(1,1,4):20,(1,1,5):178,(1,2,5):33,(2,1,5):33,(1,3,5):4,(3,1,5):4} + need(dict(full_hist)==expected,'full low-rectangle census') + # Coefficients are ordered (m, P, constant). No unbounded numerical scan. + full_bound=(2,-3,229);ordinary_bound=(2,1,217) + combined=tuple(Fraction(a,4)+Fraction(3*b,4) for a,b in zip(full_bound,ordinary_bound)) + need(combined==(2,0,220) and 2*57+220==334,'exact convex combination') + need(Fraction(334)>Fraction(2672,9),'zero-saving allowance') + derived=next(a for a in allspaces if dimension(a)==8 and a not in seeds) + controls=[rejects(lambda:closure_premises(allspaces-{H[0]},seeds),'removed paired generator'), + rejects(lambda:closure_premises(allspaces-{derived},seeds),'removed generated span'), + rejects(lambda:parse('{"same":1,"same":2}'),'duplicate JSON key')] + ordered=sorted(table,key=lambda x:(x['left'],x['right'],x['rank'])) + encoded=json.dumps(ordered,sort_keys=True,separators=(',',':')).encode() + result={'candidate_lf_sha256':CANDIDATE,'archive_sha256':ARCHIVE,'payload_sha256':PAYLOAD, + 'generated_spaces':len(allspaces),'space_dimension_histogram':dict(sorted(Counter(dimension(a) for a in allspaces).items())), + 'full_low_rectangles':{str(k):v for k,v in sorted(full_hist.items())}, + 'ordinary_low_rectangles':{str(k):v for k,v in sorted(ordinary_hist.items())}, + 'rectangle_count':len(table),'rectangle_table_sha256':hashlib.sha256(encoded).hexdigest(), + 'full_bound_coefficients':full_bound,'ordinary_bound_coefficients':ordinary_bound, + 'combined_bound_coefficients':[int(x) for x in combined], + 'result':'C >= 2m+220 = 334+2s, m=57+s','controls':controls, + 'scope':'Any rank57 fit on the fixed mask with BOTH factor families in its column/row spaces; arbitrary rational coefficients and term count. Exterior factors and larger fitting rank excluded.'} + print(json.dumps(result,sort_keys=True)) + +if __name__=='__main__':main()