AmplificationProgram.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

A binary stack-machine implementation of the exact rational Taylor amplification used for the binary nuclear charges. The input parameter D is unary; the large output and every arithmetic register are binary.

abbrev OAI.ContinuumCoulomb.AmplificationProgram.State line 16
def OAI.ContinuumCoulomb.AmplificationProgram.stateCode line 18
def OAI.ContinuumCoulomb.AmplificationProgram.step line 21
def OAI.ContinuumCoulomb.AmplificationProgram.start line 25
def OAI.ContinuumCoulomb.AmplificationProgram.partialTaylor line 27
theorem OAI.ContinuumCoulomb.AmplificationProgram.iterate_start line 31
Source documentation
Scaled numerator, factorial denominator and power are maintained by literal natural-number additions and multiplications.
```
theorem iterate_start (D n : ℕ) :
    ((step^[n]) (start D)).1 = D ∧
    ((step^[n]) (start D)).2.1 = n ∧
    (((step^[n]) (start D)).2.2.1 : ℚ) = (n.factorial : ℚ) * partialTaylor D n ∧
    ((step^[n]) (start D)).2.2.2.1 = n.factorial ∧
    ((step^[n]) (start D)).2.2.2.2 = D ^ n := by
…
```
Mentions: OAI.ContinuumCoulomb.AmplificationProgram.step, OAI.ContinuumCoulomb.AmplificationProgram.start, OAI.ContinuumCoulomb.AmplificationProgram.partialTaylor
theorem OAI.ContinuumCoulomb.AmplificationProgram.ceil_nat_ratio line 61
Source documentation
Natural ceiling of a nonnegative rational quotient is computed with addition, subtraction by one, and ordinary natural division.
```
theorem ceil_nat_ratio (A F : ℕ) (hF : 0 < F) :
    Nat.ceil ((A : ℚ) / F) = (A + F - 1) / F := by
…
```
def OAI.ContinuumCoulomb.AmplificationProgram.result line 77
theorem OAI.ContinuumCoulomb.AmplificationProgram.result_correct line 79
theorem OAI.ContinuumCoulomb.AmplificationProgram.bits_add_max line 93
Source documentation
Addition costs at most one more bit than the larger input.
```
theorem bits_add_max (a b : ℕ) :
    (a + b).bits.length ≤ max a.bits.length b.bits.length + 1 := by
…
```
theorem OAI.ContinuumCoulomb.AmplificationProgram.bits_succ line 107
def OAI.ContinuumCoulomb.AmplificationProgram.measure line 114
theorem OAI.ContinuumCoulomb.AmplificationProgram.stateCode_length line 117
theorem OAI.ContinuumCoulomb.AmplificationProgram.measure_le_code line 123
theorem OAI.ContinuumCoulomb.AmplificationProgram.code_le_measure line 130
theorem OAI.ContinuumCoulomb.AmplificationProgram.step_measure line 137
theorem OAI.ContinuumCoulomb.AmplificationProgram.iterate_D line 152
theorem OAI.ContinuumCoulomb.AmplificationProgram.iterate_index_bits line 157
theorem OAI.ContinuumCoulomb.AmplificationProgram.iterate_measure line 167
theorem OAI.ContinuumCoulomb.AmplificationProgram.iterate_code_bound line 182
Source documentation
The entire arithmetic state stays polynomial in iteration count and initial binary input size, including arbitrary initial register contents.
```
theorem iterate_code_bound (n : ℕ) (s : State) (i : ℕ) (hi : i ≤ n) :
    (stateCode ((step^[i]) s)).length ≤
      (16 * (Polynomial.X + 1) ^ 2 + 16 : Polynomial ℕ).eval (n + (stateCode s).length) := by
…
```
Mentions: OAI.ContinuumCoulomb.AmplificationProgram.State, OAI.ContinuumCoulomb.AmplificationProgram.stateCode, OAI.ContinuumCoulomb.AmplificationProgram.step
def OAI.ContinuumCoulomb.AmplificationProgram.stepProgram line 194
def OAI.ContinuumCoulomb.AmplificationProgram.repeatProgram line 209
def OAI.ContinuumCoulomb.AmplificationProgram.orderProgram line 213
def OAI.ContinuumCoulomb.AmplificationProgram.startProgram line 224
def OAI.ContinuumCoulomb.AmplificationProgram.resultProgram line 230
def OAI.ContinuumCoulomb.AmplificationProgram.rawProgram line 242
Source documentation
Every step is compiled from actual binary add/multiply/divide routines; the repetition count is polynomial in the unary input size.
```
noncomputable def rawProgram : Procedure unaryCode Nat.bits taylorAmplification :=
…
```
Mentions: OAI.ContinuumCoulomb.taylorAmplification
theorem OAI.ContinuumCoulomb.AmplificationProgram.encodeUnary_replicate line 245
theorem OAI.ContinuumCoulomb.AmplificationProgram.encodeDigits_quote line 251
def OAI.ContinuumCoulomb.AmplificationProgram.inputProgram line 257
Source documentation
Strip the false unary terminator with two actual reversals and one pop.
```
noncomputable def inputProgram : Procedure BinaryEncoding.unary.encode unaryCode id := by
…
```
def OAI.ContinuumCoulomb.AmplificationProgram.certificate line 268
Source documentation
Exact amplification with explicit prefix encodings and a finite polynomial-time machine.
```
noncomputable def certificate :
    Turing.TM2ComputableInPolyTime BinaryEncoding.unary.encode BinaryEncoding.natural.encode
      taylorAmplification := by
…
```
Mentions: OAI.ContinuumCoulomb.taylorAmplification