per_nucleon_phi_factor_pos
plain-language theorem explainer
The theorem asserts that the per-nucleon phi factor phi^k remains strictly positive for every natural number rung k. Nuclear modelers working in the Recognition Science phi-ladder would cite it when assembling the master binding-energy certificate. The proof is a one-line term reduction that unfolds the definition and applies the standard positivity of powers of the positive constant phi.
Claim. For every natural number $k$, the per-nucleon J-cost factor satisfies $0 < phi^k$, where $phi$ is the self-similar fixed point of the Recognition Composition Law.
background
In the Recognition Science treatment of nuclear binding, each nucleon contributes a bond cycle whose J-cost contribution is tracked on the phi-ladder. The auxiliary definition per_nucleon_phi_factor k := phi^k supplies the recognition contribution at rung k. The surrounding module derives the iron-peak rung from the D=3 identity k_iron = consciousnessGap - configDim - holonomyShift = 26, placing the saturation of the eight-tick octave at that level.
proof idea
The term proof unfolds per_nucleon_phi_factor to expose phi^k and then applies the lemma pow_pos together with the already-established positivity of phi.
why it matters
The result is referenced inside the bindingEnergyCert record (via the field per_nucleon_pos) and inside iron_to_alpha_factor_pos, thereby closing the positivity obligations for the master certificate. It supports the parameter-free claim that the binding-energy maximum occurs at the phi-ladder rung forced by T7 and T8 of the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.