yukawaAt_bounded_above
plain-language theorem explainer
Recognition Science maps each fermion to a rung on the phi-ladder and defines its Yukawa coupling as one minus the J-cost at that rung. The theorem shows the resulting coupling is at most one for any integer rung. Model builders checking mass hierarchy consistency would cite this bound. The argument unfolds the definition and applies the non-negativity lemma for J-cost together with linarith.
Claim. For every integer $r$, the Yukawa coupling $1 - Jcost(phi^{r-8})$ satisfies $1 - Jcost(phi^{r-8}) ≤ 1$.
background
The module derives Yukawa couplings from the J-cost structure. Each fermion occupies a rung $r$ on the phi-ladder relative to the electron at rung 8. Its coupling is then 1 minus Jcost of phi to the power (r-8). The J-cost satisfies non-negativity for positive arguments by the AM-GM inequality, as stated in Jcost_nonneg: J(x) ≥ 0 for x > 0.
proof idea
The proof unfolds yukawaAt to expose 1 minus Jcost of phi to the (r-8). It asserts positivity of that power via zpow_pos applied to Constants.phi_pos. Linarith then combines the result with Jcost_nonneg to obtain the inequality.
why it matters
The bound is packaged into the YukawaCert record as the bounded_above field, alongside the rung-8 unity case. It underpins the module's claim that the phi-ladder generates the observed fermion mass hierarchy with couplings in the unit interval. In the framework this step closes the upper bound required for consistency with the Recognition Composition Law and the T5 J-uniqueness property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.