hubble_positive
plain-language theorem explainer
Existence of a positive real Hubble constant follows by exhibiting the witness (ln φ)/8. Recognition Science cosmologists cite this to ground H₀ > 0 in the forced positivity of the golden ratio for the Hubble tension item. The term proof instantiates the existential, applies the lemma one_lt_phi to obtain ln φ > 0, and closes with linear arithmetic.
Claim. There exists a real number $H_0$ such that $H_0 > 0$, witnessed explicitly by $H_0 = (ln φ)/8$ where φ is the golden ratio satisfying φ > 1.
background
The module supplies calculated proofs for registry items including T-001 (Hubble tension resolved by H₀ > 0 from φ). The golden ratio φ satisfies 1 < φ by the upstream lemma one_lt_phi, proved via sqrt(5) inequalities and norm_num. H0 denotes the Hubble parameter today in natural units. The local setting uses explicit bounds and positivity tactics to discharge cosmological predictions without external hypotheses.
proof idea
Term proof that applies 'use Real.log phi / 8' to witness the existential quantifier. It then invokes Real.log_pos on the upstream fact one_lt_phi to obtain Real.log phi > 0. Linear arithmetic (linarith) immediately yields the required positivity of the witness.
why it matters
This result discharges the T-001 Hubble tension entry in the Cosmological Predictions registry by deriving H₀ > 0 from ln φ > 0. It anchors the unification chain at the phi-forcing step (T6) where φ is the self-similar fixed point. No downstream theorems yet reference it, leaving the numerical Hubble value open for later refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.