CoarseGridArithmetic.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact arithmetic on a shared coarse-array denominator. Addition touches only the signed numerators and keeps the denominator, preventing denominator growth across the child-array sums. All counters run Boolean primitives.

theorem OAI.EditApproximation.BinaryFraction.coarseGridNatWithWork_value line 19
Source documentation
Store an integer on the common denominator by a literal bit product.
```
 theorem coarseGridNatWithWork_value (denominator : List Bool)
    (hden : 0 < bitWordValue denominator) (n : ℕ) :
    (coarseGridNatWithWork denominator hden n).1.value = n := by
…
```
Mentions: OAI.EditApproximation.bitWordValue, OAI.EditApproximation.BinaryFraction.coarseGridNatWithWork, OAI.EditApproximation.BinaryFraction.value
theorem OAI.EditApproximation.BinaryFraction.coarseGridNatWithWork_den line 30
theorem OAI.EditApproximation.BinaryFraction.coarseGridNatWithWork_cost line 39
theorem OAI.EditApproximation.BinaryFraction.coarseGridAddWithWork_value line 63
Source documentation
Add two stored cells after their denominators have been made identical.
```
 theorem coarseGridAddWithWork_value (a b : BinaryFraction)
    (hden : bitWordValue a.denominator = bitWordValue b.denominator) :
    (coarseGridAddWithWork a b).1.value = a.value + b.value := by
…
```
Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.bitWordValue, OAI.EditApproximation.BinaryFraction.coarseGridAddWithWork, OAI.EditApproximation.BinaryFraction.value
theorem OAI.EditApproximation.BinaryFraction.coarseGridAddWithWork_den line 72
theorem OAI.EditApproximation.BinaryFraction.coarseGridAddWithWork_cost line 79
theorem OAI.EditApproximation.BinaryFraction.coarseGridAddWithWork_width line 96