BandGuards.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Literal band endpoint geometry and rounding guards

The full child endpoint diameter follows from the computed internal cuts and zero connection, including the two outside endpoints.

theorem OAI.EditApproximation.connectionBudget_zero_head line 16
theorem OAI.EditApproximation.connectionBudget_zero_right line 29
Source documentation
Each actual right endpoint is the next actual left endpoint, or the parent's end when this is the last child.
```
theorem connectionBudget_zero_right {n : ℕ} (states : List (TargetInterval n))
    (start finish : ℕ) (hzero : connectionBudget start states finish = 0)
    (i : ℕ) (hi : i < states.length) :
    states[i].hi = connectionPrefixBoundary states finish (i + 1) := by
…
```
Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.connectionBudget, OAI.EditApproximation.connectionPrefixBoundary
theorem OAI.EditApproximation.zero_connection_left_endpoint line 53
theorem OAI.EditApproximation.zero_connection_right_endpoint line 64

theorem OAI.EditApproximation.computedBand_child_endpoint_diameter line 75

Source documentation

Full endpoint distance, including first/last endpoints, for every two members of the literal computed band.

theorem computedBand_child_endpoint_diameter {nx ny M : ℕ} (parent : TargetInterval nx)
    (r : TargetInterval ny) (b P : ℕ) (tau theta velocity : ℚ) (htau : 0 < tau) (htheta : 0 ≤ theta)
    (child : Fin M → TargetInterval ny → ℚ)
    (states states' : Fin M → TargetInterval ny)
    (hstates : states ∈ computedBandActions parent r b P tau theta velocity child)
    (hstates' : states' ∈ computedBandActions parent r b P tau theta velocity child)
    (i : Fin M) :
    (targetEndpointDistance (states i) (states' i) : ℝ) ≤ 4 * (theta : ℝ) * b / M := by
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.computedBandActions, OAI.EditApproximation.targetEndpointDistance

theorem OAI.EditApproximation.gridStateBox_on_grid line 115
Source documentation
Grid soundness of the literal local box enumeration.
```
theorem gridStateBox_on_grid {n g radius lo hi : ℕ} (hg : 0 < g)
    (state : TargetInterval n) (hstate : state ∈ gridStateBox n g radius lo hi) :
    g ∣ state.lo ∧ g ∣ state.hi := by
…
```
Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.gridStateBox
theorem OAI.EditApproximation.wideActionList_on_grid line 125