binding_dominates
plain-language theorem explainer
Binding energy on the φ-ladder at rung 14 exceeds forty times the valence-quark mass sum at rung 4. Recognition Science derivations of the proton mass cite this separation to treat m_p as essentially the binding term. The tactic proof reduces the claim to a lower bound on φ^10 by repeated application of the recurrence φ² = φ + 1 and closes the inequality with linear arithmetic.
Claim. Let $E_ {binding} = E_{coh} · φ^{14}$ where $E_{coh}$ is the base coherence energy, and let $m_{valence}$ be the sum of up- and down-quark contributions each evaluated at rung 4. Then $E_{binding} > 40 · m_{valence}$.
background
The module assembles the proton mass from two φ-ladder terms. Valence quarks sit at rung 4 while the binding energy sits at the confinement rung r_binding = 14. The auxiliary definition mass_on_rung(r) := Anchor.E_coh · φ^r supplies both contributions. Upstream lemmas establish the golden-ratio identities φ² = φ + 1 and the strict lower bound φ > 1.61 that drive all numerical estimates.
proof idea
Unfold the two sides into mass_on_rung expressions. Rewrite φ^14 = φ^4 · φ^10 and φ^10 = φ^5 · φ^5. Derive φ^5 = 5φ + 3 from the recurrence, combine with φ > 1.61 to obtain φ^5 > 11 and therefore φ^10 > 120. Multiply by the positive base Anchor.E_coh · φ^4 and apply nlinarith to finish.
why it matters
The result quantifies the dominance of binding over valence in the proton-mass construction of module C-008. It is invoked by the subsequent definitions of m_p and m_p_pos. In the broader framework it supplies the factor-of-40 separation that follows from the rung difference of 10 steps on the φ-ladder and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.