pi_in_piIntervalWide
plain-language theorem explainer
π satisfies 3.14 ≤ π ≤ 3.15. Workers on numerical verification or interval arithmetic inside Recognition Science would cite this for establishing basic constant bounds. The proof reduces the claim to Mathlib's pi_gt_d2 and pi_lt_d2 via rational normalization and the contains definition.
Claim. $314/100 ≤ π ≤ 315/100$, where containment of a real $x$ in an interval $I$ means $I.lo ≤ x ≤ I.hi$.
background
The module supplies rigorous interval bounds for π by importing Mathlib's proven inequalities such as Real.pi_gt_d2 (3.14 < π) and Real.pi_lt_d2 (π < 3.15). The contains predicate states that a real x lies in interval I precisely when I.lo ≤ x ≤ I.hi. The specific interval piIntervalWide is the closed interval with lo = 314/100 and hi = 315/100, whose validity is discharged by norm_num.
proof idea
The tactic proof first applies simp to unfold contains and piIntervalWide into a conjunction. Constructor splits the two inequalities. The lower bound normalizes 314/100 to 3.14 and invokes Real.pi_gt_d2; the upper bound invokes Real.pi_lt_d2 and normalizes the resulting 3.15 back to 315/100.
why it matters
This theorem supplies a basic numerical bound on π inside the Numerics.Interval.PiBounds module and supports sibling constructions such as fourPiInterval and piSqInterval. It provides concrete bounds usable for constants appearing in RS-native units (c=1, ħ=φ^{-5}) or the alpha band, while remaining independent of the J-cost function, phi-ladder, and the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.