SourceTupleBody.lean`

59 declarations, 0 contain sorry, 0 declared as axioms

One actual clause-tuple body. Its fixed finite control loads the context, computes the shared right address base, traverses every selected-slot tuple and query tape in their declared encoding order, and physically clears its work.

abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.SlotCount line 19
abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.QueryCount line 20
abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Query line 21
inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Label line 23
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.selected line 42
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.main line 45
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.framed line 47
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.framedConfiguration line 52
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.framed_stepAux line 61
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.framed_step line 68
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.framedExecution line 83
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.finish line 98
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.drainProgram line 104
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.drainStatement line 108
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.selectState line 115
Source documentation
Only the chosen-slot/query registers change; the computed context profile and original signature remain available across all local traversals.
```
def selectState (initialQuery : Query u D) (index : Fin (SlotCount u))
    (state : State u D) : State u D :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Query, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.SlotCount
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.program line 120
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.reset_step line 158
Source documentation
All finite internal state is reset before the caller continuation.
```
theorem reset_step (initialQuery : Query u D) (exit : Option (Label u D Extra))
    (state : State u D) (tapes : Arena u Extra → List Bool) :
    TM2.step (program initialQuery exit) ⟨some .reset, state, tapes⟩ =
      some ⟨exit, canonicalState initialQuery, tapes⟩ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Query, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.program
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.resetInTime line 164
structure OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Ready line 174
Source documentation
The complete representation needed at one odometer leaf. Remaining-digit stacks, output history, and retained unused headers are arbitrary.
```
structure Ready (F : Target.Formula) (c : ClauseContext F u)
    (base : Arena u Extra → List Bool) : Prop where
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.contextSignature line 200
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.workingState line 203
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.workingState_loader line 208
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.arithmeticMetadata line 212
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.queryMetadata line 218
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.arithmeticState_working line 223
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.queryState_working line 228
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.select_workingState line 233
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.rightValue line 238
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.variableRank line 241
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.leftValue line 244
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.slotBudget line 247

def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.preparePhase line 256

Source documentation

Concrete context-loader/signature phase in the tuple-body program.

