191theorem ml_from_geometry_only : 192 ∃ (ml : ℝ), 193 ml = φ ∧ 194 1 < ml ∧ ml < 5 ∧ 195 ml = StellarAssembly.ml_stellar ∧ 196 ml = NucleosynthesisTiers.ml_nucleosynthesis := by
proof body
Term-mode proof.
197 use ml_geometric 198 refine ⟨rfl, ?_, ?_, agrees_with_stellar_assembly, agrees_with_nucleosynthesis⟩ 199 · exact ml_geometric_bounds.1 200 · linarith [ml_geometric_bounds.2] 201 202/-! ## Zero-Parameter Status -/ 203 204/-- **Certificate**: M/L is derived with zero external parameters. 205 206The derivation uses only: 2071. The Meta-Principle (MP) → ledger structure 2082. The cost functional J(x) = ½(x + 1/x) - 1 from T5 2093. The eight-tick structure from T6 2104. The recognition length l_rec from the Planck identity 211 212All of these are derived from MP. Therefore M/L is derived. -/
depends on (30)
Lean names referenced from this declaration's body.