AdaptiveMeshBreakpoints.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Literal three-way breakpoint factorization. All sets below are the actual endpoint/threshold sets from AdaptiveMeshCounting. In particular an equality at a truncation threshold keeps the original half-open label.

theorem OAI.QuantitativeVanDerWaerden.continuous_rho line 14
theorem OAI.QuantitativeVanDerWaerden.no_breakpoint_of_same_signs line 21
Source documentation
Equal ternary signs exclude every closed-interval breakpoint when the two evaluation points are distinct. Equality signs are essential here.
```
theorem no_breakpoint_of_same_signs {B : Finset ℝ} {x y : ℝ} (hxy : x < y)
    (hs : ∀ b ∈ B, ternarySign (x - b) = ternarySign (y - b)) :
    ∀ b ∈ B, ¬ (x ≤ b ∧ b ≤ y) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ternarySign
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.meshLabel_eq_of_no_endpoint line 38
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.endpoints_determine_label line 52
def OAI.QuantitativeVanDerWaerden.AdaptiveMesh.truncatedLabel line 71
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.truncatedLabel_eq_none_iff line 75
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.truncatedLabel_add_int line 80
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.mem_thresholdPoints_of_rho_eq line 85
theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.truncatedBreakpoints_determine_label line 101

theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.stationary_breakpoint_factorization line 159

Source documentation

A fixed 49-point breakpoint set for the closed neighborhood of an anchor cell. It is chosen before either free affine parameter is selected.

theorem stationary_breakpoint_factorization (i : A.Label) (z : ℤ) :
    ∃ B : Finset ℝ, B.card ≤ 49 ∧
      ∀ x y : ℝ,
        A.left i + z - A.width i ≤ x ∧ x ≤ A.right i + z + A.width i →
        A.left i + z - A.width i ≤ y ∧ y ≤ A.right i + z + A.width i →
        (∀ b ∈ B, ternarySign (x - b) = ternarySign (y - b)) →
        A.meshLabel x = A.meshLabel y := by
…

Mentions: OAI.QuantitativeVanDerWaerden.ternarySign

theorem OAI.QuantitativeVanDerWaerden.AdaptiveMesh.rotating_breakpoint_factorization line 172

Source documentation

The rotating-coordinate bound is uniform in the location of the target interval, including intervals crossing the circle cut.

theorem rotating_breakpoint_factorization (D : ℕ) (hD : 0 < D) (u v : ℝ)
    (huv : u ≤ v) (hlen : v - u ≤ 4 * A.H) :
    ∃ B : Finset ℝ, B.card ≤ 16004 * D ∧
      ∀ x y : ℝ, u ≤ x ∧ x ≤ v → u ≤ y ∧ y ≤ v →
        (∀ b ∈ B, ternarySign (x - b) = ternarySign (y - b)) →
        A.truncatedLabel (1 / (1000 * (D : ℝ))) x =
          A.truncatedLabel (1 / (1000 * (D : ℝ))) y := by
…

Mentions: OAI.QuantitativeVanDerWaerden.ternarySign