SourceSignaturePrepareLemmas.lean`

86 declarations, 0 contain sorry, 0 declared as axioms

The actual numbered equation list has exactly the acceptance bounded by the private Fourier decoder. Only the repeated base-game value is an input here; list semantics and all finite sampling laws are supplied.

abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.Width line 15
abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.Arena line 16
abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.ProfileState line 17
abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.State line 18
abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.ProfileLabel line 19
inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.Label line 21
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.variableField line 28
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.polarityField line 31
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.place line 34
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.unplace line 38
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.unplace_place line 48
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.place_injective line 61
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.place_unplace line 66
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.fill line 98
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.fill_place line 104
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.fill_self line 109
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.fill_frame line 117
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.fill_update line 124
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.placedLabel line 147
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.placedConfiguration line 151
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.placedStatement line 157
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.placed_stepAux line 172
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.signStateEquiv line 200
Source documentation
Reassociate finite registers without adding a transition.
```
def signStateEquiv (u : ℕ) (τ : Type) :
    SourceSignLoad.State u (ProfileState u × τ) ≃ State u τ where
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignLoad.State, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.ProfileState, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.State
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.commitStatement line 207
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.program line 213
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.placed_step line 218
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.stepAux_commit line 235

def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.profileInTime line 248

Source documentation

The actual profile execution, placed in the loaded context arena.

def profileInTime (tapes : Arena u Extra → List Bool)
    (hwork : ∀ w : Fin 3, tapes (place (.inr w)) = [])
    (initialProfile : MachineFieldProfile.Profile (Width u))
    (initial : Signature u) (ambient : τ) (L : ℕ)
    (hL : ∀ i, (tapes (place (.inl i))).length ≤ L) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (.profile (MachineFieldProfile.labelAt (MachineFieldProfile.allPairs (Width u)) 0 0)),
        (MachineFieldProfile.normalState initialProfile, (initial, ambient)), tapes⟩
      (some ⟨some .commit,
        (MachineFieldProfile.normalState
          (MachineFieldProfile.equalityProfile (fun i => tapes (place (.inl i)))),
          (initial, ambient)), tapes⟩)
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.Arena, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.place, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.Width, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.program

def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.commitInTime line 268

def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.prepareInTime line 283

Source documentation

Actual preparation from isolated name fields and unary sign fields. The conclusion preserves every tape and arbitrary caller metadata.

def prepareInTime (F : Formula) (c : ClauseContext F u) (selected : SlotContext u)
    (tapes : Arena u Extra → List Bool)
    (hwork : ∀ w : Fin 3, tapes (place (.inr w)) = [])
    (hnames : ∀ i, tapes (place (.inl i)) = nameWords F c i)
    (suffix : Position u → List Bool)
    (hsigns : ∀ p, tapes (polarityField p) =
      encodeWord (if positiveAt (clauseAt F (c p.1)) p.2 then 1 else 0) ++ suffix p)
    (initialProfile : MachineFieldProfile.Profile (Width u))
    (initial : Signature u) (hselected : initial.selected = selected) (ambient : τ) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (.profile (MachineFieldProfile.labelAt (MachineFieldProfile.allPairs (Width u)) 0 0)),
        (MachineFieldProfile.normalState initialProfile, (initial, ambient)), tapes⟩
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.Arena, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.place, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.polarityField, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.Width, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.program

theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.loaded_name_field line 322
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.loaded_sign_field line 341
Source documentation
Unary sign fields may retain arbitrary old suffixes: only the leading sign bit is read.
```
theorem loaded_sign_field (F : Formula) (c : ClauseContext F u)
    (base : Arena u Extra → List Bool) (p : Position u) :
    SourceContextLoad.stageTapes F c base u (polarityField p) =
      encodeWord (if positiveAt (clauseAt F (c p.1)) p.2 then 1 else 0) ++
        base (polarityField p) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.Arena, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.stageTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.polarityField

def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.loadedPrepareInTime line 356

Source documentation

Exactly the loaded context signature is computed by the concrete finite program. Scratch is reset and all loaded fields and caller tapes are preserved.

def loadedPrepareInTime (F : Formula) (c : ClauseContext F u) (selected : SlotContext u)
    (base : Arena u Extra → List Bool)
    (hindex : base .index = []) (hwork : base .work = []) (hscratch : base .scratch = [])
    (hbase : ∀ p : Position u, base (variableField p) = [])
    (initialProfile : MachineFieldProfile.Profile (Width u))
    (initial : Signature u) (hselected : initial.selected = selected) (ambient : τ) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some (.profile (MachineFieldProfile.labelAt (MachineFieldProfile.allPairs (Width u)) 0 0)),
        (MachineFieldProfile.normalState initialProfile, (initial, ambient)),
        SourceContextLoad.stageTapes F c base u⟩
      (some ⟨none,
        (MachineFieldProfile.normalState (MachineFieldProfile.equalityProfile (nameWords F c)),
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.Arena, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.variableField, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.Width, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.stageTapes

def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.machine line 388
Source documentation
Finiteness of tape addresses and registers constructs an actual TM2; its execution bound is established above by the concrete transitions.
```
def machine (u : ℕ) (Extra τ : Type) [DecidableEq Extra] [Fintype Extra] [Fintype τ]
    (initialProfile : MachineFieldProfile.Profile (Width u))
    (initial : Signature u) (ambient : τ) : FinTM2 where
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.Width
abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.Arena line 408
abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.LoadState line 409
abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.PrepareState line 410
abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.State line 411
abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.Label line 412
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.prepareEntry line 416
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.stateSwap line 420
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.program line 423
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.preparationConfiguration line 429
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.preparation_step line 437
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.initialState line 456
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.finalState line 460
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.loadInTime line 465
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.signatureInTime line 486
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.prepareInTime line 508
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.machine line 530
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSoundness.leftTable line 554
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSoundness.rightOracle line 558
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSoundness.rightOracle_answer line 566
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSoundness.leftTable_answer line 572

theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSoundness.sourceList_sound line 578

Source documentation

Exact finite occurrence-list soundness, including arbitrary assignments to unused padded proof bits and to the dummy bit.

theorem sourceList_sound (F : Formula) (hne : F.clauses ≠ []) (u D : ℕ)
    (hD : 0 < D) (hDtwo : 2 ≤ D) (δ : ℝ) (hδ : 0 ≤ δ)
    (hvalue : ((baseGame F hne).repetition u).value ≤
      4 * (D : ℝ)⁻¹ * δ ^ 2)
    (bits : Fin (nBits F u) → Bool) :
    ((sourceList F u D).countP (fun e => UniqueGamesTheorem.Reduction.CloneGap.satisfied e bits) : ℝ) /
      (sourceList F u D).length ≤ (1 + δ) / 2 := by
…

Mentions: OAI.UniqueGamesTheorem.Reduction.CloneGap.satisfied

theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSoundness.sourceList_sound_rat line 597

Source documentation

The direct uniform reduction consumes rational occurrence fractions.

theorem sourceList_sound_rat (F : Formula) (hne : F.clauses ≠ []) (u D : ℕ)
    (hD : 0 < D) (hDtwo : 2 ≤ D) (δ : ℚ) (hδ : 0 ≤ δ)
    (hvalue : ((baseGame F hne).repetition u).value ≤
      4 * (D : ℝ)⁻¹ * (δ : ℝ) ^ 2)
    (bits : Fin (nBits F u) → Bool) :
    ((sourceList F u D).countP (fun e => UniqueGamesTheorem.Reduction.CloneGap.satisfied e bits) : ℚ) /
      (sourceList F u D).length ≤ (1 + δ) / 2 := by
…

Mentions: OAI.UniqueGamesTheorem.Reduction.CloneGap.satisfied

abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestEmit.Label line 622
abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestEmit.State line 623
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestEmit.localEquation line 625
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestEmit.bodyLabel line 628
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestEmit.program line 633

theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestEmit.testTrace line 643

Source documentation

The table selector is one real transition; every subsequent copy/push transition belongs to the same fixed program.

theorem testTrace (u D : ℕ) (sources : Fin 3 → K) (destination scratch : K)
    (sourceDestination : ∀ side, sources side ≠ destination)
    (sourceScratch : ∀ side, sources side ≠ scratch)
    (destinationScratch : destination ≠ scratch) (exit : Option (Label u D))
    (state : LocalInput u D) (base : K → List Bool) (values : Fin 3 → ℕ)
    (sourceWords : ∀ side, base (sources side) = encodeWord (values side))
    (scratchEmpty : base scratch = []) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program u D sources destination scratch exit)))^[
      SourceEquationEmit.steps values (localEquation u D state) + 1]
        (some ⟨some (.inl ()), (state, register), base⟩) =
      some ⟨exit, (state, none),
        prefixTapes destination base (words values (localEquation u D state))⟩ := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestEmit.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestEmit.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.steps, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestEmit.localEquation

def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestEmit.testInTime line 664
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestEmit.sourceTestInTime line 681
inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.Label line 719
abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.State line 724
structure OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.Layout line 726
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.equationBits line 738
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.steps line 741
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.bodyLabel line 747
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.statement line 751
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.program line 760
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.resultTapes line 764
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.resultTapes_other line 767
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.resultTapes_source line 771
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.resultTapes_temporary line 775
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.resultTapes_scratch line 779

theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.emitTrace line 784

Source documentation

Placement-aware finite selection plus actual equation emission.

theorem emitTrace (u D : Nat) (layout : Layout K) (labels : Label u D → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State u D))
    (atLabels : ∀ label, p (labels label) = statement u D layout labels exit label)
    (state : LocalInput u D) (base : K → List Bool) (values : Fin 3 → Nat)
    (sourceWords : ∀ side, base (layout.sources side) = encodeWord (values side))
    (scratchEmpty : base layout.scratch = []) (register : Option Bool) :
    (MachineComposition.advance (TM2.step p))^[
      SourceEquationEmit.steps values (localEquation u D state) + 1]
      (some ⟨some (labels (.test (.inl ()))), (state, register), base⟩) =
      some ⟨some (labels .append), (state, none),
        prefixTapes layout.temporary base (words values (localEquation u D state))⟩ := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.Layout, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.State, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.statement, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceEquationEmit.steps

theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.appendTrace line 813

Source documentation

Exact one-record append trace in an arbitrary caller program.

theorem appendTrace (u D : Nat) (layout : Layout K) (labels : Label u D → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State u D))
    (atLabels : ∀ label, p (labels label) = statement u D layout labels exit label)
    (state : LocalInput u D) (base : K → List Bool) (values : Fin 3 → Nat)
    (sourceWords : ∀ side, base (layout.sources side) = encodeWord (values side))
    (scratchEmpty : base layout.scratch = []) (temporaryEmpty : base layout.temporary = [])
    (register : Option Bool) :
    (MachineComposition.advance (TM2.step p))^[steps u D values state]
      (some ⟨some (labels (.test (.inl ()))), (state, register), base⟩) =
      some ⟨exit, (state, none), resultTapes layout base (equationBits u D values state)⟩ := by
…

def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.appendInTime line 856
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.programInTime line 872
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.sourceAppendInTime line 884
abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.Tape line 920
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.standardLayout line 922
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.machine line 934
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.machineInTime line 945