module module high

`IndisputableMonolith.Numerics.Interval.PhiBounds`

Certified rational endpoint bounds on √5 and on the golden ratio φ = (1+√5)/2. Mass, CKM, neutrino, and interval log/power modules import these inequalities whenever φ-ladder arithmetic must stay inside Lean’s exact rational kernel. Proofs are elementary square comparisons of rationals against 5, then linear transport to φ.

claimStrict rational bounds $a^2 < 5 < b^2$ for explicit positive rationals $a,b$ (e.g. $2.236^2 < 5 < 2.237^2$ and multi-digit refinements), hence $a < \sqrt{5} < b$, and the induced bounds on the golden ratio $\varphi = (1+\sqrt{5})/2$ such as $1.618 < \varphi < 1.6185$ and tighter digit strings.

background

Recognition Science forces φ as the unique self-similar fixed point (forcing step T6). Downstream formulas (mass ladder, electroweak rungs, CKM geometry, observability cutoffs) therefore need concrete numerical control of φ and of √5 without floating-point gaps.

The parent numerics layer (Interval.Basic) supplies verified interval arithmetic whose endpoints are rationals Lean can decide exactly. This module specializes that pattern to the golden-ratio constants imported from Mathlib: compare squares of explicit rationals to the integer 5, obtain strict bounds on √5, then push them through the affine map $x \mapsto (1+x)/2$ to bound φ.

Sibling lemmas come in coarse and fine packs (four-digit and eight-digit style endpoints), so callers can pick the precision they need.

proof idea

Each bound is a short chain. First prove rational square inequalities such as $(2236/1000)^2 < 5$ and $5 < (2237/1000)^2$ by exact integer arithmetic on cleared denominators. Monotonicity of square root on positives yields $2236/1000 < \sqrt{5} < 2237/1000$. Adding 1 and dividing by 2 transports the same endpoints to φ. Tighter packs repeat the pattern with longer decimal rationals. No transcendental analysis is required beyond Mathlib’s √ and goldenRatio definitions.

why it matters in Recognition Science

φ appears in the RS-native constants ($\hbar = \varphi^{-5}$, $G = \varphi^5/\pi$) and in the mass formula yardstick · φ^(rung−8+gap(Z)). This module is the shared numerical substrate for those claims.

Importers include Masses.ElectroweakMasses (Z at rung 1, m_Z ~ φ^51), Masses.Verification (PDG comparison), Physics.CKMGeometry (T11 mixing angles), Physics.ElectronMass.Necessity, Physics.NeutrinoSector, and Astrophysics.ObservabilityLimits (recognition-length cutoffs). Interval modules Log and Pow also import it so exp/log/power enclosures can start from certified φ endpoints rather than ad-hoc floats.

Without these lemmas, every φ-ladder inequality would re-prove the same rational squares.

scope and limits

Does not derive φ from the forcing chain; only bounds Mathlib’s goldenRatio.
Does not prove uniqueness or self-similarity of φ (that is T5–T6).
Does not supply interval enclosures for arbitrary reals, only √5 and φ.
Does not claim decimal strings are optimal; only that the stated rationals work.
Does not connect bounds to experimental PDG values (Verification stays quarantined).

used by (12)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Astrophysics.ObservabilityLimits module_import
IndisputableMonolith.Masses.ElectroweakMasses module_import
IndisputableMonolith.Masses.Verification module_import
IndisputableMonolith.Numerics.Interval.Log module_import
IndisputableMonolith.Numerics.Interval.Pow module_import
IndisputableMonolith.Physics.CKMGeometry module_import
IndisputableMonolith.Physics.ElectronMass.Necessity module_import
IndisputableMonolith.Physics.NeutrinoSector module_import
IndisputableMonolith.Physics.QuarkMasses module_import
IndisputableMonolith.Physics.WBosonAbsoluteScoreCard module_import
IndisputableMonolith.StandardModel.NeutrinoMassHierarchy module_import
IndisputableMonolith.Verification.MassComparison module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Numerics.Interval.Basic module_import

declarations in this module (98)

theorem sq_2236_lt_5 L26
theorem five_lt_sq_2237 L29
theorem sqrt5_gt_2236 L32
theorem sqrt5_lt_2237 L37
theorem phi_gt_1618 L42
theorem phi_lt_16185 L48
theorem sq_22360679_lt_5 L56
theorem five_lt_sq_22360680 L59
theorem sqrt5_gt_22360679 L62
theorem sqrt5_lt_22360680 L67
theorem phi_gt_161803395 L72
theorem phi_lt_16180340 L78
theorem phi_tight_bounds L87
def phiIntervalTight L91
theorem phi_in_phiIntervalTight L97
def phi_quarter_lo L114
def phi_quarter_hi L117
lemma phi_quarter_lo_pow4_lt_phi_lo L119
lemma phi_hi_lt_phi_quarter_hi_pow4 L123
theorem phi_quarter_gt L128
theorem phi_quarter_lt L157
theorem phi_quarter_bounds L185
theorem phi_neg_quarter_bounds L189
theorem phi_sq_gt L216
theorem phi_sq_lt L221
theorem phi_neg2_gt L229
theorem phi_neg2_lt L242
theorem phi_inv_eq L256
theorem phi_inv_gt L262
theorem phi_inv_lt L267
def phi_inv_interval_proven L273
theorem phi_inv_in_interval_proven L278
theorem phi_cubed_eq L291
theorem phi_cubed_gt L299
theorem phi_cubed_lt L304
theorem phi_pow4_eq L310
theorem phi_pow4_gt L319
theorem phi_pow4_lt L324
theorem phi_pow5_eq L330
theorem phi_pow5_gt L339
theorem phi_pow5_lt L344
theorem phi_pow6_eq L350
theorem phi_pow7_eq L360
theorem phi_pow8_eq L370
theorem phi_pow8_gt L380
theorem phi_pow8_lt L385
def phi_pow8_interval_proven L391
theorem phi_pow8_in_interval_proven L396
theorem phi_inv2_gt L409
theorem phi_inv2_lt L414
theorem phi_inv3_gt L420
theorem phi_inv3_lt L427
def phi_inv3_interval_proven L434
theorem phi_inv3_in_interval_proven L439
theorem phi_inv3_zpow_bounds L456
theorem phi_inv5_gt L492
theorem phi_inv5_lt L501
def phi_inv5_interval_proven L511
theorem phi_inv5_in_interval_proven L516
theorem phi_pow16_eq L529
theorem phi_pow16_gt L538
theorem phi_pow16_lt L543
theorem phi_pow51_eq L549
theorem phi_pow51_gt L557
theorem phi_pow51_lt L562
def phi_pow51_interval_proven L567
theorem phi_pow51_in_interval_proven L572
theorem phi_pow54_eq L579
theorem phi_pow54_gt L583
theorem phi_pow54_lt L595
theorem phi_neg54_gt L609
theorem phi_neg54_lt L623
theorem phi_pow58_eq L638
theorem phi_pow58_gt L642
theorem phi_pow58_lt L654
theorem phi_neg58_gt L667
theorem phi_neg58_lt L680
lemma qhi_pos L702
lemma qlo_pos L705
theorem phi_neg2174_gt L709

… and 18 more