OAI/Computability/MaxCut/Games/AddressGame.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

Executable direct addresses for the actual canonical game. Every original edge occurrence and its translation table is retained, in the same order. Addresses not representing realized bodies are isolated vertices. No vertex list, duplicate removal, or inverse enumeration is evaluated by the output.

  1. abbrev OAI.MaxCutGames.Reduction.AddressGame.bodyCapacity line 19
  2. def OAI.MaxCutGames.Reduction.AddressGame.vertexCount line 22
  3. def OAI.MaxCutGames.Reduction.AddressGame.vertexAddress line 25

    Source documentation

    Both bipartite sides remain distinct address blocks.

    def vertexAddress (S : Source) (k s d : Nat) (v : ActualGame.TwoSidedVertex S k s d) :
    Fin (vertexCount S k s d) :=
…

    Mentions: OAI.MaxCutGames.Reduction.ActualGame.TwoSidedVertex, OAI.MaxCutGames.Reduction.AddressGame.vertexCount

  4. theorem OAI.MaxCutGames.Reduction.AddressGame.vertexAddress_injective line 29
  5. def OAI.MaxCutGames.Reduction.AddressGame.queryAddress line 41

    Source documentation

    This is the endpoint routine used at runtime: canonicalize, serialize, apply Horner radix arithmetic, and add the side block.

    def queryAddress (S : Source) (k s d : Nat) (side : Bool) (q : ActualGame.Query S k s d) :
    Fin (vertexCount S k s d) :=
…

    Mentions: OAI.MaxCutGames.Reduction.ActualGame.Query, OAI.MaxCutGames.Reduction.AddressGame.vertexCount

  6. theorem OAI.MaxCutGames.Reduction.AddressGame.vertexAddress_query line 46
  7. def OAI.MaxCutGames.Reduction.AddressGame.explicitToAddress line 52

    Source documentation

    Proof adapter only: the output constructor does not call this inverse.

    def explicitToAddress (S : Source) (k s d : Nat) :
    Fin (ActualGame.explicitVertexCount S k s d) → Fin (vertexCount S k s d) :=
…

    Mentions: OAI.MaxCutGames.Reduction.ActualGame.explicitVertexCount, OAI.MaxCutGames.Reduction.AddressGame.vertexCount

  8. theorem OAI.MaxCutGames.Reduction.AddressGame.explicitToAddress_injective line 56
  9. theorem OAI.MaxCutGames.Reduction.AddressGame.explicitToAddress_apply line 60
  10. def OAI.MaxCutGames.Reduction.AddressGame.semanticToAddress line 67

    Source documentation

    The corresponding injection from the original semantic vertex space.

    noncomputable def semanticToAddress (S : Source) (k s d : Nat) :
    Fin (ActualGame.vertexCount S k s d) → Fin (vertexCount S k s d) :=
…

    Mentions: OAI.MaxCutGames.Reduction.ActualGame.vertexCount, OAI.MaxCutGames.Reduction.AddressGame.vertexCount

  11. theorem OAI.MaxCutGames.Reduction.AddressGame.semanticToAddress_injective line 71
  12. theorem OAI.MaxCutGames.Reduction.AddressGame.semanticToAddress_apply line 75
  13. def OAI.MaxCutGames.Reduction.AddressGame.addressEdge line 81
  14. theorem OAI.MaxCutGames.Reduction.AddressGame.addressEdge_eq_embed line 89
  15. theorem OAI.MaxCutGames.Reduction.AddressGame.addressEdge_eq_semantic_embed line 96
  16. theorem OAI.MaxCutGames.Reduction.AddressGame.addressEdge_permutation line 103
  17. def OAI.MaxCutGames.Reduction.AddressGame.outputInstance line 109

    Source documentation

    Only canonical words, bounded radix arithmetic, and the explicit outcome list occur in the runtime path. The correcting function is not inspected.

    def outputInstance (S : Source) (k : Nat) {s d : Nat} (g : SplitGadget s d)
    (en : NoiseEnumeration g) : Instance (2^s) where
