P112: exclude every canonical-source decoder at a fixed three-target placement

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.

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.

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.

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.