planetaryFormationCert
plain-language theorem explainer
The planetaryFormationCert definition packages the φ-ladder orbital radius properties into a single certificate structure. Astrophysicists deriving Titius-Bode patterns from J-cost minimisation would cite it to invoke the full set of positivity, ratio, and band guarantees at once. It is a direct field-by-field construction that assembles the supporting theorems for r_orbit without additional reasoning steps.
Claim. The certificate asserts that the orbital radius function defined by $r(k) = r_0 φ^k$ for $r_0 > 0$ and $k ∈ ℕ$ satisfies positivity $r(k) > 0$, base case $r(0) = r_0$, adjacent ratio $r(k+1)/r(k) = φ$, strict monotonicity, closed form, adjacent ratio band $(1.61, 1.62)$, gap-skip band, and half-rung agreement AgreesAtHalfRung$(r_0, r(k))$.
background
In the Recognition Science setting a protoplanetary disk minimises J-cost on radial bond density when orbital radii lie on the multiplicative φ-ladder $r_{orbit}(k) = r_0 φ^k$. The function r_orbit is the concrete definition $r_{orbit}(r_0, k) := r_0 · φ^k$. The structure PlanetaryFormationCert collects the key derived properties: positivity for all rungs, zero-rung identity, exact adjacent ratio φ, strict increase, closed form, numerical band constraints, gap-skip band, and the half-rung witness theorem.
proof idea
The definition is a direct construction of the PlanetaryFormationCert structure. Each field is assigned the corresponding theorem: r_orbit_pos to the positivity result, r_orbit_zero to the base-case identity, r_orbit_adjacent_ratio to the ratio theorem, r_orbit_strict_mono to the monotonicity theorem, r_orbit_closed to the closed-form equality, r_orbit_adjacent_ratio_band and r_orbit_gap_skip_band to the band theorems, and ladder_agrees_at_half_rung to the half-rung agreement theorem.
why it matters
This definition supplies the complete one-statement certificate for the planetary-formation model that realises the self-similar fixed point φ forced in T6. It closes the structural prediction for orbital radii in the module, enabling the empirical JPL comparison script. The accompanying module comment states that the ladder is its own half-rung witness, every prediction lying inside its own falsifier band, thereby linking the J-cost minimisation directly to the eight-tick octave and the spatial dimension D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.