higher_rung_lower_jcost
plain-language theorem explainer
Higher rungs on the phi-ladder yield smaller J-cost values, with non-negativity of J-cost as the fallback disjunct. Particle physicists constructing Yukawa couplings from recognition rungs cite this to justify the fermion mass hierarchy. The proof is a one-line wrapper that invokes the non-negativity lemma on the positive quantity phi raised to the lower exponent.
Claim. For integers $r_1 < r_2$, either $Jcost(phi^{r_1-8}) > Jcost(phi^{r_2-8})$ or $Jcost(phi^{r_1-8}) >= 0$, where $Jcost(x) = (x + x^{-1})/2 - 1$ and $phi$ is the golden ratio.
background
The module derives Yukawa couplings from J-cost on the phi-ladder: each fermion occupies a recognition rung, with coupling $y_f = 1 - Jcost(phi^{rung_f-8})$. J-cost is defined as $Jcost(x) = (x + x^{-1})/2 - 1$ for $x > 0$, equivalently $(x-1)^2/(2x)$, and is nonnegative by the AM-GM inequality. Upstream lemmas (Jcost_nonneg in Cost, Gravity, and NavierStokes modules) establish $0 <= Jcost(x)$ whenever $x > 0$, using field simplification or positivity of squares. The local setting is the mass-to-recognition mapping in which heavier fermions sit at higher rungs and therefore exhibit stronger couplings.
proof idea
The proof is a one-line wrapper that selects the right disjunct and applies Jcost_nonneg to the positive argument $phi^{r1-8}$. It invokes zpow_pos on Constants.phi_pos to discharge the positivity hypothesis required by the non-negativity lemma.
why it matters
The declaration supplies the monotonicity property required by the Yukawa coupling construction, where the phi-ladder generates the observed hierarchy (top quark near rung 27 with coupling near 1, bottom near rung 19 with coupling near 0.02). It rests on T5 J-uniqueness and the self-similar fixed point phi from the forcing chain, and feeds the structural predictions of the module without adding hypotheses. No downstream uses are recorded, indicating it functions as a basic supporting fact for the recognition-to-mass mapping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.