Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Rational cut normals preserve protected cubes after scaling

Lax263307.RationalCutBuffer · concepts/Lax263307/RationalCutBuffer.lean · lax-263307

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Clear all rational normal coefficients by one positive product of denominators. The resulting integer normal defines the same central half-space. Its bit size is bounded by the numerator bit size plus the sum of denominator bit sizes. A positive query gap, together with a bound on the sum of absolute coefficients, protects a whole coordinate cube about every valid point. Scaling coordinates by 4N and clearing denominators preserve that protected central cut.

    Concept map
    2 concepts; 4 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 8 statements. Each proof establishes one of them relative to its assumptions.

    1 central_buffer proven

    2 denominator_bound proven

    3 denominator_positive proven

    4 dot_stable proven

    5 integer_normal_cast proven

    6 normal_nonzero proven

    7 normal_size proven

    8 scaled_cleared_cut proven

    Lean source view on GitHub

    1import Lax263307.BufferedEllipsoid
    2import Mathlib.Data.Nat.Size
    3
    4/-!
    5---
    6title: Rational cut normals preserve protected cubes after scaling
    7type: theorem
    8---
    9Clear all rational normal coefficients by one positive product of denominators.
    10The resulting integer normal defines the same central half-space. Its bit size
    11is bounded by the numerator bit size plus the sum of denominator bit sizes.
    12A positive query gap, together with a bound on the sum of absolute coefficients,
    13protects a whole coordinate cube about every valid point. Scaling coordinates
    14by 4N and clearing denominators preserve that protected central cut.
    15
    16# Formalization notes
    17
    18Both clearing operations are computable. Only the correctness argument uses
    19real casts. The scaled-cube guarantee supplies the cut hypothesis for the
    20actual rounded ellipsoid loop; it does not assume that the exact hull has
    21interior. The numerator calculation matches the registered LP size-bound
    22construction and is proved directly from divisibility of the denominator
    23product.
    24-/
    25
    26namespace Lax263307.RationalCutBuffer
    27
    28open Matrix
    29
    30def denominator {n : ℕ} (a : Fin n → ℚ) : ℕ := ∏ i, (a i).den
    31
    32def integerNormal {n : ℕ} (a : Fin n → ℚ) (i : Fin n) : ℤ :=
    33 (a i).num * (denominator a / (a i).den : ℕ)
    34
    35axiom denominator_positive {n : ℕ} (a : Fin n → ℚ) : 0 < denominator a
    36
    37axiom integer_normal_cast {n : ℕ} (a : Fin n → ℚ) (i : Fin n) :
    38 (integerNormal a i : ℝ) = (denominator a : ℝ) * (a i : ℝ)
    39
    40axiom normal_nonzero {n : ℕ} (a : Fin n → ℚ) (x z : Fin n → ℝ)
    41 (gap : (fun i => (a i : ℝ)) ⬝ᵥ z < (fun i => (a i : ℝ)) ⬝ᵥ x) :
    42 ∃ i, integerNormal a i ≠ 0
    43
    44axiom denominator_bound {n : ℕ} (a : Fin n → ℚ) :
    45 denominator a ≤ 2 ^ (∑ i, Nat.size (a i).den)
    46
    47axiom normal_size {n : ℕ} (a : Fin n → ℚ) (i : Fin n) :
    48 Nat.size (integerNormal a i).natAbs ≤
    49 Nat.size (a i).num.natAbs + ∑ j, Nat.size (a j).den
    50
    51axiom dot_stable {n : ℕ} (a x y : Fin n → ℝ) (ρ L : ℝ)
    52 (nonnegative : 0 ≤ ρ) (norm : (∑ i, |a i|) ≤ L)
    53 (near : ∀ i, |x i - y i| ≤ ρ) : |a ⬝ᵥ x - a ⬝ᵥ y| ≤ L * ρ
    54
    55axiom central_buffer {n : ℕ} (a x z perturbed : Fin n → ℝ) (α Δ ρ L : ℝ)
    56 (nonnegative : 0 ≤ ρ) (norm : (∑ i, |a i|) ≤ L)
    57 (valid : a ⬝ᵥ z ≤ α) (gap : α + Δ ≤ a ⬝ᵥ x)
    58 (small : L * ρ ≤ Δ / 2) (near : ∀ i, |perturbed i - z i| ≤ ρ) :
    59 a ⬝ᵥ perturbed ≤ a ⬝ᵥ x - Δ / 2
    60
    61axiom scaled_cleared_cut {n : ℕ} (positive : 0 < n) (a : Fin n → ℚ)
    62 (query z : Fin n → ℝ) (α Δ ρ L : ℝ)
    63 (nonnegative : 0 ≤ ρ) (norm : (∑ i, |(a i : ℝ)|) ≤ L)
    64 (valid : (fun i => (a i : ℝ)) ⬝ᵥ z ≤ α)
    65 (gap : α + Δ ≤ (fun i => (a i : ℝ)) ⬝ᵥ (fun i => 4 * (n : ℝ) * query i))
    66 (small : L * ρ ≤ Δ / 2) (e : Fin n → ℝ)
    67 (near : ∀ i, |e i| ≤ ρ / (4 * n)) :
    68 (fun i => (integerNormal a i : ℝ)) ⬝ᵥ
    69 (Lax263307.BufferedEllipsoid.scale z + e - query) ≤ 0
    70
    71end Lax263307.RationalCutBuffer
    72
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Formalization notes

    Both clearing operations are computable. Only the correctness argument uses real casts. The scaled-cube guarantee supplies the cut hypothesis for the actual rounded ellipsoid loop; it does not assume that the exact hull has interior. The numerator calculation matches the registered LP size-bound construction and is proved directly from divisibility of the denominator product.

    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…