minimal_coefficients
The theorem states that any positive integers a and b satisfy a + b at least 2. It is invoked in the Z-map derivation to certify that the coefficient pair (1,1) achieves the minimal sum under the constraints a ≥ 1, b ≥ 1 for the even polynomial ansatz. The proof is a direct term-mode application of the omega tactic to the supplied inequalities.
claimFor all natural numbers $a, b$, if $a ≥ 1$ and $b ≥ 1$ then $a + b ≥ 2$.
background
The module derives the lepton charge index Z_ℓ = 1332 by integerizing the electron charge to Q̃_e = -6 via the face count k = F(3) = 6, then positing the even polynomial Z(Q̃) = a Q̃² + b Q̃⁴ that respects charge-conjugation invariance and non-negativity. Coefficient minimality requires the unique pair (a, b) = (1, 1) that minimizes a + b subject to a ≥ 1, b ≥ 1. This theorem supplies the lower bound a + b ≥ 2 that certifies the minimality claim.
proof idea
One-line term proof that applies the omega tactic directly to the two hypotheses 1 ≤ a and 1 ≤ b, yielding the conclusion 2 ≤ a + b for natural numbers.
why it matters in Recognition Science
The result closes the coefficient-minimality step in the Z-map derivation, confirming that (1,1) is admissible and minimal before the explicit evaluation Z_ℓ = 36 + 1296 = 1332. It feeds the sibling lemmas Z_lepton_eq and Z_lepton_matches_anchor_value that complete the bridge from the polynomial ansatz to the numerical value used in downstream RSBridge calculations.
scope and limits
- Does not derive the even polynomial form or the integerization scale k = 6.
- Does not compute the explicit value of Z_ℓ or evaluate the polynomial.
- Does not address uniqueness of the minimizing pair beyond the sum lower bound.
- Does not connect to the phi-ladder or T0–T8 forcing chain.
formal statement (Lean)
69theorem minimal_coefficients :
70 ∀ a b : ℕ, 1 ≤ a → 1 ≤ b → 2 ≤ a + b :=
proof body
Term-mode proof.
71 fun _ _ ha hb => by omega
72
73/-- (1,1) achieves the minimum. -/