MachineSubdivisionCorrespondence.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

The actual streamed bytes coincide with the numbered semantic subdivision. The controller copies the last table unchanged, so its input contract explicitly requires involutive tables; binary translations satisfy this condition.

def OAI.MaxCutGames.Explicit.MachineSubdivisionCorrespondence.Involutive line 17
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionCorrespondence.inverseTable_eq line 21
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionCorrespondence.translations_involutive line 29
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionCorrespondence.rowBits_eq_semantic line 50
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionCorrespondence.outputRows_eq_ofFn line 69
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionCorrespondence.outputRows_eq_semantic line 78
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionCorrespondence.output_eq_gameBits line 89
Source documentation
Exact complete serialized output, including the changed headers and every forward permutation-table entry, in occurrence order.
```
theorem output_eq_gameBits {q : Nat} (H : Instance q) (involutive : Involutive H) :
    MachineSubdivisionEmission.headerBits H.vertices q H.constraints.length ++
      outputRows H.constraints.length 0 H.constraints =
      gameBits (SubdivisionTarget.subdivide H) := by
…
```
Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionCorrespondence.Involutive, OAI.MaxCutGames.Explicit.MachineSubdivisionEmission.headerBits, OAI.MaxCutGames.Explicit.SubdivisionTarget.subdivide
def OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.prefixPolynomial line 111
def OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.timePolynomial line 116
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.input_eq line 119
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.input_size line 123
def OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.finalTapes line 130
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.final_outputEmpty line 135
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.final_accumulator line 137
def OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.prefixInTime line 145
Source documentation
The prefix contains every actual header read, fresh-name initialization, header emission, complete four-row body, and occurrence-counter test.
```
def prefixInTime {q : Nat} (H : Instance q) :
    StateTransition.EvalsToInTime (machine q).step
      (initList (machine q) (gameBits H))
      (some ⟨some .finishStart, initialState, finalTapes H⟩)
      ((prefixPolynomial q).eval (gameBits H).length) := by
…
```
Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.finalTapes, OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.prefixPolynomial
def OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.fullRunInTime line 178
Source documentation
Literal initialization to literal clean halting configuration, with exact semantic subdivision output. No execution or runtime premise is assumed.
```
def fullRunInTime {q : Nat} (H : Instance q) (involutive : Involutive H) :
    TM2OutputsInTime (machine q) (gameBits H)
      (some (gameBits (SubdivisionTarget.subdivide H)))
      ((timePolynomial q).eval (gameBits H).length) := by
…
```
Mentions: OAI.MaxCutGames.Explicit.SubdivisionTarget.subdivide, OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.timePolynomial
def OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.computableInPolyTime line 188
Source documentation
The input subtype records the mathematical involution property, while the same finite transition program is used for every instance of the fixed alphabet.
```
def computableInPolyTime (q : Nat) :
    TM2ComputableInPolyTime
      (fun H : {H : Instance q // Involutive H} => gameBits H.val)
      gameBits (fun H => SubdivisionTarget.subdivide H.val) where
…
```
Mentions: OAI.MaxCutGames.Explicit.SubdivisionTarget.subdivide
def OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.familyComputableInPolyTime line 206
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionRuntime.workAlphabetFinite line 224
def OAI.MaxCutGames.Explicit.MachineSubdivisionCompose.certifiedOutput line 243
def OAI.MaxCutGames.Explicit.MachineSubdivisionCompose.certify line 248
Source documentation
Attach the already-proved property without executing anything or changing the input or output codec.
```
def certify (upstream : TM2ComputableInPolyTime encode gameBits f)
    (involutive : ∀ a, Involutive (f a)) :
    TM2ComputableInPolyTime encode (fun H : {H : Instance q // Involutive H} => gameBits H.val)
      (certifiedOutput involutive) where
…
```
Mentions: OAI.MaxCutGames.Explicit.MachineSubdivisionCompose.certifiedOutput
def OAI.MaxCutGames.Explicit.MachineSubdivisionCompose.computableInPolyTime line 258
theorem OAI.MaxCutGames.Explicit.MachineSubdivisionCompose.finiteAlphabet line 266

def OAI.MaxCutGames.Explicit.MachineSubdivisionCompose.translationComputableInPolyTime line 275

Source documentation

Binary-translation producers discharge the only table-law condition.

def translationComputableInPolyTime {s : Nat}
    (coordinates : Fin q ≃ Integration.BinaryLinear.Vector s)
    (upstream : TM2ComputableInPolyTime encode gameBits f)
    (translations : ∀ a, Integration.TranslationTarget.IsTranslationInstance coordinates (f a)) :
    TM2ComputableInPolyTime encode gameBits (fun a => SubdivisionTarget.subdivide (f a)) :=
…

Mentions: OAI.MaxCutGames.Integration.BinaryLinear.Vector, OAI.MaxCutGames.Integration.TranslationTarget.IsTranslationInstance, OAI.MaxCutGames.Explicit.SubdivisionTarget.subdivide