additive_composition_is_minimal
plain-language theorem explainer
For natural numbers a and b each at least 1, the condition max(a, b) = 1 forces both to equal 1. Researchers deriving unit recurrence coefficients from zero-parameter ledgers cite this arithmetic fact in Phase 3 of the axiom-closure plan. The proof introduces the max hypothesis and applies order antisymmetry twice, once for each variable, after using omega to obtain the reverse inequalities.
Claim. Let $a, b$ be natural numbers with $a ≥ 1$ and $b ≥ 1$. If $max(a, b) = 1$, then $a = 1$ and $b = 1$.
background
The declaration belongs to the HierarchyForcing module, which treats Gap 2 of the axiom-closure plan: obtaining nontrivial hierarchical structure from a zero-parameter ledger. The module first shows that uniform inter-level ratios are forced, then isolates the minimal integer coefficients that achieve the zero-parameter condition. It imports LedgerCanonicality and HierarchyEmergence for the surrounding ledger and emergence machinery. The upstream lemma le_antisymm states that mutual inequalities imply equality in the logic natural numbers: if a ≤ b and b ≤ a then a = b.
proof idea
The term proof begins by introducing the hypothesis that max a b equals 1. It then builds the conjunction via constructor. For the first conjunct it applies Nat.le_antisymm to the pair consisting of the inequality a ≤ 1 (obtained from the max hypothesis via omega) and the given ha : 1 ≤ a. The second conjunct is obtained identically from hb.
why it matters
The result is invoked directly by zero_param_forces_unit_coefficients in HierarchyDynamics, which restates it as the bridge statement that minimal integer coefficients are forced by the zero-parameter posture. It supplies the second numbered item in the Phase 3 list of the module documentation, completing the arithmetic step needed before uniform scaling can be derived. Within the Recognition framework it supplies the base case for recurrence coefficients that later feed the self-similar fixed-point and eight-tick octave constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
20% high-entropy tokens suffice for effective RL on LLM reasoning
"utilizing only 20% of the tokens while maintaining performance comparable to full-gradient updates... training exclusively on the 80% lowest-entropy tokens leads to a marked decline"
-
Activation differences steer LLMs without retraining
"ActAdd is lightweight: it does not require any machine optimization and works with a single pair of data points"