BitAllocation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Fresh Boolean-list cells allocated by the literal arithmetic routines. Input tails are shared. Counts include discarded intermediate lists, so they also bound the cells simultaneously live during evaluation.

theorem OAI.EditApproximation.bitAddAllocation_le_work line 18
theorem OAI.EditApproximation.bitSubtractAllocation_le_work line 44
theorem OAI.EditApproximation.bitMulAllocation_le_work line 68
theorem OAI.EditApproximation.trimBitWordAllocation_le_work line 79
theorem OAI.EditApproximation.bitDivModAllocation_le_work line 91
Source documentation
Each division step allocates one candidate cell and one quotient cell, plus the fresh subtraction result exactly when subtraction is executed.
```
theorem bitDivModAllocation_le_work (divisor bits : List Bool) :
    bitDivModAllocation divisor bits ≤ (bitDivModWithWork divisor bits).2.2 := by
…
```
Mentions: OAI.EditApproximation.bitDivModAllocation, OAI.EditApproximation.bitDivModWithWork
theorem OAI.EditApproximation.bitCompare_recursion_le_work line 103
Source documentation
Comparison allocates no Boolean-list cells. The recursive frames have height at most the explicitly charged work counter.
```
theorem bitCompare_recursion_le_work (left right : List Bool) :
    max left.length right.length + 1 ≤ (bitCompareWithWork left right).2 := by
…
```
Mentions: OAI.EditApproximation.bitCompareWithWork