IntegerBinarySpace.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.EditApproximation.integerFinalAllocation line 16
Source documentation
Final conversion allocates only its division and clamping workspace.
```
def integerFinalAllocation (source target : List ℤ) (N : ℕ)
    (input : ComputedFamilyInput (source.map integerSymbolCode) (target.map integerSymbolCode) N) : ℕ :=
…
```
Mentions: OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.integerSymbolCode
theorem OAI.EditApproximation.integerFinalAllocation_le_work line 24
def OAI.EditApproximation.integerAcceptedSpaceTerms line 37
Source documentation
Scans and word-RAM preprocessing reserve eight scalar/control cells per charged step. Retained input/index cells are counted separately. Numerical setup, local programs and coarse initialization use their explicit allocation counters. Streaming samplers reuse a bounded buffer, without storing failed trial counts or failed words.
```
noncomputable def integerAcceptedSpaceTerms (source target : List ℤ) (N : ℕ)
    (epsilon : BinaryFraction)
    (input : ComputedFamilyInput (source.map integerSymbolCode) (target.map integerSymbolCode) N) : List ℕ :=
…
```
Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.ComputedFamilyInput, OAI.EditApproximation.integerSymbolCode
def OAI.EditApproximation.integerBinarySpace line 59
Source documentation
The space bound applies to all outcomes, including null-probability outcomes. The exact branch uses the concrete suffix-DP allocation counter.
```
noncomputable def integerBinarySpace (source target : List ℤ) (N : ℕ) (epsilon : BinaryFraction)
    (outcome : ComputedFullOutcome (source.map integerSymbolCode) (target.map integerSymbolCode) N) : ℕ :=
…
```
Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.ComputedFullOutcome, OAI.EditApproximation.integerSymbolCode
theorem OAI.EditApproximation.sum_cells_le line 72
theorem OAI.EditApproximation.embed_space_power line 82
theorem OAI.EditApproximation.bounded_space_sum line 85
theorem OAI.EditApproximation.integerBinarySpace_polynomial line 95