pith. machine review for the scientific record. sign in
theorem proved term proof

three_strategies_agree

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 101theorem three_strategies_agree : H_ThreeStrategiesAgree := by

proof body

Term-mode proof.

 102  unfold H_ThreeStrategiesAgree
 103  refine ⟨?_, ?_, ?_⟩
 104  · -- StellarAssembly = NucleosynthesisTiers
 105    -- Both are Constants.phi
 106    rw [StellarAssembly.ml_stellar_value, NucleosynthesisTiers.ml_nucleosynthesis_eq_phi]
 107    simp only [StellarAssembly.φ, NucleosynthesisTiers.φ]
 108  · -- NucleosynthesisTiers = ObservabilityLimits
 109    rw [NucleosynthesisTiers.ml_nucleosynthesis_eq_phi, ObservabilityLimits.ml_geometric_is_phi]
 110    simp only [NucleosynthesisTiers.φ, ObservabilityLimits.φ]
 111  · -- ObservabilityLimits = ml_derived
 112    rw [ObservabilityLimits.ml_geometric_is_phi, ml_derived_value]
 113    simp only [ObservabilityLimits.φ, φ]
 114
 115/-- **THEOREM (RIGOROUS)**: φ is in the observed range [0.5, 5] solar units.
 116
 117    This proves the range property for the φ value itself. Once `ml_derived_value`
 118    is proven (showing ml_derived = φ), this immediately gives `ml_in_observed_range`. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (14)

Lean names referenced from this declaration's body.