transitionRadius_pos
plain-language theorem explainer
The theorem establishes that the transition radius at rung k on the phi-ladder is strictly positive for every natural number k. Astrophysicists constructing Recognition Science models of galactic rotation curves cite it to place all five regime boundaries in the physical domain. The proof is a one-line wrapper that invokes the positivity of powers of a positive base.
Claim. For every natural number $k$, the transition radius defined by $r_k = phi^k$ satisfies $r_k > 0$, where $phi$ is the Recognition Science self-similar fixed point.
background
The module derives galactic rotation curves from Recognition Science by positing five canonical regimes (rigid-body inner, rising, flat, declining, truncation) whose boundaries lie at successive rungs of the phi-ladder. The transition radius is introduced as the noncomputable definition transitionRadius k := phi ^ k. This construction sits inside the broader forcing chain that fixes phi as the unique self-similar point and yields D = 3 spatial dimensions.
proof idea
The proof is a one-line wrapper that applies the lemma pow_pos to the fact that phi is positive and to the exponent k.
why it matters
The result is consumed by galacticRotationCert, which packages the regime count, the phi ratio between transitions, and the guarantee that every radius is positive. It thereby supplies the positivity half of the certificate that the five-regime structure is well-defined on the phi-ladder, consistent with the eight-tick octave and the mass formula yardstick * phi^(rung-8+gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.