minimal_complete_coefficients
plain-language theorem explainer
Minimal complete coefficients satisfy a + b ≥ 2 for any natural numbers a and b each at least 1. This anchors the Z-map monotonicity condition in baseline rung derivations from the 3-cube. Recognition Science mass derivations cite it to fix the minimal pair at (1,1). The proof applies the omega tactic directly to the input inequalities.
Claim. For all natural numbers $a, b$, if $a ≥ 1$ and $b ≥ 1$ then $a + b ≥ 2$.
background
The module derives baseline rung integers, octave offsets, and generation orderings from the combinatorics of the 3-cube Q₃ at D = 3, converting prior boundary assumptions into derived results. Items include non-triviality from J(1) = 0, lepton baseline A + 1 = 2, quark baseline 2^(D-1) = 4, and completeness via a ≥ 1 ∧ b ≥ 1 for Z-map monotonicity. Upstream results supply rung definitions in lepton, quark, and anchor sectors together with completeness predicates from backpropagation states.
proof idea
The proof is a one-line term that applies the omega tactic to the hypotheses 1 ≤ a and 1 ≤ b to conclude a + b ≥ 2.
why it matters
This result supplies the completeness condition B-26 in the baseline derivations, enabling the full rung table for leptons, quarks, and neutrinos. It directly implements the Z-map monotonicity item listed in the module documentation and supports subsequent octave offset and generation ordering statements. The declaration closes a foundational gap in the D = 3 cube-geometric derivations of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.