PoweringPlanBudget.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Execution budget of the concrete powered-row field plan

The cost is the sum of the actual relation and endpoint-comparison transition counts. Each fixed command scans only the serialized input graph. The execution certificates below instantiate the concrete plan trace; no execution witness or running-time bound is assumed.

def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPlanBudget.fieldBudget line 21
Source documentation
A common bound for either concrete field operation of radius at most max.
```
def fieldBudget (max inputLength : Nat) : Nat :=
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPlanBudget.field_steps_le line 24
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPlanBudget.plan_steps_le line 50
Source documentation
Sum the actual recursive cost, including its changing intermediate tapes.
```
theorem plan_steps_le (graph : PortTables.Table vertices d)
    (placement : PoweringMachineTapes.Tape max → K) (vertex : Fin vertices)
    (commands : List (PoweringMachinePlan.Command d max)) (base : K → List Bool) :
    PoweringMachinePlan.steps graph placement vertex commands base ≤
      commands.length * fieldBudget max (PortTables.tableBits graph).length := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.Command, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPlanBudget.fieldBudget
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPlanBudget.boundedRowPlan_length line 68
Source documentation
This is the actual static instruction list's length, not a supplied bound.
```
@[simp] theorem boundedRowPlan_length (n : Nat)
    (ports : Fin (n + 1) → Fin d) (direction : Bool) :
    (PoweringMachinePlan.boundedRowPlan n ports direction).length =
      PoweringMachineRow.inputSize (n + 1) (PoweringRowData.slotCount d n) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.inputSize
def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPlanBudget.rowBudget line 75
Source documentation
For fixed degree and radius this is affine in the serialized graph length.
```
def rowBudget (d n inputLength : Nat) : Nat :=
…
```

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPlanBudget.rowPlan_steps_le line 80

Source documentation

The backwards plan that produces the actual row-data tape obeys this bound.

theorem rowPlan_steps_le (graph : PortTables.Table vertices d) (n : Nat)
    (ports : Fin (n + 1) → Fin d) (direction : Bool)
    (placement : PoweringMachineTapes.Tape (2 * (n + 1)) → K)
    (vertex : Fin vertices) (base : K → List Bool) :
    PoweringMachinePlan.steps graph placement vertex
        (PoweringMachinePlan.boundedRowPlan n ports direction).reverse base ≤
      PoweringMachineRow.inputSize (n + 1) (PoweringRowData.slotCount d n) *
        ((28 * (2 * (n + 1)) + 10) * (PortTables.tableBits graph).length +
          24 * (2 * (n + 1)) + 15) := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.steps, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineRow.inputSize

def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPlanBudget.planInTime line 94

Source documentation

A genuine execution certificate for an arbitrary concrete bounded plan.

def planInTime (graph : PortTables.Table vertices d)
    (placement : PoweringMachineTapes.Tape max → K) (distinct : Function.Injective placement)
    (vertex : Fin vertices) (commands : List (PoweringMachinePlan.Command d max))
    (labels : PoweringMachinePlan.Label commands → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineUnaryEqualityBit.State A))
    (atLabels : ∀ l, program (labels l) =
      PoweringMachinePlan.instruction placement commands labels exit l)
    (base : K → List Bool) (suffix : List Bool)
    (ready : PoweringMachineField.Ready graph placement vertex suffix base) (ambient : A) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨PoweringMachinePlan.entry commands labels exit, MachineUnaryEqualityBit.clean ambient, base⟩
      (some ⟨exit, MachineUnaryEqualityBit.clean ambient,
…

def OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringPlanBudget.rowPlanInTime line 114

Source documentation

The actual row-data plan runs within the explicit fixed-plan affine bound.

def rowPlanInTime (graph : PortTables.Table vertices d) (n : Nat)
    (ports : Fin (n + 1) → Fin d) (direction : Bool)
    (placement : PoweringMachineTapes.Tape (2 * (n + 1)) → K)
    (distinct : Function.Injective placement) (vertex : Fin vertices)
    (labels : PoweringMachinePlan.Label
      (PoweringMachinePlan.boundedRowPlan n ports direction).reverse → Λ)
    (exit : Option Λ)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineUnaryEqualityBit.State A))
    (atLabels : ∀ l, program (labels l) = PoweringMachinePlan.instruction placement
      (PoweringMachinePlan.boundedRowPlan n ports direction).reverse labels exit l)
    (base : K → List Bool) (suffix : List Bool)
    (ready : PoweringMachineField.Ready graph placement vertex suffix base) (ambient : A) :
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineTapes.Tape, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryEqualityBit.State, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachinePlan.instruction, OAI.UniqueGamesTheorem.Foundations.Complexity.PoweringMachineField.Ready