OAI/Computability/UniqueGames/Machines/MachineFixedDivMod.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.Alphabet line 16
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.State line 17
3. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.residue line 19
4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.nextResidue line 22
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.nextResidue_residue line 25
6. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.scanLoop line 31
7. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.emitter line 45

   Source documentation

   Each emitter is a fixed finite statement indexed by one of the d residues.

   def emitter (d : Nat) (positive : 0 < d) (remainder : K) (exit : Option Λ)
       (r : Fin d) : TM2.Stmt (Alphabet (K := K)) Λ (State σ d) :=
   …

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

8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.scanPushBound line 52
9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.emitterPushBound line 58
10. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.tapes line 66

    Source documentation

    Three designated tapes, with the complete surrounding tape family retained.

    abbrev tapes (source quotient remainder : K) (base : K → List Bool)
        (input quotientWord remainderWord : List Bool) : K → List Bool :=
    …

11. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.unaryTapes line 70
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.unaryTapes_source line 75
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.unaryTapes_quotient line 83
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.unaryTapes_remainder line 90
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.unaryTapes_other line 97
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.update_source line 105
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.update_quotient line 123
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.update_remainder line 137
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.scanAux_true line 143
20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.scanAux_false line 159
21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.scanStep_succ line 174

    Source documentation

    A scan transition updates the actual quotient and finite residue of the already-processed count. The count itself is a proof index, not machine state.

    theorem scanStep_succ (d : Nat) (positive : 0 < d) (source quotient remainder : K)
        (sourceQuotient : source ≠ quotient) (sourceRemainder : source ≠ remainder)
        (quotientRemainder : quotient ≠ remainder) (scanLabel : Λ) (emitterLabel : Fin d → Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ d))
    …

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

22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.scanStep_zero line 201
23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.emitterStep line 224
24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.trace_fromCount line 250

    Source documentation

    The general invariant starts at the finite residue and unary quotient of k, then scans n additional input bits. It is an actual execution theorem.

    theorem trace_fromCount (d : Nat) (positive : 0 < d) (source quotient remainder : K)
        (sourceQuotient : source ≠ quotient) (sourceRemainder : source ≠ remainder)
        (quotientRemainder : quotient ≠ remainder) (scanLabel : Λ) (emitterLabel : Fin d → Λ)
        (exit : Option Λ) (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ d))
    …

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

25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.divModTrace line 288

    Source documentation

    Exact unary quotient and remainder, with both output counters initially zero.

    theorem divModTrace (d : Nat) (positive : 0 < d) (source quotient remainder : K)
        (sourceQuotient : source ≠ quotient) (sourceRemainder : source ≠ remainder)
        (quotientRemainder : quotient ≠ remainder) (scanLabel : Λ) (emitterLabel : Fin d → Λ)
        (exit : Option Λ) (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ d))
    …

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

26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.divModFromTapes line 310

    Source documentation

    Caller-frame form: the only initial tape hypotheses are the three unary prefixes.

    theorem divModFromTapes (d : Nat) (positive : 0 < d) (source quotient remainder : K)
        (sourceQuotient : source ≠ quotient) (sourceRemainder : source ≠ remainder)
        (quotientRemainder : quotient ≠ remainder) (scanLabel : Λ) (emitterLabel : Fin d → Λ)
        (exit : Option Λ) (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ d))
    …

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

27. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.divModInTime line 337
28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.scanTrace_fromCount line 362

    Source documentation

    Stop just before emission, retaining the final finite residue as actual control.

    theorem scanTrace_fromCount (d : Nat) (positive : 0 < d) (source quotient remainder : K)
        (sourceQuotient : source ≠ quotient) (sourceRemainder : source ≠ remainder)
        (quotientRemainder : quotient ≠ remainder) (scanLabel : Λ) (emitterLabel : Fin d → Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ d))
    …

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

29. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.emitterWithFinish line 396

    Source documentation

    A fixed table on finite ambient control may retain the residue before local reset.

    def emitterWithFinish [Fintype σ] (d : Nat) (positive : 0 < d) (remainder : K)
        (exit : Option Λ) (finish : σ → Fin d → σ) (r : Fin d) :
        TM2.Stmt (Alphabet (K := K)) Λ (State σ d) :=
    …

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

30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.emitterWithFinishPushBound line 404
31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.emitterWithFinishStep line 412
32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.divModTraceWithFinish line 439

    Source documentation

    The callback is a fixed finite-control table, applied in the existing emitter transition.

    theorem divModTraceWithFinish [Fintype σ] (d : Nat) (positive : 0 < d)
        (source quotient remainder : K)
        (sourceQuotient : source ≠ quotient) (sourceRemainder : source ≠ remainder)
        (quotientRemainder : quotient ≠ remainder) (scanLabel : Λ) (emitterLabel : Fin d → Λ)
        (exit : Option Λ) (finish : σ → Fin d → σ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ d))
    …

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

33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFixedDivMod.divModFromTapesWithFinish line 467