def
definition
planetaryFormationCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Astrophysics.PlanetaryFormationFromJCost on GitHub at line 200.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
197 ∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
198 AgreesAtHalfRung r0 (r_orbit r0 k)
199
200def planetaryFormationCert : PlanetaryFormationCert where
201 r_orbit_pos := r_orbit_pos
202 r_orbit_zero := r_orbit_zero
203 r_orbit_adjacent_ratio := r_orbit_adjacent_ratio
204 r_orbit_strict_mono := r_orbit_strict_mono
205 r_orbit_closed_form := r_orbit_closed
206 r_orbit_adjacent_band := r_orbit_adjacent_ratio_band
207 r_orbit_gap_skip_band := r_orbit_gap_skip_band
208 ladder_agrees_at_half_rung := ladder_agrees_at_half_rung
209
210/-- **PLANETARY FORMATION ONE-STATEMENT.** Stable protoplanetary-disc
211orbital radii sit on the φ-ladder `r_orbit(k) = r₀ · φᵏ`. Adjacent
212rungs differ by exactly φ; gap-skip rungs (the asteroid-belt /
213Jupiter pattern) differ by φ². The ladder is its own half-rung
214witness: every prediction is inside its own falsifier band. -/
215theorem planetary_formation_one_statement :
216 (∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ, 0 < r_orbit r0 k) ∧
217 (∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
218 r_orbit r0 (k + 1) / r_orbit r0 k = phi) ∧
219 (∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
220 r_orbit r0 k < r_orbit r0 (k + 1)) ∧
221 (∀ r0 : ℝ, 0 < r0 → ∀ k : ℕ,
222 (2.5 : ℝ) < r_orbit r0 (k + 2) / r_orbit r0 k ∧
223 r_orbit r0 (k + 2) / r_orbit r0 k < 2.7) :=
224 ⟨r_orbit_pos, r_orbit_adjacent_ratio, r_orbit_strict_mono,
225 r_orbit_gap_skip_band⟩
226
227end
228
229end PlanetaryFormationFromJCost
230end Astrophysics