Executable.lean`

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Quantitative compilation measured in ordinary TM0 transitions.

def OAI.RationalHitting.ExecutableGenerator.inputTables line 9
Source documentation
Dense, staged integer input tables. No quotient-field element is computed.
```
def inputTables (n N e : ℕ) (x : Fin 3 → ℕ) : Vector (Table (Generator.D e)) (n+1) :=
…
```
Mentions: OAI.RationalHitting.Generator.D
lemma OAI.RationalHitting.ExecutableGenerator.inputTables_denote line 12
def OAI.RationalHitting.ExecutableGenerator.normalizedEntry line 17
Source documentation
Cramer's numerators are computed by the staged division-free algorithm.
```
def normalizedEntry {d : ℕ} (A B : Table d) (den : ℤ) (i j : Fin d) : ℚ :=
…
```
lemma OAI.RationalHitting.ExecutableGenerator.normalizedEntry_spec line 20
abbrev OAI.RationalHitting.ExecutableGenerator.RationalTable line 26
def OAI.RationalHitting.ExecutableGenerator.tuple line 28
def OAI.RationalHitting.ExecutableGenerator.normalized line 31
lemma OAI.RationalHitting.ExecutableGenerator.tuple_normalized line 35
def OAI.RationalHitting.ExecutableGenerator.atPoint line 41
Source documentation
The only singularity test; all repeated algebra is materialized in dense tables.
```
def atPoint (n N e : ℕ) (x : Fin 3 → ℕ) : Option (Tuple n (Generator.D e)) :=
…
```
Mentions: OAI.RationalHitting.Tuple, OAI.RationalHitting.Generator.D
lemma OAI.RationalHitting.ExecutableGenerator.U_det_eq_zero line 46
theorem OAI.RationalHitting.ExecutableGenerator.atPoint_spec line 66
Source documentation
Exact pointwise equality, including points rejected by the original determinant test.
```
theorem atPoint_spec (n N e : ℕ) (x : Fin 3 → ℕ) :
    atPoint n N e x = Generator.atPoint n N e x := by
…
```
Mentions: OAI.RationalHitting.ExecutableGenerator.atPoint, OAI.RationalHitting.Generator.atPoint
def OAI.RationalHitting.ExecutableGenerator.output line 81
Source documentation
A computable generator preserving the list and its order.
```
def output (n N e H : ℕ) : Output n where
…
```
Mentions: OAI.RationalHitting.Output
theorem OAI.RationalHitting.ExecutableGenerator.output_spec line 86
def OAI.RationalHitting.ExecutableGenerator.list line 89
theorem OAI.RationalHitting.ExecutableGenerator.list_spec line 92
def OAI.RationalHitting.ExecutableGenerator.encoded line 94
theorem OAI.RationalHitting.ExecutableGenerator.encoded_spec line 96
theorem OAI.RationalHitting.ExecutableGenerator.exact_output line 107
Source documentation
The hitting property and output-size bounds for the computed list.
```
theorem exact_output (n s : ℕ) (hn : 1 ≤ n) (hs : 1 ≤ s) :
    (list n s).dimension ≤ 256*(n+s+1)^10 ∧
    (encodeOutput (list n s)).length ≤ PolynomialBounds.outputConstant*(n+s+1)^104 ∧
    Hits s (list n s) := by
…
```
Mentions: OAI.RationalHitting.ExecutableGenerator.list, OAI.RationalHitting.encodeOutput, OAI.RationalHitting.PolynomialBounds.outputConstant, OAI.RationalHitting.Hits
def OAI.RationalHitting.ExecutableGenerator.Implementation line 118
Source documentation
A finite-state implementation with polynomial transition count.
```
def Implementation : Prop :=
…
```
theorem OAI.RationalHitting.ExecutableGenerator.main_of_implementation line 123
Source documentation
The finite-state implementation and list bounds imply the main statement.
```
theorem main_of_implementation (hi : Implementation) : MainStatement := by
…
```
Mentions: OAI.RationalHitting.ExecutableGenerator.Implementation, OAI.RationalHitting.MainStatement