AgreesAtHalfRung
plain-language theorem explainer
A measured semi-major axis agrees with the Recognition Science φ-ladder at scale r0 when it lies inside the closed interval bounded by one rung value scaled by 1/√φ and √φ. Astrophysicists testing J-cost minimization in protoplanetary disks cite this predicate to certify agreement with the predicted multiplicative ladder against observed radii. The definition is the direct existential quantification over rung index k using the already-defined orbit function.
Claim. A measured semi-major axis $r$ agrees with the φ-ladder at inner scale $r_0$ if there exists a natural number $k$ such that $r_0 φ^k / √φ ≤ r ≤ r_0 φ^k · √φ$.
background
In the Recognition Science treatment of planetary formation, a protoplanetary disk minimizes J-cost on radial bond density when orbital radii occupy the multiplicative φ-ladder $r(k) = r_0 · φ^k$. The half-rung tolerance predicate declares that a measured radius lies within a factor √φ ≈ 1.272 of some ladder rung; this width equals half the adjacent ratio in log-space and follows from the self-similar fixed point forced in T6. The module imports φ from the core constants and uses the orbit function that multiplies the reference scale by successive powers of φ. Upstream results supply rung conventions from mass anchors and spin statistics, but the local predicate isolates the geometric tolerance band without reference to sector offsets.
proof idea
The definition is the direct existential statement that the measured radius lies in the closed interval [r(k)/√φ, r(k)·√φ] for some natural number k, where r(k) is the orbit function. No lemmas are invoked; the body simply unfolds the interval condition using the already-defined orbit function.
why it matters
This predicate supplies the tolerance band required by the ladder_agrees_at_half_rung theorem and the PlanetaryFormationCert structure, both of which witness that every exact rung satisfies the half-rung condition. It operationalizes the T6 self-similarity argument for orbital radii in the astrophysics track, allowing empirical tests of the J-cost derivation of the Titius-Bode pattern against observed semi-major axes with only a single overall scale r0. The half-rung width follows immediately from the adjacent ratio φ in the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.