Z_strictly_increasing
plain-language theorem explainer
The declaration proves that the Z-map polynomial Z(a, b, q) = a q² + b q⁴ is strictly increasing in the charge index q for a, b at least 1. Mass-spectrum workers in Recognition Science cite it to guarantee ordered rungs on the baseline ladder derived from D = 3. The proof unfolds the quartic, invokes Nat.pow_lt_pow_left on the even powers, multiplies the resulting inequalities by the positive coefficients a and b, and closes with linarith.
Claim. Let $a, b$ be positive integers. For positive integers $q_1 > q_2 > 0$, $a q_2^2 + b q_2^4 < a q_1^2 + b q_1^4$.
background
The BaselineDerivation module upgrades boundary assumptions about rung integers to theorems derived from the combinatorics of the 3-cube Q₃ at D = 3. The Z-map polynomial is defined by Z_poly(a, b, q) := a q² + b q⁴ and serves as the charge index for baseline mass assignments. B-26 records the monotonicity statement that is now proved rather than assumed.
proof idea
Unfold Z_poly. Apply Nat.pow_lt_pow_left to obtain strict inequalities for the squares and fourth powers of q₂ and q₁, cast to ℤ, multiply on the left by the positive integers a and b using mul_lt_mul_of_pos_left, then finish with linarith.
why it matters
The theorem supplies the monotonicity required by neutrino_rung and completes the B-26 upgrade listed in the module table. It anchors the ordering of charge indices in the D = 3 derivations that feed the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.