…
  18. theorem OAI.MaxCutGames.Reduction.AddressGame.outputInstance_eq_embed line 121

    Source documentation

    An exact instance equality, retaining the explicit edge-list order.

    theorem outputInstance_eq_embed (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (en : NoiseEnumeration g) :
    outputInstance S k g en =
      embedInstance (ActualGame.outputInstanceWithEnumeration S k g en)
        (explicitToAddress S k s d) (explicitToAddress_injective S k s d) := by
…

    Mentions: OAI.MaxCutGames.Reduction.AddressGame.outputInstance, OAI.MaxCutGames.Reduction.ActualGame.outputInstanceWithEnumeration, OAI.MaxCutGames.Reduction.AddressGame.explicitToAddress, OAI.MaxCutGames.Reduction.AddressGame.explicitToAddress_injective

  19. theorem OAI.MaxCutGames.Reduction.AddressGame.outputInstance_length line 130
  20. theorem OAI.MaxCutGames.Reduction.AddressGame.outputInstance_count line 137
  21. theorem OAI.MaxCutGames.Reduction.AddressGame.completeAt_outputInstance_iff_explicit line 148
  22. theorem OAI.MaxCutGames.Reduction.AddressGame.soundAt_outputInstance_iff_explicit line 155
  23. theorem OAI.MaxCutGames.Reduction.AddressGame.completeAt_outputInstance_iff line 162
  24. theorem OAI.MaxCutGames.Reduction.AddressGame.soundAt_outputInstance_iff line 168
  25. theorem OAI.MaxCutGames.Reduction.AddressGame.outputInstance_translations line 174
  26. def OAI.MaxCutGames.Reduction.AddressGame.tableOutput line 185

    Source documentation

    The concrete vector-table interface contains no correcting-map witness.

    def tableOutput (S : Source) (k : Nat) {s d : Nat} (T : Integration.NoiseTables.Table s d) :
    Instance (2^s) :=
…

    Mentions: OAI.MaxCutGames.Integration.NoiseTables.Table

  27. theorem OAI.MaxCutGames.Reduction.AddressGame.completeAt_tableOutput_iff line 190
  28. theorem OAI.MaxCutGames.Reduction.AddressGame.soundAt_tableOutput_iff line 195
  29. theorem OAI.MaxCutGames.Reduction.AddressGame.tableOutput_translations line 200
  30. theorem OAI.MaxCutGames.Reduction.AddressGame.vertexCount_eq_polynomial line 206

    Source documentation

    Exact polynomial bound for the complete two-sided address space.

    theorem vertexCount_eq_polynomial (S : Source) (k s d : Nat) :
    vertexCount S k s d = 2 * (CanonicalAddress.capacityPolynomial k s d).eval
      (S.«variables» + S.occurrences) := by
…

    Mentions: OAI.MaxCutGames.Reduction.AddressGame.vertexCount, OAI.MaxCutGames.Reduction.CanonicalAddress.capacityPolynomial

  31. abbrev OAI.MaxCutGames.Reduction.FixedOutcomes.Parameter line 221
  32. def OAI.MaxCutGames.Reduction.FixedOutcomes.occurrenceTuples line 224
  33. def OAI.MaxCutGames.Reduction.FixedOutcomes.fixedParams line 229

    Source documentation

    Ambient linear map, noise occurrence index, scalar linear functional, in exactly the original nested enumeration order.

    def fixedParams (k s d : Nat) (indices : List N) : List (Parameter k s d N) :=
…

    Mentions: OAI.MaxCutGames.Reduction.FixedOutcomes.Parameter

  34. def OAI.MaxCutGames.Reduction.FixedOutcomes.assemble line 233
  35. def OAI.MaxCutGames.Reduction.FixedOutcomes.outcomeEquiv line 238

    Source documentation

    The reassociation changes only parentheses, not enumeration order.

    def outcomeEquiv (m k s d : Nat) (N : Type*) :
    (Query m k s d × (N × (E k →ₗ[F2] F2))) ≃
      ((Fin k → Fin m) × Parameter k s d N) :=
…

    Mentions: OAI.MaxCutGames.Reduction.FixedOutcomes.Parameter

  36. theorem OAI.MaxCutGames.Reduction.FixedOutcomes.pairs_associate_inline_FixedOutcomes line 243
  37. theorem OAI.MaxCutGames.Reduction.FixedOutcomes.indexedOutcomes_factor line 249
  38. theorem OAI.MaxCutGames.Reduction.FixedOutcomes.indexedOutcomes_reassociate line 256
  39. theorem OAI.MaxCutGames.Reduction.FixedOutcomes.occurrenceTuples_length line 263
  40. theorem OAI.MaxCutGames.Reduction.FixedOutcomes.fixedParams_length line 266
  41. theorem OAI.MaxCutGames.Reduction.FixedOutcomes.fixedParams_nonempty line 275
  42. abbrev OAI.MaxCutGames.Reduction.FixedOutcomes.CoefficientParameter line 282

    Source documentation

    A coefficient-only representation of each fixed linear-map parameter.

    abbrev CoefficientParameter (k s d : Nat) (N : Type*) :=
…
  43. def OAI.MaxCutGames.Reduction.FixedOutcomes.coefficientValues line 285
  44. def OAI.MaxCutGames.Reduction.FixedOutcomes.fixedCoefficientParams line 288
  45. def OAI.MaxCutGames.Reduction.FixedOutcomes.fromCoefficientParameter line 293
  46. theorem OAI.MaxCutGames.Reduction.FixedOutcomes.fixedCoefficientParams_map line 299

    Source documentation

    The concrete coefficient enumeration produces precisely the fixed parameter list. No choice of maps or representatives is made by this constructor.

    theorem fixedCoefficientParams_map (k s d : Nat) (indices : List N) :
    (fixedCoefficientParams k s d indices).map fromCoefficientParameter =
      fixedParams k s d indices := by
…

    Mentions: OAI.MaxCutGames.Reduction.FixedOutcomes.fixedCoefficientParams, OAI.MaxCutGames.Reduction.FixedOutcomes.fromCoefficientParameter, OAI.MaxCutGames.Reduction.FixedOutcomes.fixedParams

  47. theorem OAI.MaxCutGames.Reduction.FixedOutcomes.fixedCoefficientParams_length line 306
  48. def OAI.MaxCutGames.Reduction.FixedOutcomes.tableParams line 311
  49. theorem OAI.MaxCutGames.Reduction.FixedOutcomes.tableParams_length line 315
  50. theorem OAI.MaxCutGames.Reduction.FixedOutcomes.outputInstance_constraints line 319
  51. theorem OAI.MaxCutGames.Reduction.FixedOutcomes.tableOutput_constraints line 330
  52. def OAI.MaxCutGames.Reduction.AddressByteSemantics.queryWords line 345
  53. def OAI.MaxCutGames.Reduction.AddressByteSemantics.queryRank line 351
  54. def OAI.MaxCutGames.Reduction.AddressByteSemantics.permutationWords line 355
  55. def OAI.MaxCutGames.Reduction.AddressByteSemantics.edgeWords line 363
  56. def OAI.MaxCutGames.Reduction.AddressByteSemantics.edgeBits line 368
  57. theorem OAI.MaxCutGames.Reduction.AddressByteSemantics.queryWords_length line 372
  58. theorem OAI.MaxCutGames.Reduction.AddressByteSemantics.permutationWords_length line 378
  59. theorem OAI.MaxCutGames.Reduction.AddressByteSemantics.queryWords_actual line 382
  60. theorem OAI.MaxCutGames.Reduction.AddressByteSemantics.queryAddress_false line 389
  61. theorem OAI.MaxCutGames.Reduction.AddressByteSemantics.queryAddress_true line 398
  62. theorem OAI.MaxCutGames.Reduction.AddressByteSemantics.addressEdge_words line 409

    Source documentation

    Exact full serialized edge, including every forward permutation image.

    theorem addressEdge_words (S : Source) (k : Nat) {s d : Nat}
    (g : SplitGadget s d) (omega : ActualGame.Outcome S k g) :
    constraintWords (AddressGame.addressEdge S k g omega) =
      edgeWords (CanonicalAddress.base S.«variables» S.occurrences s d)
        (AddressGame.bodyCapacity S k s d)
        (CanonicalBodyTemplate.sourceFields omega.1.1 (ActualGame.names S))
        omega.1.2 (ActualGame.rightQuery S k g omega).2
        (fun j => ActualGame.rhs S (omega.1.1 j)) := by
…

    Mentions: OAI.MaxCutGames.Reduction.ActualGame.Outcome, OAI.MaxCutGames.Reduction.AddressGame.addressEdge, OAI.MaxCutGames.Reduction.AddressByteSemantics.edgeWords, OAI.MaxCutGames.Reduction.CanonicalAddress.base, OAI.MaxCutGames.Reduction.AddressGame.bodyCapacity, OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.sourceFields, OAI.MaxCutGames.Reduction.ActualGame.names, OAI.MaxCutGames.Reduction.ActualGame.rightQuery, OAI.MaxCutGames.Reduction.ActualGame.rhs

  63. theorem OAI.MaxCutGames.Reduction.AddressByteSemantics.addressEdge_bits line 423
  64. theorem OAI.MaxCutGames.Reduction.AddressByteSemantics.edgeBits_split line 435

    Source documentation

    The actual edge emitter's three payloads concatenate to the codec exactly.

    theorem edgeBits_split {k s d : Nat} (base capacity : Nat)
    (fields : Fin k → Fin 4 → Nat) (X Y : ActualGame.Map k s d) (b : Fin k → F2) :
    edgeBits base capacity fields X Y b =
      encodeWords [queryRank base fields X b, capacity + queryRank base fields Y b] ++
        encodeWords (permutationWords X Y b) := by
…

    Mentions: OAI.MaxCutGames.Reduction.ActualGame.Map, OAI.MaxCutGames.Reduction.AddressByteSemantics.edgeBits, OAI.MaxCutGames.Reduction.AddressByteSemantics.queryRank, OAI.MaxCutGames.Reduction.AddressByteSemantics.permutationWords

  65. abbrev OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.Spec line 451
  66. abbrev OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.Values line 452
  67. abbrev OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.Parameter line 453
  68. def OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.bitVector line 456
  69. def OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.rightMap line 458
  70. def OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.row line 461
  71. def OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.rows line 469
  72. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.row_left_length line 473
  73. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.row_right_length line 477
  74. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.rows_length line 481
  75. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.selected_rows line 485
  76. def OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.interpreted line 493

    Source documentation

    A total proof-side interpretation. The fallback handles arbitrary malformed static specs; actual canonical rows always take the checked decoding branch.

    def interpreted (width : Nat) (bits : List Bool) : {words : List Nat // words.length = width} :=
…
  77. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.interpreted_encoded line 498
  78. def OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.values line 502
  79. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.row_left_output line 512
  80. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.row_right_output line 518
  81. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.values_row_left line 524
  82. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.values_row_right line 532
  83. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.correct_rows line 540
  84. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.payload_row line 556
  85. def OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.rhsBits line 565
  86. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.bitVector_rhsBits line 568
  87. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.rightMap_actual line 571
  88. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.payload_row_actual line 577

    Source documentation

    Each static row emits exactly the concrete game's constraint encoding.

    theorem payload_row_actual (S : Source) (k : Nat) {s d : Nat}
    (T : NoiseTables.Table s d) (U : ActualGame.Question S k) (p : Parameter k T) :
    MachineOutcomeRows.payload
        (CanonicalAddress.base S.«variables» S.occurrences s d) (AddressGame.bodyCapacity S k s d)
        (values (CanonicalBodyTemplate.sourceFields U (ActualGame.names S)))
        (row T p (rhsBits S U)) =
      encodeWords (constraintWords (AddressGame.addressEdge S k (TableReduction.tableSkeleton T)
        (FixedOutcomes.assemble U p))) := by
…

    Mentions: OAI.MaxCutGames.Reduction.ActualGame.Question, OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.Parameter, OAI.MaxCutGames.Reduction.MachineOutcomeRows.payload, OAI.MaxCutGames.Reduction.CanonicalAddress.base, OAI.MaxCutGames.Reduction.AddressGame.bodyCapacity, OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.values, OAI.MaxCutGames.Reduction.CanonicalBodyTemplate.sourceFields, OAI.MaxCutGames.Reduction.ActualGame.names, OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.row, OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.rhsBits, OAI.MaxCutGames.Reduction.AddressGame.addressEdge, OAI.MaxCutGames.Reduction.FixedOutcomes.assemble

  89. def OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.tupleBits line 589
  90. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.tuplePayload_actual line 595
  91. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.encodeWords_flatMap_inline_AddressOutcomeSpecs line 606
  92. theorem OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.gameBits_factor line 613

    Source documentation

    Complete output-byte factorization used by the actual outer loop.

    theorem gameBits_factor (S : Source) (k : Nat) {s d : Nat} (T : NoiseTables.Table s d) :
    gameBits (AddressGame.tableOutput S k T) =
      encodeWords [(AddressGame.tableOutput S k T).vertices, 2^s,
        (AddressGame.tableOutput S k T).constraints.length] ++
      (FixedOutcomes.occurrenceTuples S.occurrences k).flatMap (tupleBits S k T) := by
…

    Mentions: OAI.MaxCutGames.Reduction.AddressGame.tableOutput, OAI.MaxCutGames.Reduction.FixedOutcomes.occurrenceTuples, OAI.MaxCutGames.Reduction.AddressOutcomeSpecs.tupleBits

  93. abbrev OAI.MaxCutGames.Integration.AddressTupleBody.Arena line 636
  94. abbrev OAI.MaxCutGames.Integration.AddressTupleBody.Rows line 637
  95. abbrev OAI.MaxCutGames.Integration.AddressTupleBody.Slots line 638
  96. abbrev OAI.MaxCutGames.Integration.AddressTupleBody.BodyState line 639
  97. abbrev OAI.MaxCutGames.Integration.AddressTupleBody.CleanupLabel line 640
  98. abbrev OAI.MaxCutGames.Integration.AddressTupleBody.RowLabel line 642
  99. abbrev OAI.MaxCutGames.Integration.AddressTupleBody.Label line 644
  100. instance OAI.MaxCutGames.Integration.AddressTupleBody.labelFintype line 648
  101. def OAI.MaxCutGames.Integration.AddressTupleBody.sourceLabels line 654
  102. def OAI.MaxCutGames.Integration.AddressTupleBody.rhsLabel line 656
  103. def OAI.MaxCutGames.Integration.AddressTupleBody.rowLabels line 657
  104. def OAI.MaxCutGames.Integration.AddressTupleBody.cleanupLabels line 659
  105. def OAI.MaxCutGames.Integration.AddressTupleBody.resetLabel line 661
  106. def OAI.MaxCutGames.Integration.AddressTupleBody.main line 664
  107. def OAI.MaxCutGames.Integration.AddressTupleBody.reset line 666
  108. def OAI.MaxCutGames.Integration.AddressTupleBody.instruction line 669
  109. def OAI.MaxCutGames.Integration.AddressTupleBody.program line 683
  110. def OAI.MaxCutGames.Integration.AddressTupleBody.rhs line 687
  111. def OAI.MaxCutGames.Integration.AddressTupleBody.loaded line 690
  112. def OAI.MaxCutGames.Integration.AddressTupleBody.tupleBits line 694
  113. def OAI.MaxCutGames.Integration.AddressTupleBody.emitted line 699
  114. def OAI.MaxCutGames.Integration.AddressTupleBody.finalTapes line 706
  115. structure OAI.MaxCutGames.Integration.AddressTupleBody.Ready line 712
  116. def OAI.MaxCutGames.Integration.AddressTupleBody.budget line 722
  117. def OAI.MaxCutGames.Integration.AddressTupleBody.run line 731
  118. def OAI.MaxCutGames.Integration.AddressTupleBody.source line 785
  119. theorem OAI.MaxCutGames.Integration.AddressTupleBody.rhs_eq_actual line 788
  120. theorem OAI.MaxCutGames.Integration.AddressTupleBody.canonicalValues_eq_actual line 791
  121. theorem OAI.MaxCutGames.Integration.AddressTupleBody.tupleBits_actual line 800
  122. theorem OAI.MaxCutGames.Integration.AddressTupleBody.actualInvariant line 813

    Source documentation

    All generic template-correctness obligations are discharged from the actual loader's canonical field values and the checked fixed-row specs.

    theorem actualInvariant (F : SourceEncoding.Input) (tuple : Fin k → Fin F.equations.length)
    (T : NoiseTables.Table s d) (base : Arena k s d noiseCount → List Bool)
    (ready : Ready F tuple base)
    (clean : MachineAddressEdge.Clean (Slots k s d noiseCount) base) (B C : Nat)
    (hB : base (headerTape k s d noiseCount .baseValue) = encodeWord B)
    (hC : base (headerTape k s d noiseCount .capacity) = encodeWord C) :
    MachineOutcomeRows.Invariant (Slots k s d noiseCount) B C
      (AddressOutcomeSpecs.values (AddressTupleLoaded.canonicalValues F tuple))
      (MachineOutcomeRows.selected (AddressOutcomeSpecs.rows k T) (rhs F tuple))
      (loaded F tuple base) := by
…

    Mentions: OAI.MaxCutGames.Integration.NoiseTables.Table, OAI.MaxCutGames.Integration.AddressTupleBody.Arena, OAI.MaxCutGames.Integration.AddressTupleBody.Ready, OAI.MaxCutGames.Integration.AddressTupleBody.Slots, OAI.MaxCutGames.Integration.AddressTupleLoaded.canonicalValues, OAI.MaxCutGames.Integration.AddressTupleBody.rhs, OAI.MaxCutGames.Integration.AddressTupleBody.loaded

  123. def OAI.MaxCutGames.Integration.AddressTupleBody.run_fixed_rows line 837

    Source documentation

    Actual fixed-row execution. Physical readiness and stored header values are its only data hypotheses; no template or body-execution premise remains.

    noncomputable def run_fixed_rows (T : NoiseTables.Table s d)
    (labels : Label k s d noiseCount (AddressOutcomeSpecs.rows k T) → Λ) (exit : Option Λ)
    (P : Λ → TM2.Stmt (fun _ : Arena k s d noiseCount => Bool) Λ (BodyState k))
    (atLabels : ∀l, P (labels l) = instruction (AddressOutcomeSpecs.rows k T) labels exit l)
    (F : SourceEncoding.Input) (tuple : Fin k → Fin F.equations.length)
    (base : Arena k s d noiseCount → List Bool) (ready : Ready F tuple base)
    (clean : MachineAddressEdge.Clean (Slots k s d noiseCount) base)
    (oldRhs : Fin k → Bool) (B C : Nat)
    (hB : base (headerTape k s d noiseCount .baseValue) = encodeWord B)
    (hC : base (headerTape k s d noiseCount .capacity) = encodeWord C) :
    StateTransition.EvalsToInTime (TM2.step P)
      ⟨some (labels (main (AddressOutcomeSpecs.rows k T))), (((oldRhs, ()), ()), none), base⟩
…

    Mentions: OAI.MaxCutGames.Integration.NoiseTables.Table, OAI.MaxCutGames.Integration.AddressTupleBody.Label, OAI.MaxCutGames.Integration.AddressTupleBody.Arena, OAI.MaxCutGames.Integration.AddressTupleBody.BodyState, OAI.MaxCutGames.Integration.AddressTupleBody.instruction, OAI.MaxCutGames.Integration.AddressTupleBody.Ready, OAI.MaxCutGames.Integration.AddressTupleBody.Slots, OAI.MaxCutGames.Integration.AddressTupleBody.main

  124. theorem OAI.MaxCutGames.Integration.AddressTupleBody.finalTapes_eq line 858
  125. def OAI.MaxCutGames.Integration.AddressTupleBody.run_actual line 866
  126. theorem OAI.MaxCutGames.Integration.AddressTupleBody.saved_of_current line 892