Z_poly_strictly_increasing
plain-language theorem explainer
The theorem shows that the charge index polynomial Z(a,b,q) = a q² + b q⁴ is strictly increasing in the positive integer argument q whenever the coefficients satisfy a ≥ 1 and b ≥ 1. It is invoked in derivations that order lepton charge indices by magnitude within the Recognition Science Z-map. The proof unfolds the definition, invokes monotonicity of integer powers, casts coefficients to positive integers, and closes the inequality with linarith.
Claim. For natural numbers $a,b$ with $a≥1$, $b≥1$ and positive integers $q_1>q_2>0$, the polynomial $Z(a,b,q)=a q^2 + b q^4$ satisfies $Z(a,b,q_2)<Z(a,b,q_1)$.
background
Z_poly is the even polynomial $Z(Q̃)=a Q̃^2 + b Q̃^4$ with no constant term, used to map integerized charge $Q̃_e=-6$ to the lepton charge index. The module derives $Z_ℓ=1332$ from the structural face count $k=F(3)=6$, the minimal coefficients $(a,b)=(1,1)$, and the even-polynomial ansatz that enforces charge-conjugation invariance and non-negativity. The upstream definition in BaselineDerivation states that if $a≥1$ and $b≥1$ then Z is strictly increasing on the positive integers.
proof idea
The tactic proof unfolds Z_poly, applies Nat.pow_lt_pow_left to obtain $q_2^2<q_1^2$ and $q_2^4<q_1^4$, casts $a$ and $b$ to positive integers via exact_mod_cast, and finishes with linarith on the two scaled inequalities.
why it matters
It supplies the monotonicity needed to order charge indices in the lepton sector of the Z-map derivation. The module summary records that the same index 1332 is shared by electron, muon and tau once the minimal even polynomial is fixed. The result sits inside the RSBridge layer that converts the geometric input $k=6$ into the numerical anchor used by the mass formula on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.