Separate guarantees for the construction program
Lax235315.ConstructionContracts · concepts/Lax235315/ConstructionContracts.lean · lax-235315
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
The construction has three independent obligations. Every random tape must halt within the time budget. A run that reaches the final halt with its success flag set must output a suitable graph Welzl order. At least two thirds of all tapes must reach such a successful termination.
For a resource constant K, the time budget and tape length are both K(|x|+1)(ceil(log₂ n)+1). The word-size condition is exactly the condition of Lax195003 with that same K.
Concept map
Lean source view on GitHub
| 1 | import Lax235315.ConstructionProgram |
| 2 | import Lax195003.WelzlOrdersComputation |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Separate guarantees for the construction program |
| 7 | type: definition |
| 8 | --- |
| 9 | The construction has three independent obligations. Every random tape must |
| 10 | halt within the time budget. A run that reaches the final halt with its |
| 11 | success flag set must output a suitable graph Welzl order. At least two |
| 12 | thirds of all tapes must reach such a successful termination. |
| 13 | |
| 14 | For a resource constant K, the time budget and tape length are both |
| 15 | K(|x|+1)(ceil(log₂ n)+1). The word-size condition is exactly the condition |
| 16 | of Lax195003 with that same K. |
| 17 | |
| 18 | # Formalization notes |
| 19 | |
| 20 | The successful-tape event checks the actual program counter and a designated |
| 21 | memory cell. It does not assume that the output is correct. The separate |
| 22 | output theorem must establish that implication. |
| 23 | The three contracts are predicates, not fields assumed by a program object. |
| 24 | They use the registered machine, CSR encoding, neighborhood complexity and |
| 25 | output relation directly. Each later claim supplies its own sufficient lower |
| 26 | bound on K; taking a common upper bound permits their composition without |
| 27 | guessing a numerical constant before the cost proof is complete. |
| 28 | -/ |
| 29 | |
| 30 | namespace Lax235315.ConstructionContracts |
| 31 | open Lax808846.Ram Lax11.GraphEncoding |
| 32 | open Lax195003.WelzlOrdersNeighborhoodComplexity |
| 33 | open Lax195003.WelzlOrdersInGraphs Lax195003.WordRamRandomness |
| 34 | open Lax235315.ConstructionProgram |
| 35 | |
| 36 | /-- The common step budget and random-tape length. -/ |
| 37 | def timeBudget (K n : ℕ) (x : List ℕ) : ℕ := |
| 38 | K * (x.length + 1) * (Nat.clog 2 n + 1) |
| 39 | |
| 40 | /-- A linearly bounded graph, its CSR encoding, and the registered word-size condition. -/ |
| 41 | def ValidInput (K c n w : ℕ) (G : SimpleGraph (Fin n)) (x : List ℕ) : Prop := |
| 42 | 1 ≤ c ∧ HasLinearNeighborhoodComplexityWithConstant G c ∧ |
| 43 | EncodesGraph x n G ∧ |
| 44 | (∀ v ∈ c :: x, K * (x.length + v + 1) ≤ 2 ^ w) |
| 45 | |
| 46 | /-- Termination at the final instruction with the success flag set, within T steps. -/ |
| 47 | def SuccessfulTermination (w : ℕ) (input : List ℕ) (T : ℕ) |
| 48 | (s : State) (t : ℕ) : Prop := |
| 49 | t + 1 ≤ T ∧ run w program t (initState input) = some s ∧ |
| 50 | step w program s = none ∧ s.pc + 1 = program.length ∧ |
| 51 | s.mem successFlagCell = 1 |
| 52 | |
| 53 | /-- The random tapes whose execution reaches a successful final state. -/ |
| 54 | def goodTapes (w c : ℕ) (x : List ℕ) (T : ℕ) : Set (Fin T → Bool) := |
| 55 | {ρ | ∃ s t, SuccessfulTermination w ((c :: x) ++ bitTape ρ) T s t} |
| 56 | |
| 57 | /-- Every random tape leads to a halted run within the common budget. -/ |
| 58 | def HasRunningTimeBound (K : ℕ) : Prop := |
| 59 | ∀ (c n w : ℕ) (G : SimpleGraph (Fin n)) (x : List ℕ), |
| 60 | ValidInput K c n w G x → |
| 61 | ∀ ρ : Fin (timeBudget K n x) → Bool, |
| 62 | ∃ y : List ℕ, ∃ t ≤ timeBudget K n x, |
| 63 | RunsTo w program ((c :: x) ++ bitTape ρ) y t |
| 64 | |
| 65 | /-- Every successful final state contains an output meeting the registered crossing bound. -/ |
| 66 | def HasCorrectOutput (K : ℕ) : Prop := |
| 67 | ∀ (c n w : ℕ) (G : SimpleGraph (Fin n)) (x : List ℕ), |
| 68 | ValidInput K c n w G x → |
| 69 | ∀ (ρ : Fin (timeBudget K n x) → Bool) (s : State) (t : ℕ), |
| 70 | SuccessfulTermination w ((c :: x) ++ bitTape ρ) (timeBudget K n x) s t → |
| 71 | EncodesGraphWelzlOrder G 1 (12 * c ^ 2 * (Nat.clog 2 n) ^ 2) s.out |
| 72 | |
| 73 | /-- At least two thirds of the equally likely tapes reach a successful final state. -/ |
| 74 | noncomputable def HasSuccessProbability (K : ℕ) : Prop := |
| 75 | ∀ (c n w : ℕ) (G : SimpleGraph (Fin n)) (x : List ℕ), |
| 76 | ValidInput K c n w G x → |
| 77 | (2 / 3 : ℚ) * (2 ^ timeBudget K n x : ℚ) ≤ |
| 78 | ((goodTapes w c x (timeBudget K n x)).ncard : ℚ) |
| 79 | |
| 80 | end Lax235315.ConstructionContracts |
| 81 |
Formalization notes
The successful-tape event checks the actual program counter and a designated memory cell. It does not assume that the output is correct. The separate output theorem must establish that implication. The three contracts are predicates, not fields assumed by a program object. They use the registered machine, CSR encoding, neighborhood complexity and output relation directly. Each later claim supplies its own sufficient lower bound on K; taking a common upper bound permits their composition without guessing a numerical constant before the cost proof is complete.
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments