fourPiIntervalTight
plain-language theorem explainer
This definition supplies the narrow rational interval with endpoints 12.566368 and 12.566372 asserted to contain 4π. Numerics researchers building verified bounds inside the Recognition Science framework cite it when tighter control on multiples of π is required than the standard Mathlib d6 bounds. The body is a direct abbreviation whose sole non-trivial step is the norm_num tactic confirming the endpoint ordering.
Claim. The tight interval for $4π$ is the closed rational interval $I$ with lower endpoint $12566368/1000000$ and upper endpoint $12566372/1000000$.
background
The module Numerics.Interval.PiBounds assembles machine-checked interval bounds for π and its multiples by importing proven inequalities from Mathlib.Analysis.Real.Pi.Bounds. The underlying data structure is the Interval type from Numerics.Interval.Basic, a triple of rational lower bound, rational upper bound, and a proof that the lower bound does not exceed the upper bound. Upstream Mathlib lemmas such as Real.pi_gt_d6 supply 3.141592 < π < 3.141593, which scale directly to the corresponding bounds on 4π.
proof idea
The definition directly assigns the concrete rational values 12566368/1000000 and 12566372/1000000 to the lower and upper fields. The validity obligation is discharged by a single norm_num tactic that automatically verifies the inequality between these fixed rationals.
why it matters
This interval is the container referenced by the downstream theorem four_pi_in_interval_tight, which certifies that 4π lies inside it. The construction supports the module's goal of supplying exact rational bounds that compose with Recognition Science constants such as the fine-structure interval (137.030, 137.039). It aligns with the framework's requirement for machine-verified numerical claims that later enter mass-ladder or coupling calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.