docs(research): record affine opening boundary

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.

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`.