fourPiInterval
plain-language theorem explainer
This definition constructs the closed rational interval with endpoints 12.56 and 12.6. Numerics routines inside the Recognition framework cite it when they need a machine-checked enclosure for 4π that avoids floating-point issues. The construction is a direct structure definition whose sole non-trivial content is a norm_num check that the lower endpoint does not exceed the upper endpoint.
Claim. Let $I$ be the closed interval with rational endpoints $lo = 1256/100$ and $hi = 126/10$ satisfying $lo ≤ hi$.
background
The module supplies rigorous interval bounds on π and its multiples by importing Mathlib's proven inequalities such as 3.14 < π < 3.15. An Interval is the structure with fields lo : ℚ, hi : ℚ and valid : lo ≤ hi. The local setting is the construction of concrete, decidable enclosures for constants that appear in later numerical checks within Recognition Science.
proof idea
The definition directly populates the lo and hi fields with the given rationals. The valid field is discharged by a single norm_num tactic that reduces the inequality 1256/100 ≤ 126/10 to a decidable statement on integers.
why it matters
The interval is the explicit container referenced by the downstream theorem four_pi_in_interval, which certifies containment of 4π. It supplies one link in the chain of machine-checked bounds on π that support numerical verification steps throughout the framework, especially where constants derived from the phi-ladder require explicit rational enclosures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.