From daf116c67c1425d1e70a051010e3e57daaf095ad Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Wed, 21 Oct 2026 10:16:18 +0200 Subject: [PATCH 1/2] Bound three-mark decoder invoices by source density and axial count --- .../p112-no-axial-three-mark/AXIAL-AUDIT.md | 46 ++ .../p112-no-axial-three-mark/AXIAL-PROOF.md | 54 ++ .../INDEPENDENT-AUDIT.md | 89 +++ .../INDEPENDENT-RESULT.json | 104 ++++ research/p112-no-axial-three-mark/PROOF.md | 150 +++++ research/p112-no-axial-three-mark/README.md | 69 +++ research/p112-no-axial-three-mark/RESULT.json | 530 ++++++++++++++++++ .../p112-no-axial-three-mark/SOURCES.json | 48 ++ research/p112-no-axial-three-mark/TASK.json | 72 +++ research/p112-no-axial-three-mark/VERIFY.json | 36 ++ .../p112-no-axial-three-mark/independent.py | 124 ++++ research/p112-no-axial-three-mark/verify.py | 107 ++++ 12 files changed, 1429 insertions(+) create mode 100644 research/p112-no-axial-three-mark/AXIAL-AUDIT.md create mode 100644 research/p112-no-axial-three-mark/AXIAL-PROOF.md create mode 100644 research/p112-no-axial-three-mark/INDEPENDENT-AUDIT.md create mode 100644 research/p112-no-axial-three-mark/INDEPENDENT-RESULT.json create mode 100644 research/p112-no-axial-three-mark/PROOF.md create mode 100644 research/p112-no-axial-three-mark/README.md create mode 100644 research/p112-no-axial-three-mark/RESULT.json create mode 100644 research/p112-no-axial-three-mark/SOURCES.json create mode 100644 research/p112-no-axial-three-mark/TASK.json create mode 100644 research/p112-no-axial-three-mark/VERIFY.json create mode 100644 research/p112-no-axial-three-mark/independent.py create mode 100644 research/p112-no-axial-three-mark/verify.py diff --git a/research/p112-no-axial-three-mark/AXIAL-AUDIT.md b/research/p112-no-axial-three-mark/AXIAL-AUDIT.md new file mode 100644 index 0000000000..c721225e14 --- /dev/null +++ b/research/p112-no-axial-three-mark/AXIAL-AUDIT.md @@ -0,0 +1,46 @@ +# Independent audit of the axial normal form + +21 October 2026. PASS for the support-monotone normalization and the bound +`cost >= 12+n-3a`. This is a written proof audit using the previously checked +geometry; no new coefficient search, invoice solver or literature claim. + +Keep the precise hypotheses: three ordinary two-copy canonical marks in three +distinct paired roles, query matrix `C A`, exact endpoint `C C^T`, arbitrary +rational actual readers, and whole-group binary-rank tariffs. + +After restricting readers to the six marked ports, absorb each axial query's +nonzero scale into its reader. Queries on one axis have the same physical +source closure. Their merged reader support lies in the union of the old +supports. Rank of the corresponding concatenated pairing blocks is at most +the sum of their ranks, so the merge cannot increase the invoice. Removing +zero products gives normalized counts n and a, with a<=3. The counts need +not agree with the original factorization's term counts. + +For an axial term the source span has dimension six. The ambient binary +pairing is nondegenerate in dimension nine, so its annihilator has dimension +three. The established reader-span bound gives tariff at least k-1, where +k is the number of its selected reader triads. If h of those readers occupy +its own two marked ports, their full triads give an identity submatrix of +size3h: each own triad is orthonormal and the two are mutually orthogonal. +Thus tariff >= max(k-1,3h). This is at least k+h-2: use k-1 for h=0,1, and +3h=6 with k<=6 for h=2. Non-axial terms retain tariff >= k+1. + +At each output port, a sole active query must be proportional to the desired +marked unit vector. It is therefore its own axial query. Uniqueness of the +merged axial query per axis means every output with only one reader incidence +is counted in H=sum h; H may also count ports with more incidences, which only +weakens the lower bound. Hence I=sum k >=12-H. Summing the term tariffs yields + + cost >= I+(n-a)+H-2a >=12+n-3a. + +A hypothetical cost<=17 consequently has n<=5+3a. The retained at-most-five-term +floor excludes n<=5 independently of axial count. Thus the remaining normalized +ranges are n=6..8 for a=1, n=6..11 for a=2, and n=6..14 for a=3. The a=0 case +is already closed. These are necessary bounds, not existence statements. + +This audit does not claim a result for exterior queries, repeated paired roles, +residual-bearing or singleton marks, or changed fitting endpoints. Neither a +support-only feasible solution nor the systematic non-Fano suggestion in the +research note has been verified as an exact cheaper decoder. + +Separate AI-agent proof audit; no independent human or formal-kernel review. diff --git a/research/p112-no-axial-three-mark/AXIAL-PROOF.md b/research/p112-no-axial-three-mark/AXIAL-PROOF.md new file mode 100644 index 0000000000..c2d782a75a --- /dev/null +++ b/research/p112-no-axial-three-mark/AXIAL-PROOF.md @@ -0,0 +1,54 @@ +# Axial normal form and the next structural test + +21 October2026. Local deduction checked by a separate AI agent; no cheaper decoder or multiplication-bound claim. This extends the source-density floor in PROOF.md. No independent human or proof-kernel review is claimed. + +## Scope and support-monotone normalization + +Use exactly three ordinary two-copy canonical P112 marks in three distinct paired roles, with indicator matrix C. Let Q=C A and Q R=C C^T over Q, with arbitrary actual readers. Restrict reader columns to the six marked physical ports; every removed endpoint column was zero. This preserves the endpoint and cannot increase a full-group tariff. + +A query is axial when its coefficient column is a nonzero multiple of one marked unit vector. Absorb that scalar into its reader. All axial terms for the same mark can be replaced by their single sum c_i (sum r_t)^T. The new reader support lies in the union of old reader supports. With a fixed source closure S, binary rank satisfies rho(S,union T_t)<=sum rho(S,T_t), because the union matrix is assembled from the old column blocks. Thus this merge cannot increase the invoice. Remove zero terms after merging. Let n be the remaining term count and a the number of axial terms. Then a<=3, at most one for each marked axis. These are normalized counts, not the original number of terms before restriction/merging. + +## A finite term-count bound even with axial queries + +The existing geometric premises give dim(V)>=k+2 for the span V of any k selected reader triads. A non-axial query uses at least two marked coordinates, so its physical source span U has dimension at least8 in the nondegenerate9-dimensional binary ambient space. Its term tariff is at least k+1. + +For an axial term let k be the number of selected reader triads and h the number of its own two marked physical ports carrying a nonzero reader coefficient (h=0,1,2). Its source role spans a6-dimensional space, so its tariff is at least dim(V)-3>=k-1. Its own two physical triads are orthonormal and mutually orthogonal (the canonical expanded endpoint is I334); the h own reader triads therefore supply an I_(3h) submatrix, so the tariff is also at least3h. Since k<=6, + + tariff >= max(k-1,3h) >= k+h-2. + +For h=0 or1 the second inequality follows from k-1; for h=2 it follows from6>=k. This uses only the already authenticated canonical geometry. + +Let I be the sum of all reader-triad incidences after normalization, and H the sum of h over axial terms. Every marked port needs at least one reader entry. If it has only one, that query must be proportional to its own marked unit vector, hence it is counted in H. Every other port needs at least two. Therefore I>=12-H, even when some own axial readers coexist with additional terms. + +Summing dense and axial term bounds gives + + cost >= I+(n-a)+H-2a >= 12+n-3a. + +Consequently any local cost at most17 has n<=5+3a. Combined with the previously established no-saving result for n<=5, the only remaining normalized counts are: + +- a=1: 6<=n<=8; +- a=2: 6<=n<=11; +- a=3: 6<=n<=14. + +This does not prove those remaining classes save or are representable. The counts do not apply to exterior queries, repeated paired roles, singleton/residual marks or changed endpoints. The cost of the original factorization is at least the normalized cost, so an original cheap candidate would yield a cheap normalized one within these bounds. + +The independently checked stronger fact dim(V)>=6 for three distinct reader triads can improve individual k=3 tariffs by one. It is not needed for this term-count bound. + +## A decisive next test + +For one declared physical placement, a source/reader support type has one of +7 nonempty marked-source subsets and63 nonempty actual-reader subsets, at +most441 types. Charge its exact full-group tariff. A proposed invoice<=17 must +respect the axial uniqueness and term-count limits above. Every desired entry +of A R=C^T must be covered, and a zero entry cannot be covered by exactly one +nonzero product. These are necessary constraints, not sufficient rational +realizability. An infeasibility certificate would close every coefficient +choice at that placement. A feasible support requires an exact bilinear +endpoint solution with nonzero coefficients and a fresh full invoice before +it can be called a decoder. No support-feasibility census is claimed here. + +The same written proof audit checked the merge, the identity3h submatrix and +the incidence correction. Both registered geometry replays establish all +finite premises; no new computational input is required. The n>=6 part of the +remaining ranges invokes the precisely cited earlier five-term theorem, while +the upper bounds n<=5+3a follow from this proof alone. Apache-2.0. diff --git a/research/p112-no-axial-three-mark/INDEPENDENT-AUDIT.md b/research/p112-no-axial-three-mark/INDEPENDENT-AUDIT.md new file mode 100644 index 0000000000..7a0b3dfae1 --- /dev/null +++ b/research/p112-no-axial-three-mark/INDEPENDENT-AUDIT.md @@ -0,0 +1,89 @@ +# Independent audit of the no-axial three-mark floor + +21 October 2026. PASS for the stated `12+n` theorem and the interface to the +retained at-most-five-term theorem. Separate AI-agent review, not independent +human or formal-kernel verification. No cheaper decoder or new bound. + +## Written argument checked + +Three ordinary canonical marks in distinct paired roles have six actual ports +in six distinct triads. Disjoint indicator supports make `C` injective and +prevent cancellation between the coordinates of a single query `C a`. +Consequently a query with at least two nonzero marked coordinates touches two +complete paired roles; their binary union has dimension at least eight. + +Deleting reader entries outside the six output ports preserves the complete +endpoint, since each corresponding output column was zero. Whole-group tariffs +are monotone under this deletion. Count `n` only after deleting zero outer +products from this restricted factorization. Added null cancellations outside +the target cannot inflate this `n` and invalidate the bound. + +If one remaining term reads `k` of the six ports, the selected triads span at +least `k+2` dimensions: triad dimensions cover k=1; pair/triple facts cover k=2,3; +pigeonhole gives a complete paired role at k=4 and two at k=5,6. The source +annihilator has dimension at most one in the nondegenerate nine-dimensional +binary space. Hence the full pairing rectangle has rank at least `k+1`. + +`A R=C^T` forces every selected actual reader to use at least two query columns, +since no single non-axial query spans a marked unit vector. Distinct reader +ports occupy distinct triads, so their incidences are counted exactly by the +sum of the per-term k values. That sum is at least twelve. Therefore the +restricted invoice, and thus the original invoice, is at least `12+n`. +This closes every restricted n>=6. It does not by itself close n<=5. + +## Independently reconstructed finite geometry + +`independent.py` reads only the same two foundational SHA256-pinned inputs. +It imports no producer. It represents each physical space by its complete +annihilator as a512-bit set, intersects these sets, and derives ranks from +cardinality. No Gaussian elimination or producer receipt is used. + +All666 triad pairs have ranks `{4:2,5:59,6:605}`. The independent calculation +checks all7770 triad triples, whose ranks are `{6:31,7:900,8:4431,9:2408}`. +Thus every triple actually has rank at least six, stronger than the rank-five +premise needed in the proof. The producer's smaller argument checks the70 +extensions of the two rank-four pairs; that is sufficient because any triple +of rank at most four would contain such a pair and violate its extension check. + +The inputs have53 ordinary two-copy marks and18 distinct paired roles. Each +role consists of two mutually orthogonal orthonormal triads and has dimension +and canonical self-tariff six. All153 role pairs have ranks `{8:11,9:142}`. +These checks establish the finite premises without pricing decoder candidates. + +## Exact predecessor interface + +PR3684 at `fad2e401ff63c634fb04e47146b0323449af70dd`, +`research/p112-triad-matroid-boundary/PROOF.md`, section +"Every five-term replacement of three canonical terms has the original floor" +(lines349 onward), states the floor for any three distinct canonical columns +and any rational factorization of their exact sum into at most five terms. +It permits ambient factors, exterior directions, zero terms and cancellation. +The present restricted factorization is a special case, and its three ordinary +canonical terms have total tariff18. Hence this retained theorem closes n<=5; +together with the new n>=6 result it gives the all-term-count no-saving +corollary in the stated no-axial, three-distinct-role class. + +The predecessor proof and cost proof were inspected for this interface; its +full historical computational suite was not rerun during this audit. Its +archival merge does not itself establish independent mathematical acceptance. +The new registered finite replay should claim only the self-contained geometry +and new written12+n argument. If the all-n corollary is presented, name its +prior theorem dependency explicitly rather than implying the small replay +reproves the old classification. + +The following hashes match both the exact PR head and local working bytes: + +- `PROOF.md`: `80682e0928bbc052a56c4ad6c9a73d0f84f09c7c78190aae85e38754d9c438ac`. +- `COST-PROOF.md`: `a51e3dd991e77d94ad749863e2a476eef8c7a0ab638fb637c2eada2090057c6d`. +- `MATROID-PROOF.md`: `6e22565ed5f289e3e7a24cb9ed85b6f05820df1ee5bb65e54fd805e7b745eae7`. +- `VALIDATION.md`: `0731fcb078d0d50a3e8018cfeea315c1e9daa20f0ebf576bc477e9a751ae2ff6`. + +## Scope that must remain visible + +The source queries must lie in the three selected canonical marks' span and +have at least two nonzero marked coordinates. The marks must be ordinary, +two-copy, and from distinct paired roles. Axial queries, exterior source +directions, repeated roles, residual-bearing or singleton targets, and changed +allowed-free endpoints are not covered. The count n is the restricted active +count. The seven-query signed gluing is a corollary only after invoking the +retained <=5 theorem for its possible lower-active-count specializations. diff --git a/research/p112-no-axial-three-mark/INDEPENDENT-RESULT.json b/research/p112-no-axial-three-mark/INDEPENDENT-RESULT.json new file mode 100644 index 0000000000..db9dcac8c2 --- /dev/null +++ b/research/p112-no-axial-three-mark/INDEPENDENT-RESULT.json @@ -0,0 +1,104 @@ +{ + "status": "PASS_INDEPENDENT_NO_AXIAL_GEOMETRY", + "method": "Exact annihilator sets; no elimination or producer imports", + "scientific_inputs": { + "research/p112-rational-decoder-gate/CANDIDATE.json": "dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b", + "research/adaptive-kernel-demotion/inputs/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + "physical_triads": 37, + "triad_pair_checks": 666, + "triad_pair_ranks": { + "4": 2, + "5": 59, + "6": 605 + }, + "triad_triple_checks": 7770, + "triad_triple_ranks": { + "6": 31, + "7": 900, + "8": 4431, + "9": 2408 + }, + "ordinary_marks": 53, + "paired_roles": [ + [ + 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 + ] + ], + "paired_role_union_checks": 153, + "paired_role_union_ranks": { + "8": 11, + "9": 142 + }, + "canonical_ordinary_tariff": 6, + "scope": "Finite geometry only; arbitrary-coefficient cost >= 12+n is a written proof" +} diff --git a/research/p112-no-axial-three-mark/PROOF.md b/research/p112-no-axial-three-mark/PROOF.md new file mode 100644 index 0000000000..eb55a57e3d --- /dev/null +++ b/research/p112-no-axial-three-mark/PROOF.md @@ -0,0 +1,150 @@ +# A source-density floor for three ordinary marked targets + +21 October 2026. Local structural deduction, not a lower multiplication bound. +This proof is independent of the selective circuit-relaxation package. + +## Precise statement + +Choose three ordinary two-copy canonical P112 marks from three distinct paired +roles. Their indicator matrix C has six nonzero rows, one in each of six +distinct physical triads. Let Q=C A, where every nonzero column of A has at +least two nonzero coordinates. For an arbitrary rational actual reader R with + +`Q R = C C^T`, + +first zero every reader column outside the six selected actual ports, and +delete zero outer products. Call the remaining number n. Then the original +complete physical-group invoice satisfies + +`cost >= 12+n`. + +In particular, n>=6 cannot improve the canonical local invoice18. Combining +this with the prior at-most-five-term three-projector floor gives a corollary +excluding every term count in this no-axial-query class; see the dependency +statement below. The primary new +claim here is the self-contained `12+n` bound; the older five-term theorem is +not a computational input to this note. + +This does not cover a query column proportional to one marked axis, repeated +paired roles, J-singleton targets, or the residual-bearing three-copy target. +Nor does it cover query vectors outside the chosen canonical span. It allows +arbitrary rational coefficients, all reader asymmetry and cancellation, and +unbounded term count within the stated class. + +## Pinned finite geometric facts + +Use the physical groups and canonical marks from +`research/p112-rational-decoder-gate/CANDIDATE.json`, and their binary +nine-coordinate vectors from +`research/adaptive-kernel-demotion/inputs/DATA-PHASES.json`. The script verifies +their exact SHA256 pins before use, both partitions of112 ports, orthonormality +of every physical triad, and the following small facts. + +1. The18 ordinary paired roles consist of disjoint pairs of triads and each + role spans dimension6. Every two roles together span dimension at least8: + 142 of the153 pairs have rank9 and11 have rank8. +2. Among the666 distinct triad pairs,605 have rank6,59 rank5 and two rank4. + The rank4 pairs have physical group indices(1,11) and(2,27). Adjoining any + third physical triad to either pair gives rank at least6, in all70 tests. + Consequently every pair of triads has rank at least4, and every triple has + rank at least5: a triple of rank<=4 would have every pair of rank<=4 and + contradict the checked third-triad property. + +These are geometry premises, not a search over embeddings or coefficients. + +## Proof + +First delete every reader entry at a port outside the six selected rows of C. +Its complete old column Q R[:,p] is zero, so this deletion preserves the +endpoint and weakly shrinks the support/tariff of each term. Work with this +restricted factorization. Any terms that become zero can be removed; let n +denote its number of active terms. For a factorization with additional active +terms outside these ports, the proved lower bound uses this restricted n; +the conclusion cost>=18 for n>=6 refers to the restricted active count. + +For a term let U be the binary span of all physical triads touched by its query, +and T the nonempty set of selected triads touched by its reader. Its query uses +at least two marked coordinates, so disjointness of C implies its source +support includes the two complete paired roles. By Fact1, dim U>=8. + +Write V for the span of T and k=|T|. Then dim V>=k+2: + +- k=1 gives3 by triad orthonormality; +- k=2 gives at least4, and k=3 at least5, by Fact2; +- k=4 contains both triads of some one of the three roles, giving at least6; +- k=5 or6 contains both triads of at least two roles, giving at least8. + +The ambient binary dot product is nondegenerate in dimension9. The complete +source/reader tariff is + +`rank = dim V - dim(V intersect U-perp) >= dim V -1 >= k+1`. + +Injectivity of C gives `A R = C^T`. At each of the six selected actual ports, +the active A-columns must span its marked unit vector. A single column cannot +do this, because every A-column has at least two nonzero coordinates. Thus each +selected port has at least two nonzero reader entries. Since those six ports +belong to distinct triads, summing k over the terms counts those reader +incidences exactly, and gives at least12. Summing the tariff bounds yields + +`cost >= sum(k+1) >=12+n`. + +If the original factorization has terms removed by reader restriction, its cost +is at least the restricted cost. For a complete no-saving conclusion, apply +the `12+n` bound when the restricted n>=6 and the prior five-term theorem when +the restricted n<=5. No inference is made by counting removed zero-effect terms. + +## Candidate consequence and provenance + +The locally proposed two-sign non-Fano dictionary + +`a+b, a+c, b+c, a+b+c, a-c, b-c, a+b-c` + +has no axial column. Hence it cannot improve the invoice in this scope, +without any reader or physical-placement search. Its original motivation was +to glue two sign-related specializations of the non-Fano recovery construction +in Das and Rai, [Generalized Fano and non-Fano networks](https://arxiv.org/pdf/1609.05815), +Lemma5 with q=2. Neither that paper nor a network broadcast rate supplies the +physical tariff argument. The dictionary gluing and geometric floor are local +deductions. More broadly, this bound applies to all no-axial dictionaries in the +specified three-mark canonical span, not only the seven displayed queries. + +## Prior five-term corollary and evidence boundary + +The standalone new theorem is `cost>=12+n`. For restricted n<=5, invoke the +five-term triple theorem in `research/p112-triad-matroid-boundary/PROOF.md`, +section "Every five-term replacement of three canonical terms has the original floor", and +its `COST-PROOF.md`. It covers any three canonical projectors and arbitrary +rational replacement factors, a superset of this note's factors. Consequently +the two results together give cost>=18 for every term count in the stated +no-axial three-distinct-role class. Keep the restricted n convention: terms +removed by zero-column restriction cannot move a factorization between cases. + +That earlier package is PR3684, exact source head +`fad2e401ff63c634fb04e47146b0323449af70dd`, retained in canonical main +`12fa8c5c844be21bfefb38a19503fbd867a11244`. Its unchanged proof files are pinned +as provenance in SOURCES.json. It has archival, partially-reviewed status; +merging is not scientific acceptance. Its complete classification/pricing +replay was previously run, but is not rerun or silently included in this +package's two geometry commands. The all-term corollary depends on that prior +theorem; the new12+n result does not. + +## Replay and next boundary + +`python3 -I -O -Werror -B research/p112-no-axial-three-mark/verify.py` + +The primary script authenticates the two foundational inputs and checks the +small geometry premises, all53 ordinary marks and their tariff6. Its default +is read-only; `--write-receipt` explicitly regenerates RESULT.json. The separate +independent checker reconstructs the geometry using annihilator sets instead +of elimination and additionally checks all7770 triad triples. The quantified +invoice proof above is a written argument, not a coefficient enumeration or a +proof-assistant theorem. These replays do not recheck the older five-term result. + +An axial query, an exterior query direction, repeated roles, or more marked +targets can evade this proof's premises. Their presence is not evidence of a +saving. A new construction should identify how it pays for dense reader/source +supports before any coefficient search. + +Prepared by flyingviper with substantial OpenAI Codex assistance. Separate +AI agents audited the proof and implemented independent checks; no independent +human or formal-kernel review is claimed. Apache-2.0. diff --git a/research/p112-no-axial-three-mark/README.md b/research/p112-no-axial-three-mark/README.md new file mode 100644 index 0000000000..a7f2b5f26f --- /dev/null +++ b/research/p112-no-axial-three-mark/README.md @@ -0,0 +1,69 @@ +# Source-density budgets for three ordinary P112 targets + +For three ordinary canonical marks in distinct paired roles, suppose every +query is in their span and uses at least two marks. Restrict arbitrary actual +readers to the six selected ports and remove zero terms; let n count the +remaining terms. The full physical-group invoice is at least **12+n**. +Thus six or more active terms cannot improve the canonical local cost18. +The proof covers every rational coefficient choice, arbitrary reader asymmetry +and cancellation, and unbounded term counts within these explicit premises. + +Allowing axial queries still gives a useful finite bound. Merge parallel axial +queries without increasing cost; let a<=3 count the remaining axial terms and +n count all active terms after restriction and merging. AXIAL-PROOF.md proves +**cost>=12+n-3a**. Therefore any cost<=17 witness has at most8,11 or14 normalized +terms when a=1,2 or3. This does not construct a saving or exclude those ranges. + +The argument combines small binary geometry facts with incidence counting: +each query spans at least8 physical dimensions, a reader touching k selected +triads costs at least k+1, and six marked outputs require at least12 reader +incidences. No coefficient grid or invoice census is used. + +Combining with the separately retained five-term triple theorem from +[PR3684](https://github.com/CrocSwap/integer-mult-bounds/pull/3684) rules out +all term counts in this class. That corollary has an explicit prior-theorem +dependency; the standalone12+n bound does not. The prior package's full +classification is not rerun here, and archival merging is not scientific +approval. PROOF.md and SOURCES.json identify the exact source head and proof pins. + +## Reproduction and scope + +From the repository root, Python3.12 or later, standard library only: + +```sh +python3 -I -O -Werror -B research/p112-no-axial-three-mark/verify.py +python3 -I -O -Werror -B research/p112-no-axial-three-mark/independent.py +python3 -B scripts/research_package.py --package research/p112-no-axial-three-mark +``` + +Both checkers authenticate only the two foundational geometry inputs. Their +normal modes are read-only. They use different rank methods and validate the +finite premises of the written proof, not the general theorem by enumeration. + +The12+n theorem excludes axial queries (a single marked coordinate); the +12+n-3a bound covers them after the stated normalization. Both exclude exterior +query directions, repeated paired roles, singleton/residual targets and +changed endpoints. It supplies no cost296 decoder, native schedule, universal +334 floor or improved multiplication bound. + +## Open next questions + +- Can axial and dense queries share readers profitably? First use the proved normalized term cap and test the at-most441 + exact support types at one declared placement, with cancellation constraints + and invoice<=17. Blocker: support feasibility alone does not provide + compatible nonzero rational coefficients or an exact endpoint. +- Can a larger jointly interacting marked set or an exterior direction evade + these costs? First provide one exact endpoint identity and a favorable + symbolic source/reader tariff budget. Blocker: density can erase rank savings, + and no such candidate is supplied here. + +## Credit + +The geometry and canonical cover retain their original P112 attribution. +The earlier five-term boundary is flyingviper's PR3684, including Nick Petalas' +classification and transfer lineage as credited in that package. The present +source-density argument is a local deduction, arising while screening a +signed non-Fano gluing; the motivating literature is identified in PROOF.md. +Prepared by flyingviper with substantial OpenAI Codex assistance and separate +AI-agent proof/implementation audits. No independent human or proof-assistant +review is claimed. Apache-2.0. diff --git a/research/p112-no-axial-three-mark/RESULT.json b/research/p112-no-axial-three-mark/RESULT.json new file mode 100644 index 0000000000..6c10d92e4a --- /dev/null +++ b/research/p112-no-axial-three-mark/RESULT.json @@ -0,0 +1,530 @@ +{ + "scope": "finite geometry premises for the written arbitrary-coefficient 12+n bound", + "source_sha256": { + "research/p112-rational-decoder-gate/CANDIDATE.json": "dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b", + "research/adaptive-kernel-demotion/inputs/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + "ports": 112, + "triad_count": 37, + "ordinary_marks": 53, + "ordinary_invoice": 6, + "triad_pair_checks": 666, + "triad_pair_rank_counts": { + "4": 2, + "5": 59, + "6": 605 + }, + "rank4_triad_pairs": [ + [ + 1, + 11 + ], + [ + 2, + 27 + ] + ], + "rank4_pair_third_checks": [ + [ + 1, + 11, + 2, + 7 + ], + [ + 1, + 11, + 3, + 7 + ], + [ + 1, + 11, + 4, + 7 + ], + [ + 1, + 11, + 5, + 7 + ], + [ + 1, + 11, + 6, + 7 + ], + [ + 1, + 11, + 7, + 6 + ], + [ + 1, + 11, + 8, + 7 + ], + [ + 1, + 11, + 9, + 7 + ], + [ + 1, + 11, + 10, + 7 + ], + [ + 1, + 11, + 12, + 7 + ], + [ + 1, + 11, + 13, + 6 + ], + [ + 1, + 11, + 14, + 7 + ], + [ + 1, + 11, + 15, + 7 + ], + [ + 1, + 11, + 16, + 7 + ], + [ + 1, + 11, + 17, + 7 + ], + [ + 1, + 11, + 18, + 7 + ], + [ + 1, + 11, + 19, + 7 + ], + [ + 1, + 11, + 20, + 7 + ], + [ + 1, + 11, + 21, + 6 + ], + [ + 1, + 11, + 22, + 6 + ], + [ + 1, + 11, + 23, + 7 + ], + [ + 1, + 11, + 24, + 6 + ], + [ + 1, + 11, + 25, + 7 + ], + [ + 1, + 11, + 26, + 7 + ], + [ + 1, + 11, + 27, + 7 + ], + [ + 1, + 11, + 28, + 7 + ], + [ + 1, + 11, + 29, + 7 + ], + [ + 1, + 11, + 30, + 6 + ], + [ + 1, + 11, + 31, + 7 + ], + [ + 1, + 11, + 32, + 7 + ], + [ + 1, + 11, + 33, + 7 + ], + [ + 1, + 11, + 34, + 7 + ], + [ + 1, + 11, + 35, + 7 + ], + [ + 1, + 11, + 36, + 7 + ], + [ + 1, + 11, + 37, + 7 + ], + [ + 2, + 27, + 1, + 7 + ], + [ + 2, + 27, + 3, + 7 + ], + [ + 2, + 27, + 4, + 7 + ], + [ + 2, + 27, + 5, + 7 + ], + [ + 2, + 27, + 6, + 7 + ], + [ + 2, + 27, + 7, + 7 + ], + [ + 2, + 27, + 8, + 7 + ], + [ + 2, + 27, + 9, + 7 + ], + [ + 2, + 27, + 10, + 6 + ], + [ + 2, + 27, + 11, + 7 + ], + [ + 2, + 27, + 12, + 7 + ], + [ + 2, + 27, + 13, + 7 + ], + [ + 2, + 27, + 14, + 7 + ], + [ + 2, + 27, + 15, + 7 + ], + [ + 2, + 27, + 16, + 6 + ], + [ + 2, + 27, + 17, + 7 + ], + [ + 2, + 27, + 18, + 7 + ], + [ + 2, + 27, + 19, + 7 + ], + [ + 2, + 27, + 20, + 7 + ], + [ + 2, + 27, + 21, + 6 + ], + [ + 2, + 27, + 22, + 7 + ], + [ + 2, + 27, + 23, + 7 + ], + [ + 2, + 27, + 24, + 7 + ], + [ + 2, + 27, + 25, + 7 + ], + [ + 2, + 27, + 26, + 7 + ], + [ + 2, + 27, + 28, + 7 + ], + [ + 2, + 27, + 29, + 7 + ], + [ + 2, + 27, + 30, + 7 + ], + [ + 2, + 27, + 31, + 7 + ], + [ + 2, + 27, + 32, + 7 + ], + [ + 2, + 27, + 33, + 7 + ], + [ + 2, + 27, + 34, + 7 + ], + [ + 2, + 27, + 35, + 7 + ], + [ + 2, + 27, + 36, + 7 + ], + [ + 2, + 27, + 37, + 7 + ] + ], + "minimum_third_union_rank": 6, + "paired_roles": [ + [ + 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 + ] + ], + "role_pair_checks": 153, + "role_pair_rank_counts": { + "8": 11, + "9": 142 + }, + "status": "PASS_NO_AXIAL_THREE_MARK_GEOMETRY" +} diff --git a/research/p112-no-axial-three-mark/SOURCES.json b/research/p112-no-axial-three-mark/SOURCES.json new file mode 100644 index 0000000000..1088d498ef --- /dev/null +++ b/research/p112-no-axial-three-mark/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/adaptive-kernel-demotion/inputs/DATA-PHASES.json", + "usage": "input", + "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + { + "path": "research/p112-rational-decoder-gate/CANDIDATE.json", + "usage": "input", + "git_blob": "e645ae164f5b4132889bd2aab162ecc2e8ebf4c4", + "sha256": "dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b" + }, + { + "path": "research/p112-triad-matroid-boundary/PROOF.md", + "usage": "provenance", + "git_blob": "8c16d8ed171fa94cac96fcafd3c27a334f6cc4b7", + "sha256": "80682e0928bbc052a56c4ad6c9a73d0f84f09c7c78190aae85e38754d9c438ac" + }, + { + "path": "research/p112-triad-matroid-boundary/COST-PROOF.md", + "usage": "provenance", + "git_blob": "91e4e33a025d76b265d23255cf2cfe89a5acbbcf", + "sha256": "a51e3dd991e77d94ad749863e2a476eef8c7a0ab638fb637c2eada2090057c6d" + } + ], + "prior_theorem": { + "pr": 3684, + "head": "fad2e401ff63c634fb04e47146b0323449af70dd", + "role": "Cited at-most-five-term result used only in the all-term corollary; not a live input or rerun by this package", + "review_status": "archival partially reviewed; no scientific approval inferred" + } +} diff --git a/research/p112-no-axial-three-mark/TASK.json b/research/p112-no-axial-three-mark/TASK.json new file mode 100644 index 0000000000..915f66b39c --- /dev/null +++ b/research/p112-no-axial-three-mark/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "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": "Prove a coefficient-independent12+n full-group invoice floor for no-axial queries in the span of three ordinary P112 marks from distinct paired roles, with arbitrary actual readers and restricted active term count n. Extend to axial queries after support-monotone merging: cost>=12+n-3a, giving normalized term caps8/11/14 for hypothetical cost<=17.", + "scope_change_reason": "The donor-assigned rational-decoder goal and continuous literature screen led to a seven-query non-Fano gluing. A dimension/incidence proof rejects every no-axial dictionary in this three-mark scope without coefficient or invoice searches.", + "bottleneck_link": "Any six-or-more-active-term decoder in this class costs at least18. Combined with the cited prior five-term theorem, a useful three-role canonical-source candidate must include an axial query.", + "budget_minutes": null, + "stop_rule": "Stop after the source-density proofs, two independent geometry checks, precise prior-theorem interface and focused publication. No coefficient/placement or support-feasibility census.", + "outcome": "negative-result", + "evidence": "PROOF.md gives the new12+n theorem and separately states its prior-dependent all-term corollary; verify.py and independent.py certify the small binary geometry premises. AXIAL-PROOF.md gives the separately audited axial merge and term cap from the same geometry.", + "author": "flyingviper", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, implementation, separate-agent mathematical audit and packaging. No independent human or formal-kernel review claimed.", + "open_questions": [ + { + "question": "Can axial and dense queries share readers below18?", + "why_it_matters": "Axial queries evade both steps in this source-density floor.", + "first_step": "Apply the proved normalized term cap to at most441 source/reader types at one declared placement, imposing exact tariffs, required-entry coverage and impossible-single-cover cancellation constraints.", + "blocked_by": "No saving identity or sufficient tariff certificate yet." + }, + { + "question": "Can larger target blocks or exterior directions save?", + "why_it_matters": "They evade the three-role canonical-source premise.", + "first_step": "Give one exact endpoint identity and a favorable full-group tariff budget before searching coefficients.", + "blocked_by": "No compatible cheap candidate or native execution proof." + } + ], + "budget_override": "User requests continuation until 30 percent account usage remains, with independent checks and publication of useful verified partial results." +} diff --git a/research/p112-no-axial-three-mark/VERIFY.json b/research/p112-no-axial-three-mark/VERIFY.json new file mode 100644 index 0000000000..33f6bb1674 --- /dev/null +++ b/research/p112-no-axial-three-mark/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p112-rational-decoder-gate/CANDIDATE.json", + "research/adaptive-kernel-demotion/inputs/DATA-PHASES.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Authenticate2inputs,112port partitions,37orthonormaltriads,666triadpairs,70criticalthird-triadunions,18roles/153rolepairs and53ordinary invoices. Geometry premises of written12+n proof only; prior\u22645theorem not replayed." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 30, + "checks": "Independent annihilator-set reconstruction of the geometric premises and all7770triadtriples, no producer imports." + } + ] +} diff --git a/research/p112-no-axial-three-mark/independent.py b/research/p112-no-axial-three-mark/independent.py new file mode 100644 index 0000000000..4df2242614 --- /dev/null +++ b/research/p112-no-axial-three-mark/independent.py @@ -0,0 +1,124 @@ +#!/usr/bin/env python3 +"""Independent exact geometric premises for the no-axial three-mark floor. + +Uses explicit annihilator sets in F2^9, not Gaussian elimination or producer +imports. The quantified invoice deduction is a written argument, not this replay. +""" +import argparse +from collections import Counter +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +PINS = { + "research/p112-rational-decoder-gate/CANDIDATE.json": + "dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b", + "research/adaptive-kernel-demotion/inputs/DATA-PHASES.json": + "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", +} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def check(repo): + objects = [] + for path, digest in PINS.items(): + raw = (repo / path).read_bytes() + need(sha256(raw).hexdigest() == digest, "scientific input pin: " + path) + objects.append(json.loads(raw)) + candidate, data = objects + groups = candidate["groups"] + marks = candidate["factor_supports"] + labels = {r["port"]: r["q"] for r in data["recipes"]} + owner = {p: g for g, ports in enumerate(groups) for p in ports} + need(sorted(p for g in groups for p in g) == list(range(112)), "group partition") + need(sorted(p for m in marks for p in m) == list(range(112)), "mark partition") + need(set(labels) == set(range(112)) and len(data["recipes"]) == 112, + "unique physical labels") + need(all(0 < v < 512 for v in labels.values()), "nine-bit nonzero labels") + triads = [g for g in range(len(groups)) if len(groups[g]) == 3] + + def dot(a, b): + return (a & b).bit_count() % 2 + + need(len(triads) == 37, "triad count") + need(all(dot(labels[p], labels[q]) == int(p == q) + for g in triads for p in groups[g] for q in groups[g]), + "triad orthonormality") + # Bit v represents the ambient vector v, including zero. Intersections of + # annihilators correspond to spans of unions. Their size is 2^(9-rank). + annihilators = { + g: sum(1 << v for v in range(512) + if all(dot(v, labels[p]) == 0 for p in groups[g])) + for g in range(len(groups)) + } + + def union_rank(group_indices): + intersection = (1 << 512) - 1 + for g in group_indices: + intersection &= annihilators[g] + cardinality = intersection.bit_count() + need(cardinality > 0 and cardinality & (cardinality - 1) == 0, + "annihilator must be a subspace") + return 9 - (cardinality.bit_length() - 1) + + pair_counts = Counter(union_rank(gs) for gs in combinations(triads, 2)) + triple_counts = Counter(union_rank(gs) for gs in combinations(triads, 3)) + ordinary = [m for m in marks if len(m) == 2 + and all(len(groups[owner[p]]) == 3 for p in m)] + roles = sorted({tuple(sorted(owner[p] for p in m)) for m in ordinary}) + need(len(ordinary) == 53 and len(roles) == 18, "ordinary mark/role counts") + need(all(len(set(r)) == 2 for r in roles) + and len({g for r in roles for g in r}) == 36, "disjoint paired roles") + need(all(union_rank(r) == 6 for r in roles), "paired-role dimension") + need(all(dot(labels[p], labels[q]) == 0 + for a, b in roles for p in groups[a] for q in groups[b]), + "paired triads are mutually orthogonal") + # Each ordinary self-rectangle is thus two orthonormal triads: tariff six. + role_pair_counts = Counter(union_rank(a + b) for a, b in combinations(roles, 2)) + need(pair_counts == {4: 2, 5: 59, 6: 605}, "all physical pair ranks") + need(triple_counts == {6: 31, 7: 900, 8: 4431, 9: 2408}, + "all physical triple ranks") + need(role_pair_counts == {8: 11, 9: 142}, "all paired-role union ranks") + return { + "status": "PASS_INDEPENDENT_NO_AXIAL_GEOMETRY", + "method": "Exact annihilator sets; no elimination or producer imports", + "scientific_inputs": PINS, + "physical_triads": len(triads), + "triad_pair_checks": sum(pair_counts.values()), + "triad_pair_ranks": dict(sorted(pair_counts.items())), + "triad_triple_checks": sum(triple_counts.values()), + "triad_triple_ranks": dict(sorted(triple_counts.items())), + "ordinary_marks": len(ordinary), + "paired_roles": roles, + "paired_role_union_checks": sum(role_pair_counts.values()), + "paired_role_union_ranks": dict(sorted(role_pair_counts.items())), + "canonical_ordinary_tariff": 6, + "scope": "Finite geometry only; arbitrary-coefficient cost >= 12+n is a written proof", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo-root", type=Path, default=HERE.parents[1]) + parser.add_argument("--write-receipt", action="store_true") + args = parser.parse_args() + result = check(args.repo_root) + payload = json.dumps(result, indent=2) + "\n" + receipt = HERE / "INDEPENDENT-RESULT.json" + if args.write_receipt: + receipt.write_text(payload, encoding="utf-8", newline="\n") + else: + need(receipt.read_text(encoding="utf-8") == payload, "receipt mismatch") + print(json.dumps({k: result[k] for k in + ("status", "triad_pair_checks", "triad_triple_checks", + "paired_role_union_checks", "canonical_ordinary_tariff")})) + + +if __name__ == "__main__": + main() diff --git a/research/p112-no-axial-three-mark/verify.py b/research/p112-no-axial-three-mark/verify.py new file mode 100644 index 0000000000..3f3e60cc07 --- /dev/null +++ b/research/p112-no-axial-three-mark/verify.py @@ -0,0 +1,107 @@ +#!/usr/bin/env python3 +"""Pinned geometric premises for the no-axial three-mark invoice bound.""" +from collections import Counter +from hashlib import sha256 +from itertools import combinations +from pathlib import Path +import argparse +import json + +HERE=Path(__file__).resolve().parent +PINS={ + 'research/p112-rational-decoder-gate/CANDIDATE.json': + 'dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b', + 'research/adaptive-kernel-demotion/inputs/DATA-PHASES.json': + 'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa', +} + + +def need(ok,message): + if not ok: + raise ValueError(message) + + +def rank(vectors): + pivots={} + for v in vectors: + while v: + p=v.bit_length()-1 + if p in pivots: + v ^= pivots[p] + else: + pivots[p]=v + break + return len(pivots) + + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--repo-root',type=Path, + default=HERE.parents[1]) + parser.add_argument('--write-receipt',action='store_true') + args=parser.parse_args() + source=[] + for path,digest in PINS.items(): + data=(args.repo_root/path).read_bytes() + need(sha256(data).hexdigest()==digest,'immutable input '+path) + source.append(json.loads(data)) + candidate,data=source + groups,marks=candidate['groups'],candidate['factor_supports'] + owner={p:i for i,ps in enumerate(groups) for p in ps} + marked={p:j for j,ps in enumerate(marks) for p in ps} + label={row['port']:row['q'] for row in data['recipes']} + need(set(owner)==set(marked)==set(label)==set(range(112)),'all112 ports') + need(sum(map(len,groups))==sum(map(len,marks))==len(data['recipes'])==112, + 'disjoint partitions and unique labels') + need(all(0=5, + 'no three physical triads fit in dimension4') + roles=sorted({tuple(sorted(owner[p] for p in ps if len(groups[owner[p]])==3)) + for ps in marks if len(ps)>=2}) + need(len(roles)==18 and all(len(r)==2 for r in roles),'18 paired roles') + need(len({i for r in roles for i in r})==36,'disjoint role triads') + need(all(group_rank(r)==6 for r in roles),'orthogonal paired roles span6') + role_pair_ranks=[[a,b,group_rank(roles[a]+roles[b])] + for a,b in combinations(range(18),2)] + need(Counter(r for a,b,r in role_pair_ranks)=={9:142,8:11},'role pair profile') + ordinary=[ps for ps in marks if len(ps)==2 and all(len(groups[owner[p]])==3 for p in ps)] + need(len(ordinary)==53,'53 ordinary marks') + for ps in ordinary: + rg=tuple(sorted(owner[p] for p in ps)) + need(len(set(rg))==2 and rg in roles,'ordinary mark occupies a paired role') + vv=[label[p] for g in rg for p in groups[g]] + gram=[sum(((x&y).bit_count()%2)< Date: Wed, 21 Oct 2026 10:24:07 +0200 Subject: [PATCH 2/2] Close every canonical-source decoder at the fixed three-mark placement --- .../FIXED-THREE-MARK-SOURCE-SPAN.md | 54 +++++ .../INDEPENDENT-FIXED-SOURCE-SPAN-PROOF.md | 67 ++++++ .../INDEPENDENT-FIXED-SOURCE-SPAN-RESULT.json | 221 ++++++++++++++++++ research/p112-no-axial-three-mark/README.md | 26 ++- research/p112-no-axial-three-mark/TASK.json | 10 +- research/p112-no-axial-three-mark/VERIFY.json | 24 ++ .../fixed-three-mark-source-span.json | 58 +++++ .../fixed_three_mark_source_span.py | 57 +++++ .../independent_fixed_source_span.py | 76 ++++++ 9 files changed, 583 insertions(+), 10 deletions(-) create mode 100644 research/p112-no-axial-three-mark/FIXED-THREE-MARK-SOURCE-SPAN.md create mode 100644 research/p112-no-axial-three-mark/INDEPENDENT-FIXED-SOURCE-SPAN-PROOF.md create mode 100644 research/p112-no-axial-three-mark/INDEPENDENT-FIXED-SOURCE-SPAN-RESULT.json create mode 100644 research/p112-no-axial-three-mark/fixed-three-mark-source-span.json create mode 100644 research/p112-no-axial-three-mark/fixed_three_mark_source_span.py create mode 100644 research/p112-no-axial-three-mark/independent_fixed_source_span.py diff --git a/research/p112-no-axial-three-mark/FIXED-THREE-MARK-SOURCE-SPAN.md b/research/p112-no-axial-three-mark/FIXED-THREE-MARK-SOURCE-SPAN.md new file mode 100644 index 0000000000..6be3f935d4 --- /dev/null +++ b/research/p112-no-axial-three-mark/FIXED-THREE-MARK-SOURCE-SPAN.md @@ -0,0 +1,54 @@ +# Complete canonical-source closure at one fixed three-mark placement + +21 October2026. New written deduction with a small exact geometric certificate; checked by a separate AI agent. No new multiplication bound. + +Fix the three canonical indicator columns c0,c1,c2 on {0,67}, {7,64}, {1,75}. Let C have those columns. Allow ANY finite number of rational queries Q=C A and arbitrary rational actual readers R such that Q R=C C^T. After restriction to the six marked actual reader ports and merging parallel axial queries, every factorization with invoice at most17 would have at most five terms. The already published five-term triple floor then rules it out. Thus the complete canonical-source family at this fixed placement has minimum18, attained by its three canonical projectors. + +The new self-contained theorem is the reduction to at most five terms; the final all-term floor explicitly uses the retained five-term theorem from PR3684 at fad2e401ff63c634fb04e47146b0323449af70dd, research/p112-triad-matroid-boundary/PROOF.md and COST-PROOF.md. That result is present in canonical main12fa8c5c844be21bfefb38a19503fbd867a11244. Its archival merge does not imply independent mathematical acceptance. This note does not replay the old full classification. + +## Normalization + +Every reader column outside the six marked ports reconstructs zero and may be set to zero separately. This preserves the endpoint and weakly reduces every tariff. Normalize an axial query proportional to c_j to c_j by absorbing the scalar into its reader. Replace all terms with that same axial query by c_j times the sum of their readers. New support is contained in the old reader union, and fixed-source rank subadditivity makes this operation tariff-nonincreasing. Remove zero terms. Let n be the normalized active count. There is at most one axial query for each marked axis. + +Because the three canonical supports are disjoint, a query with coefficient support sigma has exactly the physical source groups belonging to those marked axes. Every restricted reader uses some subset T of the six distinct physical groups, with one actual reader port in each. There are only7*63=441 nonzero support types, regardless of coefficient values or term count. + +## The complete small tariff certificate + +The six physical groups in marked-port order are17,18,29,30,31,32. Rebuilding the exact binary full-group pairing ranks yields: + +- All support types cost at least2. +- Exactly one costs2: source sigma={c1}, reader T={75}, i.e. group32, the second copy of c2. +- Exactly41 types cost3, and every one has a singleton reader. +- Every type with at least two reader ports costs at least4. + +The complete tariff histogram is {2:1,3:41,4:1,5:33,6:197,7:16,8:152}. The coefficient/reader masks for the unique cheap type are(2,32). The script authenticates both input hashes, canonical targets and physical groups, all441 tariffs and all12288 fixed-axial source-union subadditivity checks. Its compact digest commits the complete table. + +## Why six or more normalized terms cannot cost17 + +After axial merging there is at most one cost2 term, because the only cheap type has axial source c1. Every other active term costs at least3. Hence + + cost >= 3n-1. + +If n>=7, the invoice is at least20. If n=6 and cost<=17, equality in this lower bound is forced: one cost2 term and five cost3 terms. Every one has exactly one reader port. All six required endpoint columns are nonzero, so each of the six ports must be assigned exactly one of these six terms. The cost2 term would then have to reconstruct the c2 output at port75 using a nonzero multiple of c1 alone. The indicator columns are independent, so that is impossible. Thus n=6 also cannot cost<=17. + +Consequently every hypothetical cheaper factorization reduces to n<=5, preserving the exact endpoint and without increasing cost. The cited five-term triple theorem excludes it. This argument treats arbitrary rational coefficients, dependent queries, null cancellations and asymmetric copies. It does not classify coefficients or enumerate reader products. + +## Scope and next question + +This closes every canonical-source query dictionary at this fixed three-mark placement, including the seven-query systematic non-Fano completion, regardless of term count. It does not close other placements, repeated roles, more targets, exterior directions, or changed endpoints. No claim is made that the n>=6 subfamily itself attains18; the whole family attains18 using three canonical terms. + +The new reduction could be reproduced independently by rebuilding the441 table with a different binary-rank implementation. The tiny key premises are the unique2-cost off-axis singleton and the fact that every cost3 type is also singleton-reader. If these premises occur at another proposed placement, the same proof applies there, but no placement census is asserted or run. + + python3 -I -O -Werror -B research/p112-no-axial-three-mark/fixed_three_mark_source_span.py + +Default execution checks its compact receipt read-only; --write-receipt explicitly regenerates it. The input and invoice model are the same two pinned foundational files used by the prior P112 packages. This is a local deduction, not a claim from PIR or network-coding literature. + +The independent checker reconstructs all441 tariffs with binary span and +annihilator sets, without producer imports, and agrees on the complete table. +See INDEPENDENT-FIXED-SOURCE-SPAN-PROOF.md for its proof audit. Since the endpoint +and tariff are symmetric under transposition, the same floor holds if all +readers instead lie in this canonical span. A cheaper factorization at this +placement would need both factor families to escape the canonical span. +These are separate AI-agent checks, not independent human or formal-kernel +review. Prepared by flyingviper with substantial OpenAI Codex assistance. +Apache-2.0. diff --git a/research/p112-no-axial-three-mark/INDEPENDENT-FIXED-SOURCE-SPAN-PROOF.md b/research/p112-no-axial-three-mark/INDEPENDENT-FIXED-SOURCE-SPAN-PROOF.md new file mode 100644 index 0000000000..3ac310480c --- /dev/null +++ b/research/p112-no-axial-three-mark/INDEPENDENT-FIXED-SOURCE-SPAN-PROOF.md @@ -0,0 +1,67 @@ +# Independent fixed-mark canonical-source-span floor audit + +21 October 2026. PASS for the exact441-type tariff facts and the new >=6-term +exclusion. The all-term floor additionally invokes the retained <=5-term theorem. +No claim is made for other placements, changed endpoints or exterior queries. + +## Complete support tariff check + +Fix marked indicators a,b,c on `[0,67]`, `[7,64]`, `[1,75]`, in physical triads +`[17,18,29,30,31,32]`. For any rational query Cx, its exact physical source +closure depends only on the nonzero coordinate set sigma of x, because the +three indicator supports are disjoint. After restricting readers to those six +ports, the exact reader closure is a nonempty subset T of six distinct triads. +Thus all nonzero terms belong to the7 times63 =441 support types. + +The independent checker rebuilds these441 tariffs from only the two pinned +foundational inputs, with explicit binary span sets and annihilator +intersections. No producer import, primary receipt or Gram elimination is used. +It confirms every cost is at least2. The unique cost2 type is sigma={b}, +T={c-right}, encoded `(2,32)`. Exactly41 types have cost3, and every such reader +T is a singleton. Every type with at least two reader triads costs at least4. +The three canonical self-projectors each cost6 and attain total18. + +## Arbitrary coefficient and term-count proof + +Begin with any rational Q=C A and Q R=C C^T. Delete reader columns outside +the six marked ports; their old complete endpoint columns were zero. This +preserves the endpoint and cannot increase any tariff. Delete zero products. +Normalize each axial query's nonzero scalar into its reader and merge all +parallel axial queries on the same mark by summing readers. Fixed-source rank +subadditivity bounds the merged tariff by the sum of old tariffs. Remove any +new zero products. Let n count terms after these steps. + +Every term of cost2 is axial on b. The merge therefore leaves at most one +such term. All other nonzero terms have cost at least3. If n>=7, the cost is +at least2+3*(n-1)>=20 (or at least3n when no cost2 term remains), so cannot +be at most17. + +For n=6, cost at most17 requires exactly one cost2 term and five cost3 terms, +with exact total17. Every one has a singleton reader support. The six nonzero +marked endpoint columns each require at least one incidence. Six singleton +terms provide exactly six incidences, so exactly one term must read each +marked port. In particular the unique cost2 term is the sole reader at c-right, +but its query is a nonzero multiple of b. It cannot reconstruct c there: C is +injective and b,c are distinct marked coordinate axes. This contradiction +excludes n=6 for all nonzero rational coefficients, not merely sampled ones. + +For n<=5 apply the retained theorem in +`research/p112-triad-matroid-boundary/PROOF.md`, section beginning line349, +PR3684 head `fad2e401ff63c634fb04e47146b0323449af70dd`. It covers any three +canonical terms and arbitrary rational <=5-term exact replacements. Here +its baseline is18. The proof SHA256 is +`80682e0928bbc052a56c4ad6c9a73d0f84f09c7c78190aae85e38754d9c438ac`. +The dependency and its old evidence must remain explicit; the small441-type +replay does not reprove that historical classification. + +Thus no rational factorization with queries confined to this fixed C-span, +regardless of its original term count or copy-asymmetric actual readers, +can improve18. The original invoice dominates the normalized invoice. The +canonical three terms attain18, making the bound sharp. Arbitrary exterior +queries, other physical target placements, and changed allowed-free endpoints +remain outside this theorem. Transposing gives the corresponding reader-span +statement because the endpoint and physical tariffs are symmetric; it does +not require both factor families to be confined simultaneously. + +Separate AI-agent exact check and proof audit; not independent human or +formal-kernel verification. No cheaper decoder or multiplication-bound claim. diff --git a/research/p112-no-axial-three-mark/INDEPENDENT-FIXED-SOURCE-SPAN-RESULT.json b/research/p112-no-axial-three-mark/INDEPENDENT-FIXED-SOURCE-SPAN-RESULT.json new file mode 100644 index 0000000000..7dbe21f88c --- /dev/null +++ b/research/p112-no-axial-three-mark/INDEPENDENT-FIXED-SOURCE-SPAN-RESULT.json @@ -0,0 +1,221 @@ +{ + "status": "PASS_INDEPENDENT_FIXED_SOURCE_SPAN_TARIFF_SCREEN", + "scientific_inputs": { + "research/p112-rational-decoder-gate/CANDIDATE.json": "dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b", + "research/adaptive-kernel-demotion/inputs/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + "targets": [ + [ + 0, + 67 + ], + [ + 7, + 64 + ], + [ + 1, + 75 + ] + ], + "physical_groups": [ + 17, + 18, + 29, + 30, + 31, + 32 + ], + "complete_nonzero_types": 441, + "cost_histogram": { + "2": 1, + "3": 41, + "4": 1, + "5": 33, + "6": 197, + "7": 16, + "8": 152 + }, + "cost2_types": [ + [ + 2, + 32 + ] + ], + "cost3_types": [ + [ + 1, + 1 + ], + [ + 1, + 2 + ], + [ + 1, + 4 + ], + [ + 1, + 8 + ], + [ + 1, + 16 + ], + [ + 1, + 32 + ], + [ + 2, + 1 + ], + [ + 2, + 2 + ], + [ + 2, + 4 + ], + [ + 2, + 8 + ], + [ + 2, + 16 + ], + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 3, + 4 + ], + [ + 3, + 8 + ], + [ + 3, + 16 + ], + [ + 3, + 32 + ], + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 4, + 4 + ], + [ + 4, + 8 + ], + [ + 4, + 16 + ], + [ + 4, + 32 + ], + [ + 5, + 1 + ], + [ + 5, + 2 + ], + [ + 5, + 4 + ], + [ + 5, + 8 + ], + [ + 5, + 16 + ], + [ + 5, + 32 + ], + [ + 6, + 1 + ], + [ + 6, + 2 + ], + [ + 6, + 4 + ], + [ + 6, + 8 + ], + [ + 6, + 16 + ], + [ + 6, + 32 + ], + [ + 7, + 1 + ], + [ + 7, + 2 + ], + [ + 7, + 4 + ], + [ + 7, + 8 + ], + [ + 7, + 16 + ], + [ + 7, + 32 + ] + ], + "all_cost3_readers_singleton": true, + "multiple_reader_minimum": 4, + "canonical_term_costs": [ + 6, + 6, + 6 + ], + "ordered441rows_sha256": "e2bfae5a759a7dc2ee767f7379cb3a94cd12e81d2f8570cb0767c77941e57a1a", + "method": "Exact binary span sets and annihilator intersections; no producer imports or Gram elimination", + "scope": "Finite441type tariff facts; normalized arbitrary-term proof is written; <=5branch uses retained theorem" +} diff --git a/research/p112-no-axial-three-mark/README.md b/research/p112-no-axial-three-mark/README.md index a7f2b5f26f..31ae29474f 100644 --- a/research/p112-no-axial-three-mark/README.md +++ b/research/p112-no-axial-three-mark/README.md @@ -1,4 +1,17 @@ -# Source-density budgets for three ordinary P112 targets +# Source-span floors and density budgets for three P112 targets + +At the fixed marks `{0,67}`, `{7,64}`, `{1,75}`, the package now closes **every +rational query dictionary in their canonical span**, with arbitrary term count +and actual readers. The exact minimum is18. A complete441-type tariff table +and support-monotone normalization reduce any hypothetical cost<=17 decoder +to at most five terms; the precisely cited prior five-term theorem closes +that remaining case. The same statement holds with queries and readers +exchanged. This is an all-coefficient source-span result at one placement, +not a fixed-dictionary or coefficient-box search. + +FIXED-THREE-MARK-SOURCE-SPAN.md gives the new reduction and its exact prior +dependency. Two independent checkers rebuild all441 tariffs. The general +source-density budgets below also apply to other distinct ordinary roles. For three ordinary canonical marks in distinct paired roles, suppose every query is in their span and uses at least two marks. Restrict arbitrary actual @@ -33,22 +46,25 @@ From the repository root, Python3.12 or later, standard library only: ```sh python3 -I -O -Werror -B research/p112-no-axial-three-mark/verify.py python3 -I -O -Werror -B research/p112-no-axial-three-mark/independent.py +python3 -I -O -Werror -B research/p112-no-axial-three-mark/fixed_three_mark_source_span.py +python3 -I -O -Werror -B research/p112-no-axial-three-mark/independent_fixed_source_span.py python3 -B scripts/research_package.py --package research/p112-no-axial-three-mark ``` -Both checkers authenticate only the two foundational geometry inputs. Their +All four checkers authenticate only the two foundational geometry inputs. Their normal modes are read-only. They use different rank methods and validate the finite premises of the written proof, not the general theorem by enumeration. The12+n theorem excludes axial queries (a single marked coordinate); the -12+n-3a bound covers them after the stated normalization. Both exclude exterior +12+n-3a bound covers them after the stated normalization. The general density statements exclude exterior query directions, repeated paired roles, singleton/residual targets and -changed endpoints. It supplies no cost296 decoder, native schedule, universal +changed endpoints; the complete source-span closure fixes one placement. It supplies no cost296 decoder, native schedule, universal 334 floor or improved multiplication bound. ## Open next questions -- Can axial and dense queries share readers profitably? First use the proved normalized term cap and test the at-most441 +- Can another physical placement admit a cheaper axial/dense mixture? First check whether the complete441-type cheap-tariff obstruction also + applies there; otherwise use the normalized term cap and at-most441 exact support types at one declared placement, with cancellation constraints and invoice<=17. Blocker: support feasibility alone does not provide compatible nonzero rational coefficients or an exact endpoint. diff --git a/research/p112-no-axial-three-mark/TASK.json b/research/p112-no-axial-three-mark/TASK.json index 915f66b39c..3fd6524a75 100644 --- a/research/p112-no-axial-three-mark/TASK.json +++ b/research/p112-no-axial-three-mark/TASK.json @@ -45,20 +45,20 @@ ] }, "scope_status": "changed", - "actual_scope": "Prove a coefficient-independent12+n full-group invoice floor for no-axial queries in the span of three ordinary P112 marks from distinct paired roles, with arbitrary actual readers and restricted active term count n. Extend to axial queries after support-monotone merging: cost>=12+n-3a, giving normalized term caps8/11/14 for hypothetical cost<=17.", + "actual_scope": "Prove a coefficient-independent12+n full-group invoice floor for no-axial queries in the span of three ordinary P112 marks from distinct paired roles, with arbitrary actual readers and restricted active term count n. Extend to axial queries after support-monotone merging: cost>=12+n-3a, giving normalized term caps8/11/14 for hypothetical cost<=17. At fixedmarks{0,67},{7,64},{1,75}, prove every cost<=17 canonical-source factorization reduces to\u22645terms, via all441supporttariffs; combine with preciselycitedprior\u22645theorem to close everyrationaldictionary/termcount at thisplacement.", "scope_change_reason": "The donor-assigned rational-decoder goal and continuous literature screen led to a seven-query non-Fano gluing. A dimension/incidence proof rejects every no-axial dictionary in this three-mark scope without coefficient or invoice searches.", - "bottleneck_link": "Any six-or-more-active-term decoder in this class costs at least18. Combined with the cited prior five-term theorem, a useful three-role canonical-source candidate must include an axial query.", + "bottleneck_link": "The fixed three-mark canonical-source family has no saving at any term count; any cheaper factorization there must escape the canonical span on both sides. General density/axial budgets constrain other three-role placements.", "budget_minutes": null, "stop_rule": "Stop after the source-density proofs, two independent geometry checks, precise prior-theorem interface and focused publication. No coefficient/placement or support-feasibility census.", "outcome": "negative-result", - "evidence": "PROOF.md gives the new12+n theorem and separately states its prior-dependent all-term corollary; verify.py and independent.py certify the small binary geometry premises. AXIAL-PROOF.md gives the separately audited axial merge and term cap from the same geometry.", + "evidence": "PROOF.md gives the new12+n theorem and separately states its prior-dependent all-term corollary; verify.py and independent.py certify the small binary geometry premises. AXIAL-PROOF.md gives the separately audited axial merge and term cap from the same geometry. FIXED-THREE-MARK-SOURCE-SPAN.md and an independent proof audit establish the normalized\u22645reduction; two separate441tariffcheckers certify its premises.", "author": "flyingviper", "ai_assistance": "Substantial OpenAI Codex assistance for proof, implementation, separate-agent mathematical audit and packaging. No independent human or formal-kernel review claimed.", "open_questions": [ { - "question": "Can axial and dense queries share readers below18?", + "question": "Does the cheap-tariff obstruction close other three-role placements?", "why_it_matters": "Axial queries evade both steps in this source-density floor.", - "first_step": "Apply the proved normalized term cap to at most441 source/reader types at one declared placement, imposing exact tariffs, required-entry coverage and impossible-single-cover cancellation constraints.", + "first_step": "Check their441source/reader tariffs against the proved unique-cheap-type criterion; if it fails, use the normalized term budget and necessary cancellation constraints.", "blocked_by": "No saving identity or sufficient tariff certificate yet." }, { diff --git a/research/p112-no-axial-three-mark/VERIFY.json b/research/p112-no-axial-three-mark/VERIFY.json index 33f6bb1674..b9ea071e73 100644 --- a/research/p112-no-axial-three-mark/VERIFY.json +++ b/research/p112-no-axial-three-mark/VERIFY.json @@ -31,6 +31,30 @@ ], "timeout_seconds": 30, "checks": "Independent annihilator-set reconstruction of the geometric premises and all7770triadtriples, no producer imports." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/fixed_three_mark_source_span.py" + ], + "timeout_seconds": 30, + "checks": "All441fixed-placementtariffs,uniqueoff-axisprice2type,41singletonprice3types,axialmerge subadditivity and canonical18baseline; finitepremises for normalized\u22645reduction only." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent_fixed_source_span.py" + ], + "timeout_seconds": 30, + "checks": "Independent binaryspan/annihilator reconstruction of all441tariffs and identical complete-table digest; no producerimports. Prior\u22645theorem is separatelycited, not rerun." } ] } diff --git a/research/p112-no-axial-three-mark/fixed-three-mark-source-span.json b/research/p112-no-axial-three-mark/fixed-three-mark-source-span.json new file mode 100644 index 0000000000..50d8d6fd16 --- /dev/null +++ b/research/p112-no-axial-three-mark/fixed-three-mark-source-span.json @@ -0,0 +1,58 @@ +{ + "status": "PASS_FIXED_THREE_MARK_CANONICAL_SOURCE_GEOMETRY", + "inputs": { + "research/p112-rational-decoder-gate/CANDIDATE.json": "dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b", + "research/adaptive-kernel-demotion/inputs/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + "targets": [ + [ + 0, + 67 + ], + [ + 7, + 64 + ], + [ + 1, + 75 + ] + ], + "physical_groups": [ + 17, + 18, + 29, + 30, + 31, + 32 + ], + "coefficient_support_count": 7, + "reader_support_count": 63, + "support_types": 441, + "tariff_histogram": { + "2": 1, + "3": 41, + "4": 1, + "5": 33, + "6": 197, + "7": 16, + "8": 152 + }, + "only_cost_below3": [ + [ + 2, + 32, + 2 + ] + ], + "all_cost_at_most3_have_single_reader": true, + "minimum_two_or_more_readers": 4, + "axial_subadditivity_checks": 12288, + "canonical_term_costs": [ + 6, + 6, + 6 + ], + "table_sha256": "e2bfae5a759a7dc2ee767f7379cb3a94cd12e81d2f8570cb0767c77941e57a1a", + "proof_scope": "After readerrestriction and axialmerge, everycost<=17factorization has atmost5terms; priorfive-termtheorem is a separate cited premise for universal18floor" +} diff --git a/research/p112-no-axial-three-mark/fixed_three_mark_source_span.py b/research/p112-no-axial-three-mark/fixed_three_mark_source_span.py new file mode 100644 index 0000000000..d853e441a4 --- /dev/null +++ b/research/p112-no-axial-three-mark/fixed_three_mark_source_span.py @@ -0,0 +1,57 @@ +#!/usr/bin/env python3 +"""Fixed three-mark canonical-source floor: all441 support tariffs.""" +from pathlib import Path +from hashlib import sha256 +from collections import Counter +import argparse,json +HERE=Path(__file__).resolve().parent +PINS={'research/p112-rational-decoder-gate/CANDIDATE.json':'dc5fbe51f9cd3a14361256ac136736bffb18971d0247b891accf0d2ee060d06b','research/adaptive-kernel-demotion/inputs/DATA-PHASES.json':'c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa'} +TARGETS=[[0,67],[7,64],[1,75]] +GROUPS=[17,18,29,30,31,32] +def need(b,m): + if not b:raise ValueError(m) +def rank(vs): + pivots={} + for v in vs: + while v: + j=v.bit_length()-1 + if j in pivots:v^=pivots[j] + else:pivots[j]=v;break + return len(pivots) +def main(): + pa=argparse.ArgumentParser();pa.add_argument('--repo-root',type=Path,default=HERE.parents[1]);pa.add_argument('--write-receipt',action='store_true');args=pa.parse_args() + objs=[] + for path,h in PINS.items(): + raw=(args.repo_root/path).read_bytes();need(sha256(raw).hexdigest()==h,'inputhash');objs.append(json.loads(raw)) + c,d=objs;owner={p:i for i,g in enumerate(c['groups'])for p in g};v={r['port']:r['q']for r in d['recipes']} + need(all(t in c['factor_supports']for t in TARGETS),'canonicalmarks') + need([owner[p]for t in TARGETS for p in t]==GROUPS,'sixdistinctphysicalgroups') + groups=[c['groups'][i]for i in GROUPS] + need(all(len(g)==3 for g in groups),'ordinarytriads') + need(len({p for g in groups for p in g})==18,'disjointphysicalgroups') + for j in range(3): + ps=groups[2*j]+groups[2*j+1] + need(all((v[p]&v[q]).bit_count()%2==int(p==q)for p in ps for q in ps),'pairedroleorthonormality') + def price(s,t): + ps=[p for j in range(3)if s>>j&1 for g in groups[2*j:2*j+2]for p in g] + qs=[p for j,g in enumerate(groups)if t>>j&1 for p in g] + return rank(sum(((v[p]&v[q]).bit_count()%2)<=2)==4,'multiple-readerfloor4') + # Check all physical masks directly, including fixed-source subadditivity + # used to merge parallel axial terms; union can cancel only by shrinking. + for s in [1,2,4]: + for t in range(64): + for u in range(64):need(price(s,t|u)<=price(s,t)+price(s,u),'axialmergeranksubadditivity') + baseline=[price(1<>i&1 for p in groups[g]] + space={0} + for v in generators:space|={w^v for w in tuple(space)} + spans.append(sum(1<0 and size&(size-1)==0,'subspace cardinality') + return size.bit_length()-1 + rows=[] + for sigma in range(1,8): + source=sum(3<<(2*j) for j in range(3) if sigma>>j&1) + for reader in range(1,64): + cost=dim(spans[reader])-dim(spans[reader]&ann[source]) + rows.append([sigma,reader,cost]) + need(len(rows)==441,'complete441types') + hist=Counter(cost for sigma,reader,cost in rows) + cheap2=[[sigma,reader] for sigma,reader,cost in rows if cost==2] + cheap3=[[sigma,reader] for sigma,reader,cost in rows if cost==3] + need(min(hist)==2,'nonzero tariff floor2') + need(cheap2==[[2,32]],'unique2costtype b to c-right') + need(len(cheap3)==41 and all(reader.bit_count()==1 for sigma,reader in cheap3),'all41cost3types have singleton readers') + need(all(cost>=4 for sigma,reader,cost in rows if reader.bit_count()>=2),'multiple-reader tariff floor4') + need(all(sigma==2 for sigma,reader in cheap2),'only one axial query ray can cost2') + canonical=[next(cost for sigma,reader,cost in rows if sigma==1<=2), + 'canonical_term_costs':canonical,'ordered441rows_sha256':sha256(json.dumps(rows,separators=(',',':')).encode()).hexdigest(), + 'method':'Exact binary span sets and annihilator intersections; no producer imports or Gram elimination', + 'scope':'Finite441type tariff facts; normalized arbitrary-term proof is written; <=5branch uses retained theorem'} + payload=json.dumps(result,indent=2)+'\n';dest=HERE/'INDEPENDENT-FIXED-SOURCE-SPAN-RESULT.json' + if ar.write_receipt:dest.write_text(payload,encoding='utf-8',newline='\n') + else:need(dest.read_text(encoding='utf-8')==payload,'immutable receipt mismatch') + print(json.dumps({k:result[k] for k in ['status','complete_nonzero_types','cost_histogram','cost2_types','multiple_reader_minimum','canonical_term_costs']})) +if __name__=='__main__':main()