noncomputable def preparePhase (F : Target.Formula) (c : ClauseContext F u)
    (initialQuery : Query u D) (exit : Option (Label u D Extra))
    (base : Arena u Extra → List Bool)
    (hformula : base .formula = formulaBits F)
    (hcurrent : ∀ j, base (.current j) = encodeWord (c j).val)
    (hindex : base .index = []) (hwork : base .work = [])
    (hscratch : base .scratch = []) (hcopy : base .copyScratch = [])
    (hfields : ∀ p : Position u, base (SourceSignaturePrepare.variableField p) = []) :
    StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
      ⟨some main, canonicalState initialQuery, base⟩
      (some ⟨some .seedZero,
        SourceContextPrepare.finalState F c (fun _ => .first)
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Query, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.variableField, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.main, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextPrepare.finalState

def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.seedZeroPhase line 279

def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.drainPhase line 294

Source documentation

The caller only supplies a local code equality; the physical drain and its entire runtime are obtained from the checked drain machine.

def drainPhase (initialQuery : Query u D) (exit : Option (Label u D Extra))
    (source : Arena u Extra) (entry : Label u D Extra) (next : Option (Label u D Extra))
    (atEntry : program initialQuery exit entry = drainStatement source entry next)
    (base : Arena u Extra → List Bool)
    (metadata : SourceSignaturePrepare.State u (QueryState u D × ArithmeticState))
    (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
      ⟨some entry, (((), register), metadata), base⟩
      (some ⟨next, (((), none), metadata), Function.update base source []⟩)
      ((base source).length + 1) := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Query, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.drainStatement, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceSignaturePrepare.State

def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.clauseRankPhase line 308
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.variableRankPhase line 325
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.rightBasePhase line 346
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.leftBasePhase line 368
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.queryPhase line 393
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.selectPhase line 419
Source documentation
The fixed selected-slot tuple is loaded in one actual transition.
```
def selectPhase (initialQuery : Query u D) (exit : Option (Label u D Extra))
    (index : Fin (SlotCount u)) (state : State u D) (base : Arena u Extra → List Bool) :
    StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
      ⟨some (.select index.castSucc), state, base⟩
      (some ⟨some (.variableRank index .start), selectState initialQuery index state, base⟩) 1 where
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Query, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.SlotCount, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.variableRank, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.selectState
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.loaded_extra line 431
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Ready.loadedClean line 437
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.loopSnapshot line 445
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.rankSnapshot line 448
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.baseSnapshot line 452
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.slotInTime line 458
Source documentation
One selected-slot tuple: actual rank, base construction, complete query stream, and physical cleanup, in the one fixed caller program.
```
theorem slotInTime (F : Target.Formula) (c : ClauseContext F u)
    (initialQuery beforeQuery : Query u D) (beforeSignature : Signature u)
    (exit : Option (Label u D Extra)) (base : Arena u Extra → List Bool) (h : Ready F c base)
    (index : Fin (SlotCount u)) (bits : List Bool) :
    ∃ afterQuery : Query u D,
      Nonempty (StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
        ⟨some (.select index.castSucc), workingState F c beforeSignature beforeQuery,
          tapes (SourceContextLoad.stageTapes F c base u) (loopSnapshot F c bits)⟩
        (some ⟨some (.select ⟨index.val + 1, by omega⟩),
          workingState F c (ofContext F c (selected index)) afterQuery,
          tapes (SourceContextLoad.stageTapes F c base u)
            (loopSnapshot F c (bits ++ SourceQueryOrder.slotBits F u D c (selected index)))⟩)
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Query, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Ready, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.SlotCount, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.workingState, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.stageTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.loopSnapshot, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.selected, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryOrder.slotBits
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.slotAt line 555
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.prefixBits line 558
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.prefixBudget line 562
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.prefixInTime line 567
Source documentation
The explicit finite loop runs in ascending slot-encoding order.
```
theorem prefixInTime (F : Target.Formula) (c : ClauseContext F u)
    (initialQuery beforeQuery : Query u D) (beforeSignature : Signature u)
    (exit : Option (Label u D Extra)) (base : Arena u Extra → List Bool) (h : Ready F c base)
    (r : Nat) (hr : r ≤ SlotCount u) :
    ∃ afterSignature : Signature u, ∃ afterQuery : Query u D,
      Nonempty (StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
        ⟨some (.select ⟨0, by omega⟩), workingState F c beforeSignature beforeQuery,
          tapes (SourceContextLoad.stageTapes F c base u) (loopSnapshot F c [])⟩
        (some ⟨some (.select ⟨r, by omega⟩), workingState F c afterSignature afterQuery,
          tapes (SourceContextLoad.stageTapes F c base u)
            (loopSnapshot F c (prefixBits (D := D) F c r))⟩)
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Query, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Ready, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.SlotCount, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.workingState, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.stageTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.loopSnapshot, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.prefixBits
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.prefixBits_eq_ofFn line 600
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.prefixBits_eq_tupleBits line 611
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.setupBudget line 622
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.finishBudget line 632
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.bodyBudget line 635
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.setupInTime line 639
Source documentation
Actual context preparation and the shared right base are computed once.
```
noncomputable def setupInTime (F : Target.Formula) (c : ClauseContext F u)
    (initialQuery : Query u D) (exit : Option (Label u D Extra))
    (base : Arena u Extra → List Bool) (h : Ready F c base) :
    StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
      ⟨some main, canonicalState initialQuery, base⟩
      (some ⟨some (.select ⟨0, by omega⟩),
        workingState F c (canonicalSignature u) initialQuery,
        tapes (SourceContextLoad.stageTapes F c base u) (loopSnapshot F c [])⟩)
      (setupBudget F c) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Query, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Ready, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.main, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.workingState, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.stageTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.loopSnapshot, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.setupBudget
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.finishInTime line 709
Source documentation
Physical cleanup and canonical finite-state reset complete the body.
```
def finishInTime (F : Target.Formula) (c : ClauseContext F u)
    (initialQuery query : Query u D) (signature : Signature u)
    (exit : Option (Label u D Extra)) (base : Arena u Extra → List Bool) (h : Ready F c base)
    (bits : List Bool) :
    StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
      ⟨some (.select ⟨SlotCount u, by omega⟩), workingState F c signature query,
        tapes (SourceContextLoad.stageTapes F c base u) (loopSnapshot F c bits)⟩
      (some ⟨exit, canonicalState initialQuery, SourceTestAppend.resultTapes queryLayout base bits⟩)
      (finishBudget F c) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Query, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Ready, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.SlotCount, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.workingState, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceContextLoad.stageTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.loopSnapshot, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.resultTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.finishBudget
theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.bodyInTime line 770
Source documentation
One complete actual clause-tuple execution. The only changed tape is the reversed-output accumulator; every internal finite register is reset.
```
theorem bodyInTime (F : Target.Formula) (c : ClauseContext F u)
    (initialQuery : Query u D) (exit : Option (Label u D Extra))
    (base : Arena u Extra → List Bool) (h : Ready F c base) :
    Nonempty (StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
      ⟨some main, canonicalState initialQuery, base⟩
      (some ⟨exit, canonicalState initialQuery,
        SourceTestAppend.resultTapes queryLayout base (SourceQueryOrder.tupleBits F u D c)⟩)
      (bodyBudget (D := D) F c)) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Target.Formula, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Query, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.Ready, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.program, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.main, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTestAppend.resultTapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceQueryOrder.tupleBits, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.bodyBudget
def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceTupleBody.machine line 791