unit_coefficients_minimal
plain-language theorem explainer
The result shows that among natural numbers a and b each at least 1 the sum a + b reaches its minimum value of 2 precisely when a = b = 1. Workers deriving the lepton charge index Z_ℓ = 1332 from the even polynomial ansatz cite this fact to fix the smallest admissible coefficients. The proof is a one-line term that invokes the omega tactic on the two inequalities.
Claim. For all natural numbers $a, b$ with $a, b$ at least 1, the inequality $a + b$ at least 2 holds.
background
The ZMapDerivation module builds the lepton charge index from the even polynomial Z(Q̃) = a Q̃² + b Q̃⁴ with Q̃ the integerized electron charge equal to -6. The sibling definition Z_poly implements this map and records that it is even in its charge argument with no constant term. The upstream BaselineDerivation.Z_poly carries the same definition and adds that the map is strictly increasing on positive integers once a and b are at least 1. The module document states that coefficient minimality requires the unique pair minimizing a + b subject to those lower bounds, and that this pair yields Z_ℓ = 1332.
proof idea
The proof is a one-line term that applies the omega tactic directly to the hypotheses 1 ≤ a and 1 ≤ b, discharging the target inequality 2 ≤ a + b.
why it matters
The declaration supplies the coefficient-minimality step required by the module document to select a = b = 1 and obtain Z_ℓ = 1332 from the polynomial evaluated at Q̃ = -6. It therefore supports the overall derivation that begins with charge integerization k = F(3) = 6 and ends at the numerical value 1332. No downstream uses are recorded, and the result does not invoke the forcing chain T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.