OAI/Computability/UniqueGames/Machines/MachineUnaryLessAtLemmas.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Physical comparison of two unary fields. Matched true bits are saved on two empty scratch stacks. The first delimiter determines the comparison, then both saved prefixes are restored. All input suffixes and other tapes survive.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.Alphabet line 17
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.State line 18
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.zeroTest line 21

    Source documentation

    A boundary test which inspects the first unary bit without consuming it.

    def zeroTest (operand : K) (exit : Option Λ) :
    TM2.Stmt (Alphabet (K := K)) Λ (State σ) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.State

  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.zeroTestTrace line 27
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.tapes line 43

    Source documentation

    Slots 0 and 1 are the operands; slots 2 and 3 are their saved prefixes.

    def tapes (slots : Fin 4 ↪ K) (base : K → List Bool)
    (left right savedLeft savedRight : List Bool) : K → List Bool :=
…
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.tapes_left line 48
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.tapes_right line 53
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.tapes_savedLeft line 58
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.tapes_savedRight line 63
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.update_tapes line 68
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.tapes_self line 86
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.stop line 90
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.scan line 94
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.scan_step_zero_left line 109
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.scan_step_zero_right line 122
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.scan_step_succ line 135
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.scanTrace line 150
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.transferLeft_tapes line 181
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.transferRight_tapes line 188
  20. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.Label line 195
  21. instance OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.(instance at line 201) line 201
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.statement line 205
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.steps line 213
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.comparisonTrace line 215
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.lessThanTrace line 271

    Source documentation

    Actual comparison on a caller frame: both complete operand tapes and all other tapes are preserved, both scratch tapes remain empty, and the finite result flag is precisely the strict comparison of the two unary values.

    theorem lessThanTrace (slots : Fin 4 ↪ K) (labels : Label → Λ) (exit : Option Λ)
    (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.Label, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.State

  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.timePolynomial line 289
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.steps_le_time line 291
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.lessThanInPolynomialTime line 297
  29. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.machine line 313
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineUnaryLessAt.machineInPolynomialTime line 324
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.rounds line 349
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.rounds_le line 351
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.two_pow_rounds_le line 354
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.growth_pow_rounds_le line 362

    Source documentation

    The exponent is a fixed growth constant, independent of the input.

    theorem growth_pow_rounds_le (growth n : Nat) :
    growth ^ rounds n ≤ (2 * (n + 1)) ^ growth := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.rounds

  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.sizeEnvelope line 370
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.semanticSize_geometric line 373

    Source documentation

    This recurrence concerns semantic cardinality, not unary encoding length.

    theorem semanticSize_geometric (sizes : Nat → Nat) (growth n : Nat)
    (initialBound : sizes 0 ≤ n + 1)
    (growthBound : ∀ i, i < rounds n → sizes (i + 1) ≤ growth * sizes i)
    (i : Nat) (hi : i ≤ rounds n) : sizes i ≤ (n + 1) * growth ^ i := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.rounds

  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.semanticSize_bound line 387
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.sizePolynomial line 400
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.sizePolynomial_eval line 403
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.timePolynomial line 409

    Source documentation

    A polynomial in initial semantic size; two extra steps include the final zero guard and actual halt. The encoding polynomial is applied once.

    noncomputable def timePolynomial (growth : Nat)
    (encodingSize bodyTime : Polynomial Nat) : Polynomial Nat :=
…
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.timePolynomial_eval line 414
  42. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.Alphabet line 422
  43. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.State line 423
  44. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.Labels line 424
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.program line 428

    Source documentation

    A concrete guard and halt are added to the supplied body statements. The body may return to Sum.inl false; it starts at Sum.inr entry.

    def program (counter : K) (entry : Λ)
    (body : Λ → TM2.Stmt (Alphabet (K := K)) (Labels Λ) (State σ)) :
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.Labels, OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.State

  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.program_guard line 436
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.machine line 443

    Source documentation

    Finite packaging of the concrete control program. Callers supply a fixed finite body; no input-dependent collection of labels or states is introduced.

    def machine [Fintype K] [Fintype Λ] [Fintype σ]
    (counter output : K) (entry : Λ) (initial : σ)
    (body : Λ → TM2.Stmt (Alphabet (K := K)) (Labels Λ) (State σ)) : FinTM2 where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.Labels, OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.State

  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.haltedConfiguration line 456
  49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.haltStep line 461
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.iterationTrace line 474

    Source documentation

    Full loop execution including the final transition that consumes the counter delimiter and halts, retaining the unread suffix. The only supplied execution hypotheses concern individual body calls in this same program.

    theorem iterationTrace (counter : K) (entry : Λ)
    (body : Λ → TM2.Stmt (Alphabet (K := K)) (Labels Λ) (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.Labels, OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.State

  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.bodyCosts_bound line 493

    Source documentation

    Actual body costs are bounded through a semantic-size sequence and a separate encoding polynomial. Index rounds n - (r+1) is the forward round corresponding to the unary guard's remaining-count index r.

    theorem bodyCosts_bound (growth n : Nat) (growthPositive : 0 < growth)
    (sizes encodedSizes cost : Nat → Nat) (encodingSize bodyTime : Polynomial Nat)
    (initialBound : sizes 0 ≤ n + 1)
    (growthBound : ∀ i, i < rounds n → sizes (i + 1) ≤ growth * sizes i)
    (encodingBound : ∀ r, r < rounds n →
      encodedSizes r ≤ encodingSize.eval (sizes (rounds n - (r + 1))))
    (bodyCost : ∀ r, r < rounds n → cost r ≤ bodyTime.eval (encodedSizes r)) :
    ∀ r, r < rounds n →
      cost r ≤ bodyTime.eval (encodingSize.eval (sizeEnvelope growth n)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.rounds, OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.sizeEnvelope

  52. def OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.iterationInTime line 512

    Source documentation

    Timed execution of the concrete guard/body/halt program. This compositional interface is not a certificate for an unprovided graph-transformation body.

    def iterationInTime (counter : K) (entry : Λ)
    (body : Λ → TM2.Stmt (Alphabet (K := K)) (Labels Λ) (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.Alphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.Labels, OAI.UniqueGamesTheorem.Foundations.Complexity.PCPIterationMachine.State