phi_sq_lt_2_7
plain-language theorem explainer
φ² < 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.