shared_descent
plain-language theorem explainer
The theorem asserts that J-cost is strictly positive for every positive real ratio away from the fixed point at unity. Researchers validating recognition models across empirical substrates would cite it to confirm shared descent behavior. The proof is a one-line wrapper that invokes the core positivity lemma for J-cost.
Claim. For every real number $r$ with $0 < r$ and $r ≠ 1$, the J-cost satisfies $0 < J(r)$.
background
J-cost is the cost function on positive ratios induced by a multiplicative recognizer or recognition event; it vanishes only at the fixed point $r = 1$ and is derived from the comparator in the MultiplicativeRecognizerL4 and ObserverForcing modules. The module ThreeSubstrateValidationCert assembles an empirical certificate that language-model layers, photonic code rates, and magnetized-plasma equilibria all obey the same J-cost properties: fixed point at unity, positive cost off equilibrium, and symmetry under inversion. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 for x ≠ 1 and x > 0, proved by rewriting Jcost via Jcost_eq_sq and applying positivity of squares and division.
proof idea
One-line wrapper that applies Jcost_pos_of_ne_one r hr hne from the Cost module (and its duplicates in JcostCore and LocalCache).
why it matters
The result is assembled into the threeSubstrateCert definition as the descent field, alongside shared_fixed_point and shared_symmetry, to certify that all three substrates obey the same J-cost descent. It directly supports the J-uniqueness step (T5) in the forcing chain and the Recognition Composition Law by guaranteeing that off-equilibrium states incur positive cost in every substrate examined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.