pith. machine review for the scientific record. sign in
def definition def or abbrev

planetaryFormationCert

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)

 200def planetaryFormationCert : PlanetaryFormationCert where
 201  r_orbit_pos := r_orbit_pos

proof body

Definition body.

 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. -/

depends on (27)

Lean names referenced from this declaration's body.