four_pi_lt_d6
The inequality 4π < 12.566372 follows from Mathlib's established bound π < 3.141593 via linear arithmetic. Numerics code in the Recognition framework cites it when tightening interval enclosures for multiples of π in spacetime or forcing calculations. The proof is a one-line wrapper that invokes Real.pi_lt_d6 and closes with linarith.
claim$4π < 12.566372$
background
The module supplies rigorous interval bounds on π drawn from Mathlib's proven constants, including Real.pi_lt_d6 which states π < 3.141593. These bounds are assembled into interval objects such as fourPiInterval for use in numerical verification inside the Recognition framework. The upstream structure for records meta-realization axioms required by self-reference, while the interval definition computes the spacetime interval as the sum of η-weighted squared displacements over four dimensions.
proof idea
The proof applies the lemma Real.pi_lt_d6 to obtain π < 3.141593, then invokes linarith to scale the inequality by 4 and reach the target bound.
why it matters in Recognition Science
This result feeds the parent theorem four_pi_in_interval_tight, which places 4π inside a tight interval object. It supplies the numerical infrastructure needed for Recognition Science constants that involve π, such as the alpha inverse band and the eight-tick octave, without introducing new hypotheses.
scope and limits
- Does not prove any bound tighter than the Mathlib source.
- Does not apply the inequality outside the real numbers.
- Does not derive any Recognition-specific constants such as phi or G.
formal statement (Lean)
194theorem four_pi_lt_d6 : 4 * pi < (12.566372 : ℝ) := by
proof body
Term-mode proof.
195 have h := Real.pi_lt_d6 -- π < 3.141593
196 linarith
197
198/-- Tight interval for 4π -/