phi_ladder_step
plain-language theorem explainer
Adjacent tiers on the φ-ladder differ by a multiplicative factor of φ. Modelers of stellar nucleosynthesis in Recognition Science cite this recurrence to relate densities at consecutive tiers. The proof proceeds by unfolding the power definition of the ladder, rewriting the exponent using the non-vanishing of φ, and applying ring simplification.
Claim. For any integer tier index $n$, the φ-ladder value satisfies $φ$-ladder$(n+1) = φ · φ$-ladder$(n)$.
background
A φ-tier is an integer index on the φ-ladder. The φ-ladder value at tier n is defined as φ raised to n. The module develops Strategy 2 for deriving mass-to-light ratios from the discrete φ-tier structure of nuclear densities and photon fluxes.
proof idea
The term proof unfolds the definition of the φ-ladder as φ to the power of the tier and the definition of φ. It rewrites the exponent addition using the lemma phi_ne_zero that φ is nonzero, then simplifies the expression with the ring tactic.
why it matters
This lemma provides the basic recurrence for the φ-ladder, which is required to compute tier differences in the nucleosynthesis-derived M/L ratio. It fills the step that allows M/L to be expressed as φ to an integer power, matching the main result of the module that M/L belongs to the set of φ^n for n between 0 and 3. The construction ties to the eight-tick octave period in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.