pith. sign in
theorem

additive_composition_is_minimal

proved
show as:
module
IndisputableMonolith.Foundation.HierarchyForcing
domain
Foundation
line
108 · github
papers citing
2 papers (below)

plain-language theorem explainer

For natural numbers a and b each at least 1, the condition max(a, b) = 1 forces a = 1 and b = 1. Researchers closing the zero-parameter ledger to hierarchical structure cite this arithmetic fact to obtain unit recurrence coefficients. The proof is a short term-mode argument that introduces the max hypothesis and applies antisymmetry of ≤ after omega extracts the reverse inequalities from the given lower bounds.

Claim. For natural numbers $a, b$ with $a ≥ 1$ and $b ≥ 1$, if $max(a, b) = 1$ then $a = 1$ and $b = 1$.

background

This theorem sits in HierarchyForcing as part of Phase 3 of the axiom-closure plan for Gap 2, which derives nontrivial hierarchical structure from a zero-parameter ledger. The module establishes both uniform scaling and minimal integer coefficients; the present result supplies the pure-arithmetic half of the latter, with no axioms required.

proof idea

The proof introduces the hypothesis max a b = 1. It constructs the conjunction by applying Nat.le_antisymm (after omega resolves a ≤ 1 from the max and the given ha) to obtain a = 1, and likewise for b. The upstream le_antisymm supplies the mutual-inequality-to-equality step in the natural numbers.

why it matters

The result is invoked verbatim by zero_param_forces_unit_coefficients in HierarchyDynamics, which restates it as the bridge fact that minimal integer coefficients are forced by the zero-parameter posture. It completes the Phase 3 arithmetic step in the module doc, feeding the derivation of uniform ratios and the subsequent phi-ladder forcing in the Recognition Science chain.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 2 of 2)