module module high

`IndisputableMonolith.Numerics.Interval.PhiBounds`

The PhiBounds module supplies machine-verified rational-endpoint bounds on sqrt(5) and the golden ratio phi. Mass-prediction and observability modules cite these intervals to anchor phi-ladder calculations and alpha_G scores inside intervals that contain measured values. Each bound is obtained by direct interval evaluation imported from Basic together with Mathlib facts on the golden ratio.

claim$2.236^2 < 5 < 2.2367^2$, $2.236 < 5^{1/2} < 2.2367$, and $1.618 < (1 + 5^{1/2})/2 < 1.6185$ (with analogous bounds at six and eight decimal places).

background

The module sits in the Numerics domain and imports Verified Interval Arithmetic from Basic, whose core technique is to enclose real numbers between rational endpoints that Lean can compute exactly. It further imports Mathlib's definition of the golden ratio and real-power functions. These bounds supply the numerical constants required by the phi-ladder mass formula and the Recognition Composition Law evaluations that appear in downstream mass and astrophysics modules.

proof idea

The module is a collection of independent theorems, each proving one concrete inequality (sq_2236_lt_5, phi_gt_1618, etc.) by interval arithmetic or norm_num on rationals. No overarching tactic script unites them; each sibling is a self-contained bound.

why it matters in Recognition Science

The bounds are imported by NumericalPredictions to certify that every RS mass prediction lies inside an interval containing the PDG value, by AlphaGScoreCard for the gravitational coupling constant, by ElectroweakMasses for Z-boson and W-boson rungs, and by ObservabilityLimits for recognition-length constraints. They close the numerical-verification step that links the T5 J-uniqueness and T6 phi fixed-point landmarks to concrete mass numbers.

scope and limits

Does not derive phi from the functional equation or RCL; imports the Mathlib definition.
Does not supply bounds on pi, e, or other constants.
Does not apply the intervals to physical derivations; only supplies the numeric facts.
Does not claim the listed decimal precisions are optimal; they are the ones proved.

used by (13)

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

IndisputableMonolith.Astrophysics.ObservabilityLimits module_import
IndisputableMonolith.Masses.AlphaGScoreCard module_import
IndisputableMonolith.Masses.ElectroweakMasses module_import
IndisputableMonolith.Masses.NumericalPredictions 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.RRF.Physics.QuarkMasses module_import
IndisputableMonolith.StandardModel.NeutrinoMassHierarchy 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