PhysicalPreparedInputBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.EditApproximation.BinaryFraction.PreparedKernelNumericBounds line 10
Source documentation
Numeric register and loop bounds, independent of previously cached values.
```
structure PreparedKernelNumericBounds {nx ny M : ℕ}
    (N P F exponent H Q eM eF B E S t : ℕ)
    (tau a eta kappa delta : BinaryFraction)
    (integer : ℕ → TargetInterval ny → ℕ) : Prop where
…
```
Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.TargetInterval
theorem OAI.EditApproximation.BinaryFraction.PreparedKernelNumericBounds.with_cached_values line 45

theorem OAI.EditApproximation.physicalPreparedStep_inputBounds line 107

Source documentation

The actual all-seed physical invariants discharge the value premises of the prepared evaluator; only representation and scalar register bounds remain.

theorem physicalPreparedStep_inputBounds {α : Type*} [DecidableEq α]
    {M J R : ℕ} [NeZero R] (source target : List α)
    (N P F exponent H Q eM eF B E S : ℕ)
    (tauWord aWord etaWord kappaWord deltaWord : BinaryFraction)
    (parentWords : TargetInterval target.length → BinaryFraction)
    (massWords initialWords : Fin M → TargetInterval target.length → BinaryFraction)
    (historyWords : ℕ → Fin M × TargetInterval target.length → BinaryFraction)
    (draw : PhysicalInternalNode M J → ℕ → CellGroupDraws M F Q)
    (integer : PhysicalInternalNode M J → Fin R → ℕ → TargetInterval target.length → ℕ)
    (node : PhysicalNode M J) (hbelow : node.1.val < J) (t : ℕ)
    (U : PhysicalEntry M J target.length → ℕ) (A tau eta kappa delta : ℚ) (T : ℕ)
    (hd : 0 ≤ delta)
…

Mentions: OAI.EditApproximation.BinaryFraction, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.PhysicalInternalNode, OAI.EditApproximation.CellGroupDraws, OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.PhysicalEntry