OAI/Computability/MaxCut/Machines/MachineExpanderFamilyCycle.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

Actual counted repetition of complete table-expansion cycles. The input counter is physically decremented, and the invariant carries the exact table at the completed family level.

  1. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.installed_returnFrame line 13
  2. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.cleaned_multipliedFrame line 24
  3. structure OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.ResizeRun line 40
  4. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.resizeInTime line 55

    Source documentation

    The resize certificate is built from actual primitive and table executions; its caller supplies no phase trace or computational hypothesis.

    noncomputable def resizeInTime {v d : Nat} {ρ : Type} [Fintype ρ]
    (positive : 0 < d) (H : Table (cloudSize d) d) (growth : 1 < cloudSize d)
    (G : Table v (degree d)) (remaining : Nat) (state : State ρ d) (suffix : List Bool) :
    ResizeRun positive H growth G remaining state suffix := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.ResizeRun

  5. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.caller_initialState line 131
  6. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.caller_normalizeState line 134
  7. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_initialState line 137
  8. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes_update_level line 142

    Source documentation

    The guard changes only the physical remaining-level word.

    theorem boundaryTapes_update_level (remaining current next : Nat)
    (word suffix : List Bool) :
    Function.update (boundaryTapes remaining current word suffix)
      (.inr .remainingLevel) (encodeWord next ++ suffix) =
      boundaryTapes next current word suffix := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  9. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialTapes_initialize line 155

    Source documentation

    The two literal prefixes install the actual level-zero table and unary one.

    theorem initialTapes_initialize (level : Nat) (suffix : List Bool) :
    Function.update
      (Function.update (initialTapes level suffix) tableTape (initialEncoding d))
      (.inr .currentSize) (encodeWord 1) =
      boundaryTapes level 1 (initialEncoding d) suffix := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.tableTape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialEncoding, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes

  10. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.actualStep_of_boolStep line 173

    Source documentation

    Static alphabet transport preserves this actual single transition.

    theorem actualStep_of_boolStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d)
    (start finish : TM2.Cfg BoolAlphabet (Label d) (State ρ d))
    (run : TM2.step (boolView positive H growth) start = some finish) :
    TM2.step (program positive H growth)
      (MachineAlphabetTransport.configuration alphabet_eq.symm start) =
      some (MachineAlphabetTransport.configuration alphabet_eq.symm finish) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Label, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.boolView, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.configuration

  11. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.bool_initializeStep line 186
  12. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.bool_levelGuard_succStep line 199
  13. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.bool_levelGuard_zeroStep line 212
  14. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.bool_doneStep line 224
  15. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initializeStep line 233

    Source documentation

    The literal initialization executes in one transition of the actual program.

    theorem initializeStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d) (base : ∀ tape, List (Alphabet tape)) (state : State ρ d) :
    TM2.step (program positive H growth) ⟨some (.inr .initialize), state, base⟩ =
      some ⟨some (.inr .levelGuard), normalizeState positive H state,
        Function.update
          (Function.update base tableTape (initialEncoding d ++ base (.inl (.inl .table))))
          (.inr .currentSize) (encodeWord 1 ++ base (.inr .currentSize))⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.normalizeState, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.tableTape, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialEncoding, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  16. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_succStep line 246

    Source documentation

    A positive level physically loses one true bit, retaining its delimiter and suffix.

    theorem levelGuard_succStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d) (base : ∀ tape, List (Alphabet tape)) (state : State ρ d)
    (remaining : Nat) (suffix : List Bool)
    (counter : base (.inr .remainingLevel) = encodeWord (remaining + 1) ++ suffix) :
    TM2.step (program positive H growth) ⟨some (.inr .levelGuard), state, base⟩ =
      some ⟨some (.inr (.affine .copyCount .seed)), clearRegister state,
        Function.update base (.inr .remainingLevel) (encodeWord remaining ++ suffix)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister

  17. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_zeroStep line 260

    Source documentation

    The zero delimiter is retained when the family loop enters its final halt.

    theorem levelGuard_zeroStep (positive : 0 < d) (H : Table (cloudSize d) d)
    (growth : 1 < cloudSize d) (base : ∀ tape, List (Alphabet tape)) (state : State ρ d)
    (suffix : List Bool)
    (counter : base (.inr .remainingLevel) = encodeWord 0 ++ suffix) :
    TM2.step (program positive H growth) ⟨some (.inr .levelGuard), state, base⟩ =
      some ⟨some (.inr .done), clearRegister state, base⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.encodeWord, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister

  18. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.doneStep line 270
  19. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialize_boundaryStep line 278
  20. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_boundary_succStep line 294
  21. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_boundary_zeroStep line 305
  22. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost line 327
  23. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost_prefix line 332
  24. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost_zero_start line 345
  25. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.levelLoopTapes line 350
  26. structure OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.LevelLoopRun line 355
  27. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.familySingleStep_inline_MachineExpanderFamilyLoop line 365
  28. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.levelLoopInTime line 373

    Source documentation

    Every body is the already constructed actual resize run. There is no whole-loop, body-trace, or computational-correctness premise.

    noncomputable def levelLoopInTime {d : Nat} {ρ : Type} [Fintype ρ]
    (positive : 0 < d) (H : Table (cloudSize d) d) (growth : 1 < cloudSize d)
    (completed remaining : Nat) (state : State ρ d) (suffix : List Bool) :
    LevelLoopRun positive H growth completed remaining state suffix := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.LevelLoopRun

  29. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.singleFamilyStep_inline_MachineExpanderFamily line 419
  30. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.familyInTime line 426

    Source documentation

    Complete initialization, actual counted loop, and normalized halt.

    noncomputable def familyInTime {d : Nat} {ρ : Type} [Fintype ρ]
    (positive : 0 < d) (H : Table (cloudSize d) d) (growth : 1 < cloudSize d)
    (level : Nat) (state : State ρ d) (suffix : List Bool) :
    StateTransition.EvalsToInTime (TM2.step (program positive H growth))
      ⟨some (.inr .initialize), state, initialTapes level suffix⟩
      (some ⟨none, initialState positive H (caller state), familyTapes H level suffix⟩)
      (familyBudget H level) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialState, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.caller, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.familyTapes

  31. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.familyInOutputSizeTime line 464

    Source documentation

    The actual complete computation is polynomial in the final full vertex count; the level is never silently treated as an equally long input.

    noncomputable def familyInOutputSizeTime {d : Nat} {ρ : Type} [Fintype ρ]
    (positive : 0 < d) (H : Table (cloudSize d) d) (growth : 1 < cloudSize d)
    (level : Nat) (state : State ρ d) (suffix : List Bool) :
    StateTransition.EvalsToInTime (TM2.step (program positive H growth))
      ⟨some (.inr .initialize), state, initialTapes level suffix⟩
      (some ⟨none, initialState positive H (caller state), familyTapes H level suffix⟩)
      ((resizeCoefficient d + 4) * (vertexCount (degree d) level + 1)^5) where
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialTapes, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialState, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.caller, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.familyTapes

  32. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_cloud_growth line 475
  33. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_cloud_gt_one line 480
  34. theorem OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_positive line 484
  35. def OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.paddedFamilyInTime line 495

    Source documentation

    At the physically computable padding level, the actual family run has a fixed polynomial bound in requested unary size. The separate ceiling-power machine supplies this exact level and preserves the requested size.

    noncomputable def paddedFamilyInTime {ρ : Type} [Fintype ρ]
    (H : Table (cloudSize PCP.Expanders.baseDegree) PCP.Expanders.baseDegree)
    (requested : Nat) (state : State ρ PCP.Expanders.baseDegree) (suffix : List Bool) :
    StateTransition.EvalsToInTime
      (TM2.step (program baseDegree_positive H baseDegree_cloud_gt_one))
      ⟨some (.inr .initialize), state,
        initialTapes (PCP.PreprocessingLevels.boundedLevel requested) suffix⟩
      (some ⟨none, initialState baseDegree_positive H (caller state),
        familyTapes H (PCP.PreprocessingLevels.boundedLevel requested) suffix⟩)
      (inputCoefficient * (requested + 1)^5) where
