phi_sq_lt_2_7
φ² < 2.7 supplies the upper half of the interval 2.5 < φ² < 2.7 required by the constants predictions certificate. Researchers verifying the full set of bounds on α, c, and the Boltzmann analog k_R cite it to close the phi component. The argument reduces the target to the quadratic identity φ² = φ + 1, invokes the numerical bound φ < 1.62, and finishes with nlinarith.
claim$φ^2 < 2.7$, where $φ$ is the positive root of $x^2 - x - 1 = 0$.
background
The module ConstantsPredictionsProved supplies explicit numerical bounds for the constants listed in the COMPLETE_PROBLEM_REGISTRY. This theorem completes the phi-squared interval recorded in the certificate section, which also lists the identities 1/φ = φ - 1 and φ + 1/φ = √5. The identity φ² = φ + 1 is taken from the lemma whose doc-comment states it follows from the defining equation x² - x - 1 = 0. The auxiliary bound φ < 1.62 is supplied by the lemma proved by showing √5 < 2.24 and simplifying. These calculations sit inside the calculated proofs for registry items C-001, C-005, and C-006, all obtained via norm_num and nlinarith on explicit real bounds.
proof idea
The term proof first rewrites the left-hand side with the equality from phi_sq_eq. It then brings in the inequality from phi_lt_onePointSixTwo. The tactic nlinarith dispatches the resulting arithmetic comparison.
why it matters in Recognition Science
The result is collected inside constants_predictions_cert_exists, which constructs an explicit witness for the ConstantsPredictionsCert by listing every proved bound including this one. It thereby discharges the phi-squared portion of the calculated predictions for the registry items. In the framework it provides the concrete numerical control on the self-similar fixed point that precedes the eight-tick octave and the emergence of three spatial dimensions.
scope and limits
- Does not derive φ from the forcing chain or Recognition Composition Law.
- Does not bound the fine-structure constant α or the gravitational constant G.
- Does not connect the bound to the mass formula or Berry creation threshold.
- Does not claim the numerical bound 2.7 is sharp.
formal statement (Lean)
199theorem phi_sq_lt_2_7 : phi^2 < (2.7 : ℝ) := by
proof body
Term-mode proof.
200 have h1 : phi^2 = phi + 1 := phi_sq_eq
201 rw [h1]
202 have h2 : phi < 1.62 := phi_lt_onePointSixTwo
203 nlinarith
204
205/-! ## Section: Certificate -/
206
207/-- **CERTIFICATE**: Constants predictions with calculated bounds.
208
209 **C-001**: 0 < α < 0.01
210 **C-005**: c = 1, c > 0
211 **C-006**: 0 < k_R < 0.5 (k_R = ln(φ))
212 **Phi formulas**: 1/φ = φ-1, φ+1/φ = √5
213 **Phi bounds**: 2.5 < φ² < 2.7
214
215 **All from φ with rigorous bounds.** -/