OAI/Computability/UniqueGames/Machines/MachineExpanderFamily.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.singleFamilyStep line 11
2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.familyInTime line 18

   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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.caller, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.familyTapes

3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.familyInOutputSizeTime line 56

   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.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialTapes, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.caller, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.familyTapes

4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.baseDegree_cloud_growth line 67
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.baseDegree_cloud_gt_one line 72
6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.baseDegree_positive line 76
7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.paddedFamilyInTime line 87

   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.UniqueGamesTheorem.Foundations.PCP.Expanders.baseDegree, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.State, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.program, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.baseDegree_positive, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.baseDegree_cloud_gt_one, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialTapes, OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingLevels.boundedLevel, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.initialState, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.caller, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineExpanderFamily.familyTapes