…

    Mentions: OAI.MaxCutGames.Foundations.PCP.Expanders.baseDegree, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.program, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_positive, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_cloud_gt_one, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialTapes, OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.boundedLevel, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialState, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.caller, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.familyTapes

  36. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree line 518
  37. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable line 519
  38. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.Tape line 520
  39. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.Alphabet line 521
  40. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.Label line 522
  41. abbrev OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.State line 523
  42. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyTape line 525
  43. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView line 527
  44. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView_left line 531
  45. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView_right line 534
  46. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingTape line 545

    Source documentation

    The only shared tape is the level: the first phase writes the exact word that the second phase's unary guard consumes.

    def ceilingTape : MachineCeilingPower.Tape → Tape
  | .level => .inl (.inr .remainingLevel)
  | tape => .inr tape

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.Tape, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.Tape

  47. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView line 549
  48. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView_left line 555
  49. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView_right line 559
  50. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyLabel line 568
  51. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingLabel line 569
  52. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.main line 570
  53. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry line 571
  54. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingStates line 573
  55. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingStates_apply line 577
  56. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familySource line 584

    Source documentation

    The family retains the completed ceiling machine's two finite registers.

    def familySource (H : SmallTable) : MachineExpanderFamily.Label fixedDegree →
    TM2.Stmt MachineExpanderFamily.BoolAlphabet
      (MachineExpanderFamily.Label fixedDegree) (State ρ) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.Label, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.State

  57. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingSource line 592

    Source documentation

    The ceiling program preserves the family state as its ambient component.

    def ceilingSource : MachineCeilingPower.Label →
    TM2.Stmt MachineCeilingPower.Alphabet MachineCeilingPower.Label (State ρ) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.Label, OAI.MaxCutGames.Foundations.Complexity.MachineCeilingPower.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.State

  58. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.program line 599

    Source documentation

    Actual composition on shared Boolean tapes. No runtime bridge operation is required, because both programs use the same physical level tape.

    def program (H : SmallTable) : Label → TM2.Stmt Alphabet Label (State ρ)
  | .inl label =>
    MachineCloudPadding.Placement.statement familyTape familyLabel none (familySource H label)
  | .inr label =>
    MachineCloudPadding.Placement.statement ceilingTape ceilingLabel (some familyEntry)
      (ceilingSource (ρ := ρ) label)

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.Label, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.Alphabet, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachineCloudPadding.Placement.statement, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyTape, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyLabel, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familySource, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingTape, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingLabel, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingSource

  59. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.program_family line 606
  60. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.program_ceiling line 612
  61. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialState line 618

    Source documentation

    Initial state for an arbitrary preserved family-state component.

    def initialState (state : MachineExpanderFamily.State ρ fixedDegree)
    (register : Option Bool) : State ρ := (state, (false, register))

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.State

  62. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalState line 621
  63. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes line 626

    Source documentation

    Only the unary request is initially present.

    def initialTapes (requested : Nat) : Tape → List Bool
  | .inr .input => encodeWord requested
  | _ => []

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.Tape, OAI.MaxCutGames.Foundations.Complexity.encodeWord

  64. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.retainedCeilingTapes line 630
  65. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes line 634
  66. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes line 639
  67. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes_input line 644
  68. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_input line 647
  69. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_power line 650
  70. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingInput line 662
  71. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingOutput line 665
  72. def OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.retainedFrame line 670
  73. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_initial_tapes line 674
  74. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_handoff_tapes line 685

    Source documentation

    The produced unary level is already on the exact family input tape.

    theorem ceiling_handoff_tapes (requested : Nat) :
    Placement.tapes ceilingView (ceilingOutput requested) (fun _ => []) =
      handoffTapes requested := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingOutput, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes

  75. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_initial_tapes line 701
  76. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_final_tapes line 709
  77. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_initial_configuration line 717
  78. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_handoff_configuration line 727

    Source documentation

    Ceiling halt enters the family initializer with no intervening transition.

    theorem ceiling_handoff_configuration {ρ : Type} (requested : Nat)
    (state : MachineExpanderFamily.State ρ fixedDegree) :
    Placement.configuration ceilingView ceilingLabel (some familyEntry) (fun _ => [])
      (MachineStateEquiv.configuration (ceilingStates ρ)
        ⟨none, ((state, false), none), ceilingOutput requested⟩) =
      ⟨some familyEntry, (state, (false, none)), handoffTapes requested⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingLabel, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry, OAI.MaxCutGames.Foundations.Complexity.MachineStateEquiv.configuration, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingStates, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingOutput, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes

  79. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_initial_configuration line 737

    Source documentation

    Static alphabet and state framing of the actual family initial endpoint.

    theorem family_initial_configuration {ρ : Type} (requested : Nat)
    (state : MachineExpanderFamily.State ρ fixedDegree) (metadata : Bool × Option Bool) :
    Placement.configuration familyView familyLabel none (retainedFrame requested)
      (MachineStateFrame.frameConfiguration metadata
        (MachineAlphabetTransport.configuration MachineExpanderFamily.alphabet_eq
          ⟨some (.inr .initialize), state,
            MachineExpanderFamily.initialTapes (PCP.PreprocessingLevels.boundedLevel requested) []⟩)) =
      ⟨some familyEntry, (state, metadata), handoffTapes requested⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyLabel, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.retainedFrame, OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameConfiguration, OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.configuration, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.alphabet_eq, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialTapes, OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.boundedLevel, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes

  80. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_final_configuration line 751

    Source documentation

    The family endpoint retains both external ceiling words and its original normalized state; its remaining-level word is the consumed zero word.

    theorem family_final_configuration {ρ : Type} (H : SmallTable) (requested : Nat)
    (state : MachineExpanderFamily.State ρ fixedDegree) :
    Placement.configuration familyView familyLabel none (retainedFrame requested)
      (MachineStateFrame.frameConfiguration (false, none)
        (MachineAlphabetTransport.configuration MachineExpanderFamily.alphabet_eq
          ⟨none,
            MachineExpanderFamily.initialState MachineExpanderFamily.baseDegree_positive H
              (MachineExpanderFamily.caller state),
            MachineExpanderFamily.familyTapes H (PCP.PreprocessingLevels.boundedLevel requested) []⟩)) =
      ⟨none, finalState H state, finalTapes H requested⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.State, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyLabel, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.retainedFrame, OAI.MaxCutGames.Foundations.Complexity.MachineStateFrame.frameConfiguration, OAI.MaxCutGames.Foundations.Complexity.MachineAlphabetTransport.configuration, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.alphabet_eq, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.initialState, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_positive, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.caller, OAI.MaxCutGames.Foundations.Complexity.MachineExpanderFamily.familyTapes, OAI.MaxCutGames.Foundations.PCP.PreprocessingLevels.boundedLevel, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalState, OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes

  81. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes_level line 765
  82. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes_level_shadow line 772
  83. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_level_shadow line 775
  84. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_remainingLevel line 778
  85. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_currentSize line 785
  86. theorem OAI.MaxCutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_table line 792