Document exact lookup for triple-line source complements

research/tintagel-source-lookup/CLAIM-AND-SOURCE.md

@@ -0,0 +1,80 @@
+# Claim and source ledger
+
+Checked 12 October 2026. This is a bounded overlap assessment for the
+lookup note, not a priority claim or a review of every open submission.
+
+| Item | Evidence | Scope |
+| --- | --- | --- |
+| Source form and neighboring triples | `upstream/build/sections/03-motifs.tex`, current main `db0e57bc7f36b5ac0fc844ad7ce1396165ee6647`, lines 210–230 | Original OpenAI manuscript bit label geometry, preserved in the repository maintained by Douglas Colkitt, including `G=I-J/9` and intersection-one orthogonality. |
+| Correct projection coefficient | Direct calculation from that form; local Tintagel v9 corrected proof | `V_L(j)=(3*1_{j in L}-1)/6`, not an independent new geometry result. |
+| Lookup contraction | `README.md`, adjacent-exterior proof | Paper induction over complete pivot blocks and all retained rows, using a column-a invariant rather than a unit-row claim. This is the scoped claim offered here. |
+| Finite normal forms | `replay.py` | 1,936 exact rational cases, 20/17 alphabet, 65,416 word records, 11,584 pivots. This computation does not prove the contraction lemma. |
+| Corroboration | `replay.py --stress`; unpublished local v9 review | 6,090 h=7–9 compressed cases are publicly replayable here. The local review reports another 6,984 operation-level deletions in 6,510 h=3–9 matrices; that separate check is not reproduced in this patch. |
+| Rank and reference termination | `README.md` projector calculation and ordered reference | `rank A=h-r`; exactly `h-r` pivots in `h` row iterations. No physical execution claim. |
+| Physical provider | Local v9 independent re-review | **Not linked** above Q=11 at the recursive pivot branch; full h=5/h=100 source graphs had structural validation only. |
+
+The frozen local Tintagel v9 archive has SHA256
+`1978c40c7b5f23a818096df10f713e23d95b7f27a1e97550093d2ce3e02cbb09`.
+Its unpublished independent re-review on 12 October 2026 accepted the corrected
+coefficient, all-row contraction, and finite replay while explicitly
+rejecting any inference of a full provider or Lean proof. The earlier
+v1/v2 prose contained incorrect coefficient and zero-row claims; this
+note uses the corrected v3 proof only. The review is local provenance,
+not a public theorem certification.
+
+A separate bounded Claude Opus review on 12 October 2026 requested the
+explicit Gram/projection derivation, pivot-row and rank reasoning, and
+the computer-assisted label now in `README.md`. It also suggested the
+false stronger statement \(\text{row }b=-e_a\), which an independent
+exact-commit publication review refuted at \(h=5,S=\{0,1,2\}\).
+The exported proof now keeps only the weaker column-\(a\) invariant;
+`replay.py` checks the counterexample as a regression. Opus
+**did not run** `replay.py` or verify
+the 65,416 records, digest, or 20/17 alphabet; those facts rely on the
+local replay and remain independently executable from this patch. The
+exact-commit reviewer separately replayed the 1,936-case checker and
+confirmed the finite counts, but the all-height step remains the
+paper induction. These reviews support scrutiny, not formal certification.
+
+## Overlap checked
+
+The existing clean source mirror's receipt 224 observed CrocSwap main at
+`db0e57bc7f36b5ac0fc844ad7ce1396165ee6647`. An exact text search
+of that tree found no `Tintagel`, `gap skeleton`, or all-retained-row
+lookup proof. Current GitHub PR title/body searches for `Tintagel`,
+`lookup`, `gap skeleton`, and source-complement language found no matching
+submission. [PR #390](https://github.com/CrocSwap/integer-mult-bounds/pull/390)
+is the related heterogeneous-bank proposal;
+[PR #430](https://github.com/CrocSwap/integer-mult-bounds/pull/430)
+audits its physical interface and B3 composition. Neither supplied the
+adjacent-exterior lookup proof in its reviewed description. An exact
+source and proof comparison of every open PR was not performed, so this
+supports a narrow contribution claim, not exclusivity or priority.
+
+Receipt 224 also records [PR #576](https://github.com/CrocSwap/integer-mult-bounds/pull/576)
+advancing to `f4e9f7e85e9211cf6ba6c5789da2aa0902d9121e`. Its
+one-commit old-to-new comparison lists only an owner assignment archive,
+plan, witness specification, and manifest. The visible diff has no
+lookup contraction, source-factor table, or one-cell interface code.
+The compressed owner archive's contents were not inspected. This is
+limited negative overlap evidence; this note does not depend on those
+assignments.
+
+The current repository README still advertises a **conditional**
+integer-multiplication record and lists all-size compiler and physical
+interfaces as assumptions. This note must not be read as resolving
+those assumptions. The local v9 source graph stops at
+`branch_number(builder, 'Q', {11: base_edge})` for a Q>11 rank-one
+pivot. Its successful h=100 graph compilation is structural, not a
+successful full source-bank run. The fixed-source-\(W\) grouping scope,
+S0-transformed-input premise, and exceptional terms remain intact.
+
+## Replay and review rule
+
+Run `python3 -I -B research/tintagel-source-lookup/replay.py --stress`.
+Check the paper induction separately. Treat certificate success,
+conditional mathematical arguments, structural graph compilation,
+finite physical runs, and formal proofs as different evidence classes.
+The public patch contains only the lookup note and a standard-library
+exact checker. It imports no confidential transcripts or downstream
+machine code and changes no selected bound or source pin.

research/tintagel-source-lookup/README.md

@@ -0,0 +1,178 @@
+# Exact lookup for triple-line source complements
+
+This note isolates one bounded part of the source-factor compiler for the
+bit construction in `upstream/build/sections/03-motifs.tex`: the exact
+rational alphabet of its ordered elimination. The source form, triple
+lines, and neighboring relation come from the pinned original OpenAI
+manuscript preserved under `upstream/` in this repository, maintained by
+Douglas Colkitt. The upstream motif section credits the underlying
+degree-one intersection construction to Alon (1998, Section 3,
+remark after Theorem 1.1).
+The contraction argument and certificate below were developed in an
+unpublished local Tintagel audit packet. The complete proof and checker
+needed for this scoped claim are reproduced here. This contribution
+does not assert a new multiplication exponent or a physical provider.
+
+## Statement
+
+Let \(h\geq3\) (\(h\geq5\) if \(T\) is present), let
+\(S\subseteq\{0,\ldots,h-1\}\) have size three, and optionally let
+\(T\) also have size three with \(|S\cap T|=1\). Set
+\(G=I-J/9\) and \(u_L=1_L\) for each chosen triple. For \(r=1\) or \(2\),
+form \(U=[u_S]\) or \(U=[u_S,u_T]\) and \(V_L(j)=(3\,1_{j\in L}-1)/6\).
+The rational source complement is \(A=I-UV^{\mathsf T}\). Process rows in
+ascending order, choosing the **rightmost nonzero unused column** of each
+row. For a pivot \(p=A_{i,c}\), update nonzero earlier unused columns
+\(j<c\) by \(C_j\leftarrow C_j-A_{i,j}C_c/p\), clear nonzero entries below
+the pivot with row operations, then normalize the pivot row. Record the
+initial matrix, every completed scalar update, pivot, and operation
+coefficient. `replay.py` specifies this exact reference order.
+
+**Computer-assisted theorem, conditional on that reference semantics.** For every
+such \(h,S,T\), all recorded matrix values belong to the 20-element
+`VALUES` table and all nonzero column, row, and normalization
+coefficients belong to the 17-element `COEFFICIENTS` table in `replay.py`.
+The reference processes exactly \(h\) rows and has \(h-r\) pivots. In
+particular this applies to every valid \(h=100\) one-line or neighboring
+two-line source input. This is an exact-rational statement about the
+reference and lookup domain. It is not a Lean theorem or an execution of
+all physical input tapes.
+
+## Projector and rank
+
+Since \(Gu_L=u_L-\mathbf1/3\) and
+\(u_K^{\mathsf T}Gu_L=|K\cap L|-1\), the selected line Gram matrix is
+\(U^{\mathsf T}GU=2I_r\). The corresponding projection coefficient is
+\(V_L=Gu_L/2\). For any triples \(L,K\),
+\[
+V_L^{\mathsf T}u_K=(|L\cap K|-1)/2.
+\]
+Thus \(V^{\mathsf T}U=I_r\), including the neighboring two-line case.
+Consequently \(A^2=A\), \(\ker A=\operatorname{im}U\), and
+\(\operatorname{rank}A=h-r\). The coefficient is \(+1/3\) inside a
+triple and \(-1/6\) outside; the latter sign means an exterior column
+starts as \(e_j+(u_S+u_T)/6\) in the two-line case. These signs matter
+to the contraction below. This projector identity does not rely on
+nondegeneracy of the ambient form at every auxiliary height.
+
+At each pivot, updates to unused columns left of the chosen column
+zero the pivot-row entries there. Entries to its right are zero by
+the rightmost rule, while previously pivoted columns were already
+cleared below. The pivot row is therefore exactly \(p e_c\) after
+the column updates. Each row clear changes only column \(c\) in the
+target row. Column updates, row clears and normalization preserve
+rank; the final matrix is a partial permutation matrix with one unit per pivot.
+Its rank is thus the pivot count \(h-r\). The reference loops over
+exactly \(h\) rows.
+
+## Adjacent-exterior contraction
+
+Call indices outside \(S\cup T\) *exterior*. Let \(a<b=a+1\) be
+adjacent exterior indices. Compare the full elimination with the run
+obtained by deleting coordinate \(a\) and order-preservingly relabeling
+the rest. The comparison is made after complete pivot blocks, not in
+the middle of separate column updates.
+
+Before row \(a\), induction over earlier complete blocks gives:
+
+1. Row \(a\) remains \(e_a\) and column \(a\) has not pivoted.
+2. If column \(b\) is unused, row \(b\) remains \(e_b\); columns \(a,b\)
+   agree at **every other retained row**, including transformed exterior
+   rows.
+3. If column \(b\) has pivoted, its row \(b\) has entry \(-1\) in
+   column \(a\); all other rows outside \(a,b\) have zero there.
+
+Initially these properties follow from the exterior-column formula.
+The full matrix's initial extra row and column entries are already
+in the contracted initial matrix or among \(0,1\).
+An earlier pivot column \(c<a\) does not target \(a,b\). When \(c>b\),
+their equal entries in the pivot row force equal column coefficients
+while \(b\) is unused; row \(a,b\) have zero in \(c\), so clearing below
+does not change them. The rightmost rule therefore cannot select \(a\)
+while \(b\) remains an eligible identical entry. If \(c=b\), the
+column-\(a\) coefficient is \(-1\); it clears column \(a\) in every
+other retained row and leaves \(-1\) in row \(b\). The ensuing
+row-\(b\) clear removes the pivot-column entry there and leaves its
+column-\(a\) entry equal to \(-1\); its other retained entries need
+not be zero. Later earlier-row blocks preserve this column-\(a\)
+invariant: every earlier candidate pivot row has zero in column
+\(a\), so it neither pivots there nor makes a column update targeting
+it; row clears also preserve that column's entries. This rules out a
+pivot at \(a\) after \(b\) has pivoted.
+There is no pivot index strictly between
+\(a\) and \(b\).
+
+The column condition must not be strengthened to a unit-row claim.
+For \(h=5\), \(S=\{0,1,2\}\), \(a=3\), \(b=4\), the first pivot is
+\((0,4)\), and its complete block leaves row \(4\) equal to
+\((-4,2,2,-1,0)\), not \(-e_3\). `replay.py` checks this exact
+counterexample. Every later use above and below concerns column \(a\)
+or entries retained after deleting \(a\); neither requires the other
+entries of row \(b\) to vanish.
+
+At row \(a\) the pivot value is \(1\). Its block changes no retained
+matrix entry. If \(b\) is unused, the row-\(a\) clear at each later row
+uses \(-A_{i,b}\), exactly the coefficient of the contracted row-\(b\)
+block. This includes previously transformed exterior rows. If \(b\)
+has pivoted, only row \(b\) has a nonzero entry in column \(a\), and
+the clear has coefficient \(+1\). Prior column updates targeting \(a\)
+duplicate the corresponding column-\(b\) arithmetic or use \(-1\);
+normalization adds only \(0,1,-1\). The omitted typed block consists of
+column updates targeting \(a\), row-\(a\) clears, row-\(a\)
+normalization, and its pivot marker. Omitting only the marker would not
+give the contracted run. After deleting that block, retained matrix
+states, later pivot choices, and operations agree in order. The full
+run's extra values and coefficients are therefore either in the
+contracted run or among \(0,1,-1\).
+
+Delete the left member of every adjacent exterior pair until each gap
+before, between, and after support indices retains at most one exterior
+index. This is a height-independent induction. A one-line support has
+three labeled positions and four gaps, giving \(2^4=16\) forms. A
+two-line support has five positions labeled one intersection `X`, two
+`A` only, and two `B` only: \(5!/(2!2!)=30\) orders and \(2^6=64\) gap
+masks, giving 1,920 forms. Every normal form has height at most 11.
+
+## Finite certificate and replay
+
+Run from the repository root with Python 3 and no package installation:
+
+```sh
+python3 -I -B research/tintagel-source-lookup/replay.py --stress
+```
+
+The script constructs all 1,936 forms over exact `Fraction` values and
+checks the explicit 20/17 tables, 65,416 word records, 11,584 pivots,
+and digest `adf555d553a11c9f2862ddf6a7206fd03428ec657763f60f9aecfc6d4850ec7d`.
+It also checks the nonunit row-\(b\) counterexample to guard the proof
+against an invalid strengthening of the column invariant.
+The optional stress flag checks all 6,090 neighboring two-line inputs
+at heights 7–9 against their compressed forms. The stress is finite
+corroboration; the induction supplies the all-height step. The program
+records completed scalar updates, so it does not certify the internal
+states or time of a machine implementation of rational arithmetic.
+
+## Scope and provenance
+
+The base triple-line geometry and source schedule are attributed to
+the cited original OpenAI manuscript and its upstream references;
+Douglas Colkitt maintains the repository and its community research.
+The local v9
+Tintagel packet, frozen at SHA256
+`1978c40c7b5f23a818096df10f713e23d95b7f27a1e97550093d2ce3e02cbb09`,
+contains the corrected sign and all-row contraction proof. An
+independent local audit accepted that paper argument and separately
+replayed the finite certificate. This unpublished provenance is not
+itself publicly reproducible; the argument and exact checker needed
+for the present claim are included here. See `CLAIM-AND-SOURCE.md` for
+evidence boundaries.
+This package was prepared with substantial AI assistance.
+
+The result only closes the exact source lookup for the specified
+one/two-line complements. General-width setup, the recursive Q>11
+pivot child, heterogeneous bank consumer, packed entry, arbitrary
+phase/native/root composition, physical cost, and all-size physical
+execution remain open. The broader fixed-\(W\) grouping, its
+S0-transformed-input premise, and exceptional
+\(M A^3+\delta M A(R+A)\) terms are not addressed by this note. No global
+multiplication theorem or new \(\kappa\) follows from this note.