OAI/Computability/MaxCut/Machines/GraphCounterFinish.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Actual cleanup and emission of the counter followed by the preserved graph.

  1. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterFinish.extraTapes line 12
  2. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterFinish.frame line 17
  3. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterFinish.trace_trans_inline_GraphCounterFinish line 24
  4. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterFinish.start_eq line 28
  5. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterFinish.finish_eq line 41
  6. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterFinish.drainTrace line 53
  7. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterFinish.clockCopyTrace line 70
  8. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterFinish.archiveCopyTrace line 91
  9. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterFinish.reverseTrace line 113
  10. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterFinish.finishTrace line 138
  11. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterFinish.finishInTime line 153
  12. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterPrefix.rawOutput line 171
  13. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterPrefix.rawInTime line 174
  14. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterPrefix.count line 198
  15. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterPrefix.output line 200
  16. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterPrefix.rowsBits line 203
  17. theorem OAI.MaxCutGames.Foundations.Complexity.GraphCounterPrefix.tableBits_decomposition line 206
  18. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterPrefix.outputsInTime line 210
  19. def OAI.MaxCutGames.Foundations.Complexity.GraphCounterPrefix.computableInPolyTime line 216
  20. def OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.rounds line 246
  21. theorem OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.rounds_le line 248
  22. theorem OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.two_pow_rounds_le line 251
  23. theorem OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.growth_pow_rounds_le line 259

    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.MaxCutGames.Foundations.Complexity.PCPIterationMachine.rounds

  24. def OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.sizeEnvelope line 267
  25. theorem OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.semanticSize_geometric line 270

    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.MaxCutGames.Foundations.Complexity.PCPIterationMachine.rounds

  26. theorem OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.semanticSize_bound line 284
  27. def OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.sizePolynomial line 297
  28. theorem OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.sizePolynomial_eval line 300
  29. def OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.timePolynomial line 306

    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 :=
…
  30. theorem OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.timePolynomial_eval line 311
  31. abbrev OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.Alphabet line 319
  32. abbrev OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.State line 320
  33. abbrev OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.Labels line 321
  34. def OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.program line 325

    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.MaxCutGames.Foundations.Complexity.PCPIterationMachine.Alphabet, OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.Labels, OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.State

  35. theorem OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.program_guard line 333
  36. def OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.machine line 340

    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.MaxCutGames.Foundations.Complexity.PCPIterationMachine.Alphabet, OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.Labels, OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.State

  37. def OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.haltedConfiguration line 353
  38. theorem OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.haltStep line 358
  39. theorem OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.iterationTrace line 371

    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.MaxCutGames.Foundations.Complexity.PCPIterationMachine.Alphabet, OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.Labels, OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.State

  40. theorem OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.bodyCosts_bound line 390

    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.MaxCutGames.Foundations.Complexity.PCPIterationMachine.rounds, OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.sizeEnvelope

  41. def OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.iterationInTime line 409

    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.MaxCutGames.Foundations.Complexity.PCPIterationMachine.Alphabet, OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.Labels, OAI.MaxCutGames.Foundations.Complexity.PCPIterationMachine.State