cosmological_predictions_cert_exists
plain-language theorem explainer
The theorem establishes existence of a certificate bundling explicit inequalities for the spectral index n_s = 1 - 2/φ³ (0.5 < n_s < 1), positivity of H₀ via ln(φ)/8, and numerical intervals 2.59 < φ² < 2.62, 6.7 < φ⁴ < 6.9, 10.7 < φ⁵ < 11.3. Researchers citing Recognition Science cosmological predictions would reference this result to confirm that the φ-derived bounds satisfy the registry items EU-003 and T-001. The proof is a direct construction that invokes one_lt_phi to obtain log positivity, then assembles the certificate fields from pre-b
Claim. There exists a structure containing the inequalities $0.5 < 1 - 2/φ^3 < 1$, $ (log φ)/8 > 0 $, $2.59 < φ^2 < 2.62$, $6.7 < φ^4 < 6.9$, and $10.7 < φ^5 < 11.3$.
background
The module supplies calculated proofs for cosmological predictions drawn from the COMPLETE_PROBLEM_REGISTRY. It covers EU-003 (primordial spectral index bounds from φ³), T-001 (Hubble positivity from ln(φ)), and related φ-power intervals, all obtained from the interval 1.61 < φ < 1.62 together with the relation φ² = φ + 1. The certificate is the structure CosmologicalPredictionsCert whose nine fields record these inequalities directly. Upstream lemmas supply the necessary positivity and interval facts: one_lt_phi proves 1 < φ via sqrt comparisons, while phi_squared_bounds, phi_fourth_bounds and phi_fifth_bounds each rewrite the power via the minimal polynomial and apply linarith on the φ interval.
proof idea
The tactic proof first obtains Real.log phi > 0 by applying Real.log_pos to one_lt_phi, then uses positivity to conclude log phi / 8 > 0. It next builds the certificate by supplying the two spectral-index inequalities (taken from sibling theorems spectral_index_gt_half and spectral_index_lt_one), the freshly proved Hubble positivity, and the three pairs of power bounds from phi_squared_bounds, phi_fourth_bounds and phi_fifth_bounds. The final trivial witness completes the existential quantifier.
why it matters
This existence theorem certifies that the calculated bounds for EU-003 and T-001 are simultaneously satisfiable inside the Recognition Science framework. It closes the CosmologicalPredictionsProved module by exhibiting a single object that collects all the φ-derived numerical constraints required by the unification pipeline. The result sits downstream of the phi-forcing chain (T5–T6) that forces φ as the self-similar fixed point and supplies the numerical interval used throughout the power-bound lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.