different_rungs_different_barriers
plain-language theorem explainer
Reactions at distinct rungs of the phi-ladder produce unequal activation barriers under the J-cost definition. Enzyme specificity arguments cite this to show why a catalyst tuned to one rung cannot flatten the saddle for another. The term proof unfolds the barrier to J, reduces equality via J(1)=0, and invokes injectivity of the map r to phi^r on the naturals.
Claim. If $r_1, r_2$ are distinct natural numbers, then $J(φ^{r_1}) - J(1) ≠ J(φ^{r_2}) - J(1)$, where $J(x) = ½(x + x^{-1}) - 1$.
background
J is the Recognition cost function $J(x) = ½(x + x^{-1}) - 1$ with minimum zero at the reactant point x=1 (upstream J_one). The activation barrier at a transition-state coordinate x* is defined as J(x*) - J(1). The module frames enzymes as J-cost lenses whose geometry cancels the saddle J(x*) exactly when the active-site rung matches the substrate rung on the phi-ladder. The phi-ladder is the discrete sequence of positive powers of the self-similar fixed point phi forced in the T6 step of the unified forcing chain.
proof idea
Term-mode proof. Unfold activationBarrier and J_one to obtain the equality J(φ^{r1}) = J(φ^{r2}). Assume the barriers coincide, apply pow_left_injective₀ (using phi_pos and the rung inequality) to recover φ^{r1} = φ^{r2}, then discharge the contradiction with the supplied hypothesis r1 ≠ r2.
why it matters
Supplies the rung-distinctness step required by the downstream theorem off_target_not_ideal, which states that an ideal enzyme for one rung yields nonzero catalyzed barrier on any other rung. This closes the specificity claim in the module doc-comment: zero-cancellation is rung-exact, so off-target substrates cannot be cancelled. It directly instantiates the phi-scaling of active sites listed as key result 3 in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.