diff --git a/docs/research/canonical-opening-experiments.md b/docs/research/canonical-opening-experiments.md index c6cd4f4..6e2a7bb 100644 --- a/docs/research/canonical-opening-experiments.md +++ b/docs/research/canonical-opening-experiments.md @@ -129,7 +129,7 @@ construction must use a proximity interaction that produces a different compressed child, or make dense checksum rows locally accessible by some additional algebraic mechanism. -## First finite synthesis result +## Radius-one classification We exhaustively enumerated binary linear checksum matrices for three-bit words at decoding radius one. Lean verified: @@ -154,9 +154,88 @@ every one-row matrix has two distinct equal-checksum words within radius one of a common center. The latter theorem is a complete finite cheating certificate, not merely a failed search result. +The later symbolic proof explains the search result. Hamming's binary +condition uses nonzero, pairwise-distinct check columns (1950, Section 3, +pp. 150-154). Lean proves the finite-field projective generalization: +radius-one unique decoding holds exactly when every checksum column is nonzero +and no two columns are proportional. It also proves the Hamming inequality + +```text +1 + input columns * (field order - 1) + <= field order ^ checksum rows. +``` + +For a binary checksum this becomes `n <= 2^r - 1`. The finite count remains a +useful exhaustive regression test. + +## The first four-axis candidate exposed response splicing + +The first `2 x 2 x 2 x 2` experiment allowed one global word for the checksum +audit and separate answers for coordinate openings. Its checksum was genuinely +radius-one unique-decoding, so checksum quality was not the defect. + +For the all-zero canonical tensor and false claimed total one, the prover uses + +```text +global response = (1, 1, 1, 0) +local responses = (0, 0, 0, 0). +``` + +The global word lies in the checksum kernel and has odd total, while every +local response is canonical. Lean verifies this explicit strategy and also +exhaustively finds a cheating strategy. The generic theorem +`safeForEveryChallenge_iff` identifies the pattern: independently safe global +and local responses splice whenever the commitment does not bind them to one +candidate. + +This negative result covers only the separated-response grammar. It is not a +barrier against commitments or proximity protocols. + +## Three bits bind the finite affine fold exactly + +The corrected protocol sends no response after the challenge. For any nonzero +binary linear functional `ell` on four block values, Lean constructs a +three-bit checksum with a kernel vector `kappa` satisfying + +```text +Hamming weight kappa >= 3 +dot ell kappa = 1. +``` + +The syndrome and public claimed bit are four independent equations, so they +decode one global block word. A true parent uses the checksum of its canonical +word. For a false parent, every syndrome decodes a different word, and some +coordinate challenge emits a false child. + +The library now retains three distinct receipts: + +- executable finite search finds no cheating strategy for any four-coordinate + claim; +- `FourCoordinateAffineBinding.exactStep` proves exactness symbolically; and +- `FourAxisAffine.exactStep` instantiates the result for an explicit + `2 x 2 x 2 x 2` tensor and emits a two-axis tensor claim. + +The last theorem is semantic. It does not prove that compiled Lean code copies +four field elements into the child or avoids retaining a closure over the +parent tensor. + +## Why the positive primitive does not scale + +An affine equation on `n + 1` binary coordinates leaves `n` free coordinates. +Lean proves that a deterministic no-response decoder representing every +solution needs at least `2^n` messages. When the messages are `r`-bit strings, +it derives `n <= r`. + +Thus the three-bit four-coordinate binder is cardinality-optimal but cannot +compress an arbitrary exponentially larger block vector to square-log size. +The lower bound assumes every affine solution must be representable; it does +not cover structured canonical tensors or additional interaction. + ## Next falsifiable step -The next candidate must combine this checksum binding with an executable -localization rule that exposes a row defect in the far case. It succeeds only -if the emitted child is smaller than the parent without sending all slice -values. Otherwise the product barrier applies unchanged. +The finite correctness interface is no longer missing. The remaining candidate +must beat the `n - 1` message barrier by exploiting structure in canonical +tensors or by using a charged far-case proximity interaction. It must also +connect the semantic two-axis child to an executable representation and full +resource profile. Otherwise the affine cardinality or local-slice product +barrier applies unchanged. diff --git a/docs/research/canonical-opening-theorem-index.md b/docs/research/canonical-opening-theorem-index.md index b78189a..a936e5a 100644 --- a/docs/research/canonical-opening-theorem-index.md +++ b/docs/research/canonical-opening-theorem-index.md @@ -125,6 +125,20 @@ Hamming radius `d` of one center have different checksums. Lean proves: These are binding statements. They neither show that a candidate is near the canonical word nor locate an error in a far candidate. +Hamming (1950, Section 3, pp. 150-154) gives the binary nonzero, +pairwise-distinct-column condition. At radius one over a finite field, Lean +proves its projective generalization: + +```text +unique decoding + iff +all columns are nonzero and no two are proportional. +``` + +Lean proves the exact cardinal inequality `1 + n*(q - 1) <= q^r`; the binary +specialization is `n <= 2^r - 1`. These finite-field bounds do not supply a +proximity test or a local implementation of a dense checksum row. + If a checksum alone exactly decodes every coordinate of every word, Lean proves that the checksum is injective. Hence a shorter binary checksum cannot exactly decode every longer binary word without additional information or interaction. @@ -153,11 +167,87 @@ For three-bit binary words at radius one, exhaustive evaluation proves that: - exactly six two-row matrices succeed; and - every one-row matrix has a checked collision witness. -This is a complete finite certificate for that parameter choice. It is not the -general Hamming-code classification and carries no asymptotic lower bound. +This is a complete finite certificate for that parameter choice. The later +projective classification explains the six survivors symbolically. The count +remains a regression test rather than an independent asymptotic result. + +## Near-far composition + +`NearFarFold` separates a unique-decoding checksum, a canonical object, a local +validity predicate, and an explicit proximity opening step. Lean proves that an +invalid canonical object is far from every valid object in its checksum fiber +and that an exact proximity step can be reinterpreted as an exact parent step. + +The interface does not construct the proximity step. In particular, it does +not justify replacing a prover-selected checksum with the canonical checksum, +or permit an uncharged oracle for deciding proximity. + +## Unbatched tensor accounting + +`unbatchedTensorOpening_not_clockClosing` proves that the sufficient inequality +`Lambda^t < t` is impossible when `2 <= Lambda`. The companion winner-cost +theorem states the corresponding natural-number mass bound. + +These results apply only to the audited unbatched tensor protocol composed with +the current multiplicative-round compiler certificate. They are not lower +bounds against arbitrary winner algorithms or tensor protocols. + +## Finite strategy checking and response splicing + +`hasCheatingOneStepStrategy` exhaustively decides whether a finite false parent +has one proof safe under every challenge. The checker proves the Boolean result +equivalent to the named existential proposition; candidate modules retain an +explicit witness in addition to the search result. + +`SeparatedResponseStrategy.safeForEveryChallenge_iff` exposes the exact +splicing seam: if the global response and each local response are independently +safe under one commitment, they combine into a strategy safe for every +challenge. + +`FourAxisSplicing` instantiates this grammar with a valid radius-one checksum. +For the zero `2 x 2 x 2 x 2` tensor and false top value one, the global branch +uses the odd checksum-kernel word `(1, 1, 1, 0)` while every local branch uses +the canonical zero word. Lean checks both the explicit strategy and the +exhaustive search result. This refutes only protocols that fail to bind the +global and local responses to one candidate. + +## Exact four-axis affine fold + +`FourCoordinateAffineBinding` gives a positive no-response baseline. For every +nonzero linear functional on four binary coordinates, it constructs a +three-bit radius-one checksum whose kernel vector has weight at least three and +affine value one. The public claimed bit plus the syndrome uniquely decodes one +four-coordinate word. + +Lean proves the decoder equations, radius-one checksum property, exhaustive +absence of a cheating finite strategy, and an `ExactOpeningStep` theorem. The +tensor instantiation `FourAxisAffine.exactStep` groups a +`2 x 2 x 2 x 2` tensor into four inner-slice contractions; one public +coordinate challenge emits a two-axis child. There is no prover response after +the challenge. + +This is semantic four-to-two shrinkage. The `Open2` type has two indices, but no +current theorem connects its Lean representation to an implementation that +copies exactly four field elements or avoids retaining a closure over the +parent tensor. + +## Affine-binding cardinality barrier + +`messageCardinality_ge_twoPow_freeCoordinates` assumes a deterministic decoder +represents every solution of one binary affine equation on `n + 1` +coordinates. Lean proves that its message space has at least `2^n` elements. +For an `r`-bit message, `binaryMessageLength_ge_freeCoordinates` gives +`n <= r`. + +The coverage assumption is essential. This theorem does not cover a structured +subset of canonical words, a probabilistic or interactive binder, or a +protocol whose later messages contribute binding information. ## Open boundary -The missing primitive must combine near-case checksum binding with a charged -far-case proximity argument that either rejects or emits a genuinely smaller -false child. No current theorem supplies that primitive. +The exact four-to-two affine fold is an optimal finite correctness baseline, +but its direct `n`-coordinate generalization transmits at least `n - 1` bits. +The remaining asymptotic primitive must therefore exploit structure in the +canonical tensors or combine a shorter checksum with a charged proximity +interaction. No current theorem supplies square-log compression, an +operational resource realization, or evidence for `P != NP`.