diff --git a/ComplexityTheory.lean b/ComplexityTheory.lean index c530c3c..57e3668 100644 --- a/ComplexityTheory.lean +++ b/ComplexityTheory.lean @@ -28,6 +28,7 @@ import ComplexityTheory.ProofComplexity.CanonicalOpening.Step import ComplexityTheory.ProofComplexity.CanonicalOpening.FiniteStrategy import ComplexityTheory.ProofComplexity.CanonicalOpening.AffineBinding import ComplexityTheory.ProofComplexity.CanonicalOpening.AffineBinding.Exact +import ComplexityTheory.ProofComplexity.CanonicalOpening.FourAxisAffine import ComplexityTheory.ProofComplexity.CanonicalOpening.FourAxisSplicing import ComplexityTheory.ProofComplexity.CanonicalOpening.LinearContraction import ComplexityTheory.ProofComplexity.CanonicalOpening.NearFar diff --git a/ComplexityTheory/ProofComplexity/CanonicalOpening/FourAxisAffine.lean b/ComplexityTheory/ProofComplexity/CanonicalOpening/FourAxisAffine.lean new file mode 100644 index 0000000..ec61aaf --- /dev/null +++ b/ComplexityTheory/ProofComplexity/CanonicalOpening/FourAxisAffine.lean @@ -0,0 +1,171 @@ +/- +Copyright (c) 2026 Windsor Nguyen and contributors. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Windsor Nguyen +-/ + +import ComplexityTheory.ProofComplexity.CanonicalOpening.AffineBinding.Exact +import Mathlib.Logic.Equiv.Fin.Basic + +/-! +# Exact affine opening from four tensor axes to two + +This module instantiates the four-coordinate affine binder with the four block +contractions of a `2 x 2 x 2 x 2` tensor. A three-bit message is fixed before +one two-bit public challenge. Every nonterminal result contains a tensor with +exactly two active indices. + +The theorem is semantic. In particular, the two-index function type does not +prove that a compiler copies four field elements instead of retaining a closure +over the parent tensor; an operational resource theorem must establish that +representation separately. +-/ + +namespace ComplexityTheory +namespace CanonicalOpening +namespace FourAxisAffine + +open scoped BigOperators +open FourCoordinateAffineBinding + +/-- One binary tensor axis. -/ +abbrev Axis := Fin 2 + +/-- A four-axis binary tensor opening claim. -/ +structure Open4 where + /-- The canonical four-axis tensor. -/ + tensor : Axis → Axis → Axis → Axis → BinaryField + /-- The public weight on the first axis. -/ + firstWeight : Axis → BinaryField + /-- The public weight on the second axis. -/ + secondWeight : Axis → BinaryField + /-- The public weight on the third axis. -/ + thirdWeight : Axis → BinaryField + /-- The public weight on the fourth axis. -/ + fourthWeight : Axis → BinaryField + /-- The claimed weighted contraction. -/ + claimed : BinaryField + +/-- The outer two-axis coefficient vector, flattened lexicographically. -/ +def outerWord (claim : Open4) : Word := fun coordinate => + let outer := finProdFinEquiv.symm coordinate + claim.firstWeight outer.1 * claim.secondWeight outer.2 + +/-- The four canonical contractions of the inner two-axis slices. -/ +def canonicalBlockWord (claim : Open4) : Word := fun coordinate => + let outer := finProdFinEquiv.symm coordinate + ∑ third, ∑ fourth, + claim.tensor outer.1 outer.2 third fourth * + claim.thirdWeight third * claim.fourthWeight fourth + +/-- The associated four-coordinate affine binding claim. -/ +def Open4.toAffineClaim (claim : Open4) : FourCoordinateAffineBinding.Claim where + linear := outerWord claim + canonical := canonicalBlockWord claim + claimed := claim.claimed + +/-- A four-axis claim is true when its associated weighted contraction is canonical. -/ +def Open4.True (claim : Open4) : Prop := + claim.toAffineClaim.True + +/-- A two-axis tensor opening emitted by one outer-coordinate challenge. -/ +structure Open2 where + /-- The challenged two-axis tensor slice. -/ + tensor : Axis → Axis → BinaryField + /-- The public weight on the first remaining axis. -/ + firstWeight : Axis → BinaryField + /-- The public weight on the second remaining axis. -/ + secondWeight : Axis → BinaryField + /-- The claimed weighted contraction of the slice. -/ + claimed : BinaryField + +/-- A two-axis child is true when its weighted slice contraction is canonical. -/ +def Open2.True (claim : Open2) : Prop := + claim.claimed = ∑ first, ∑ second, + claim.tensor first second * claim.firstWeight first * claim.secondWeight second + +/-- Construct the two-axis child selected by one flattened outer coordinate. -/ +def child (parent : Open4) (coordinate : Coordinate) (claimed : BinaryField) : Open2 := + let outer := finProdFinEquiv.symm coordinate + { tensor := fun third fourth => parent.tensor outer.1 outer.2 third fourth + firstWeight := parent.thirdWeight + secondWeight := parent.fourthWeight + claimed } + +/-- Child truth is exactly equality with the corresponding canonical block value. -/ +theorem child_true_iff (parent : Open4) (coordinate : Coordinate) + (claimed : BinaryField) : + (child parent coordinate claimed).True ↔ + claimed = canonicalBlockWord parent coordinate := by + rfl + +/-- +Execute the four-to-two fold by decoding one global block word and emitting the +challenged two-axis slice. The prover sends no post-challenge response. +-/ +def step (parent : Open4) (syndrome : Syndrome) (coordinate : Coordinate) : + OpeningStepResult Open2 := + if hNonzero : outerWord parent ≠ 0 then + .child (child parent coordinate + (decode (outerWord parent) hNonzero syndrome parent.claimed coordinate)) + else if parent.claimed = 0 then .accept else .reject + +/-- The honest message is the checksum of the four canonical block contractions. -/ +def honestSyndrome (parent : Open4) : Syndrome := + FourCoordinateAffineBinding.honestSyndrome parent.toAffineClaim + +/-- The affine four-axis fold is an exact opening step with two-axis children. -/ +def exactStep : ExactOpeningStep Open4 Syndrome Coordinate Open2 where + parentTrue := Open4.True + childTrue := Open2.True + honestProof := honestSyndrome + step := step + complete parent hTrue coordinate := by + by_cases hNonzero : outerWord parent ≠ 0 + · have hDecoded := decode_checksum (outerWord parent) hNonzero + (canonicalBlockWord parent) + change parent.claimed = dot (outerWord parent) (canonicalBlockWord parent) at hTrue + rw [← hTrue] at hDecoded + have hHonest : honestSyndrome parent = + checksum (outerWord parent) hNonzero (canonicalBlockWord parent) := by + simp [honestSyndrome, FourCoordinateAffineBinding.honestSyndrome, + Open4.toAffineClaim, hNonzero] + rw [hHonest] + simp [step, hNonzero, hDecoded, child_true_iff, + OpeningStepResult.PreservesTrue] + · have hLinear : outerWord parent = 0 := not_ne_iff.mp hNonzero + have hClaimed : parent.claimed = 0 := by + change parent.claimed = dot (outerWord parent) (canonicalBlockWord parent) at hTrue + simpa [hLinear, dot] using hTrue + simp [step, hNonzero, hClaimed, OpeningStepResult.PreservesTrue] + falseDescent parent hFalse syndrome := by + by_cases hNonzero : outerWord parent ≠ 0 + · let decoded := decode (outerWord parent) hNonzero syndrome parent.claimed + have hDecodedValue : dot (outerWord parent) decoded = parent.claimed := + dot_decode (outerWord parent) hNonzero syndrome parent.claimed + have hDifferent : decoded ≠ canonicalBlockWord parent := by + intro hEqual + apply hFalse + exact hDecodedValue.symm.trans (congrArg (dot (outerWord parent)) hEqual) + have hCoordinate : + ∃ coordinate, decoded coordinate ≠ canonicalBlockWord parent coordinate := by + by_contra hNoCoordinate + apply hDifferent + funext coordinate + by_contra hAtCoordinate + exact hNoCoordinate ⟨coordinate, hAtCoordinate⟩ + obtain ⟨coordinate, hAtCoordinate⟩ := hCoordinate + exact ⟨coordinate, by + simp [step, hNonzero, decoded, child_true_iff, + OpeningStepResult.ExposesFalse, hAtCoordinate]⟩ + · have hLinear : outerWord parent = 0 := not_ne_iff.mp hNonzero + have hClaimed : parent.claimed ≠ 0 := by + intro hZero + apply hFalse + simp [Open4.True, Open4.toAffineClaim, Claim.True, hLinear, hZero, dot] + exact ⟨0, by + simp [step, hNonzero, hClaimed, OpeningStepResult.ExposesFalse]⟩ + +end FourAxisAffine +end CanonicalOpening +end ComplexityTheory