OAI/Computability/UniqueGames/Machines/MachinePaddedExpanderFamilyBoundsLemmas.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timeCoefficient line 15
2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timePolynomial line 18
3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timePolynomial_encoding line 21
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.ceilingCost_le line 26
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.combinedCost_le line 42
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.familyCost_le line 52
7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputWord line 62
8. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputCoefficient line 67
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputWord_length_le line 71

   Source documentation

   Complete unary rotation-table output, including every delimiter.

   theorem outputWord_length_le
       (H : Table (cloudSize PCP.Expanders.baseDegree) PCP.Expanders.baseDegree) (k : Nat) :
       (outputWord H k).length ≤ outputCoefficient * (k + 1)^2 := by
   …

   Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.Expanders.baseDegree, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputWord, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputCoefficient

10. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree line 103
11. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable line 104
12. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.Tape line 105
13. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.Alphabet line 106
14. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.Label line 107
15. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.State line 108
16. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyTape line 110
17. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyView line 112
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyView_left line 116
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyView_right line 119
20. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingTape line 130

    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.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.Tape

21. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView line 134
22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView_left line 140
23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView_right line 144
24. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyLabel line 156
25. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingLabel line 157
26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.main line 158
27. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry line 159
28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingStates line 161
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingStates_apply line 165
30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familySource line 174

    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.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.State

31. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingSource line 182

    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.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.State

32. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.program line 189

    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.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCloudPadding.Placement.statement, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familySource, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingTape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingSource

33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.program_family line 196
34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.program_ceiling line 202
35. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.initialState line 208

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.State

36. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalState line 211
37. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes line 216

    Source documentation

    Only the unary request is initially present.

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

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

38. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.retainedCeilingTapes line 220
39. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes line 224
40. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes line 229
41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes_input line 234
42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_input line 237
43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_power line 240
44. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingInput line 248
45. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingOutput line 251
46. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.retainedFrame line 256
47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_initial_tapes line 260
48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_handoff_tapes line 271

    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.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingOutput, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes

49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.family_initial_tapes line 287
50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.family_final_tapes line 295
51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_initial_configuration line 303
52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_handoff_configuration line 313

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateEquiv.configuration, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingStates, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingOutput, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes

53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.family_initial_configuration line 323

    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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyView, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.retainedFrame, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameConfiguration, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.configuration, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.alphabet_eq, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialTapes, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.boundedLevel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes

54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.family_final_configuration line 337

    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.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyView, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyLabel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.retainedFrame, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineStateFrame.frameConfiguration, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineAlphabetTransport.configuration, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.alphabet_eq, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.baseDegree_positive, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.caller, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.familyTapes, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.boundedLevel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes

55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes_level line 351
56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes_level_shadow line 358
57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_level_shadow line 361
58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_remainingLevel line 364
59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_currentSize line 371
60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_table line 378
61. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingInTime line 400

    Source documentation

    Actual geometric search, placed onto the eventual family-level tape.

    noncomputable def ceilingInTime (H : SmallTable) (requested : Nat)
        (state : MachineExpanderFamily.State ρ fixedDegree) (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step (program H))
          ⟨some main, initialState state register, initialTapes requested⟩
          (some ⟨some familyEntry, (state, (false, none)), handoffTapes requested⟩)
          ((MachineCeilingPower.timePolynomial PCP.ExpanderFamily.growth).eval
            (encodeWord requested).length) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.main, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.initialState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineCeilingPower.timePolynomial, OAI.UniqueGamesTheorem.Foundations.PCP.ExpanderFamily.growth, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

62. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.materializeInTime line 424

    Source documentation

    Actual table materialization consumes the level produced by the preceding phase while retaining the original request and its computed padded size.

    noncomputable def materializeInTime (H : SmallTable) (requested : Nat)
        (state : MachineExpanderFamily.State ρ fixedDegree) :
        StateTransition.EvalsToInTime (TM2.step (program H))
          ⟨some familyEntry, (state, (false, none)), handoffTapes requested⟩
          (some ⟨none, finalState H state, finalTapes H requested⟩)
          (MachineExpanderFamilyBounds.inputCoefficient * (requested + 1)^5) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamilyBounds.inputCoefficient

63. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.paddedInTime line 447

    Source documentation

    A single concrete finite program takes the original unary request all the way to the exact forward family table. Both phase executions are supplied by proved machines; there is no construction or runtime hypothesis.

    noncomputable def paddedInTime (H : SmallTable) (requested : Nat)
        (state : MachineExpanderFamily.State ρ fixedDegree) (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step (program H))
          ⟨some main, initialState state register, initialTapes requested⟩
          (some ⟨none, finalState H state, finalTapes H requested⟩)
          (MachinePaddedExpanderFamilyBounds.timePolynomial.eval (encodeWord requested).length) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.main, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.initialState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord

64. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.placedInTime line 465

    Source documentation

    Static placements of the complete computation into a larger caller preserve every complement tape and consume exactly the same runtime budget.

    noncomputable def placedInTime {K Λ : Type} [DecidableEq K]
        (tape : Tape → K) (view : K → Option Tape)
        (left : ∀ t, view (tape t) = some t)
        (right : ∀ j t, view j = some t → tape t = j)
        (labels : Label → Λ) (exit : Option Λ) (extra : K → List Bool)
        (H : SmallTable) (target : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State ρ))
        (code : ∀ l, target (labels l) = Placement.statement tape labels exit (program H l))
        (requested : Nat) (state : MachineExpanderFamily.State ρ fixedDegree)
        (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step target)
          (Placement.configuration view labels exit extra
            ⟨some main, initialState state register, initialTapes requested⟩)
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.main, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.initialState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes