Foundation Hierarchy Forcing Additive Composition Is Minimal

The minimal composition law

In mathematics, a recurrence like x(n+2) = a·x(n+1) + b·x(n) builds a sequence from two previous terms. The coefficients a and b are positive whole numbers. The smallest possible value for the larger of the two, max(a, b), is 1. The only way to achieve that minimum is to set both a and b to 1. This is a pure fact of arithmetic, with no further assumptions needed.

The Recognition Science framework uses this fact in its account of hierarchical structure. The framework models a hierarchy as a discrete record, a ledger, of levels where each level is built from the previous ones. Within that model, a recurrence with coefficients (1, 1) means each level is simply the sum of the two levels before it. This is the minimal possible additive rule: any other positive coefficients would make the larger one at least 2.

In the framework's machine-checked library of formal theorems, the declaration additive_composition_is_minimal records this result. It proves that if max(a, b) equals 1, then a and b must both be 1. A companion theorem shows that any other pair of positive coefficients has max(a, b) at least 2. These are statements about natural numbers, proved from the basic properties of order and arithmetic.

The importance for the framework is indirect. A separate theorem, hierarchy_forced_gives_phi, shows that when a hierarchy has no free scale parameters and obeys this additive rule, the ratio between successive levels is forced to be the golden ratio, about 1.618. The minimality of (1, 1) is a necessary ingredient in that chain, but it does not by itself produce the golden ratio. The minimality statement only concerns the coefficients; it says nothing about the resulting sequence or its ratio.

What the declaration does not claim is just as precise. It does not assert that the golden ratio emerges from the minimality of (1, 1) alone. It does not claim that any hierarchy must use additive composition. It only establishes a fact about natural numbers: among positive coefficient pairs, (1, 1) is the unique pair that minimizes the larger coefficient. The framework's broader conclusions about hierarchies and the golden ratio depend on additional conditions, such as the absence of free scale parameters and the additive rule itself.

/-- **Theorem (Phase 3)**: Among recurrence coefficients (a, b) with
a ≥ 1 and b ≥ 1, the pair (1, 1) uniquely minimizes max(a, b).
No axiom needed — this is pure arithmetic. -/
theorem additive_composition_is_minimal (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b) :
    max a b = 1 → a = 1 ∧ b = 1 := by
  intro h
  constructor
  · exact Nat.le_antisymm (by omega) ha
  · exact Nat.le_antisymm (by omega) hb

/-- Any other pair has max ≥ 2. -/
theorem other_pairs_larger (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b)
    (h : ¬(a = 1 ∧ b = 1)) : 2 ≤ max a b := by omega

/-- The pair (1,1) achieves max = 1. -/
theorem min_max_achieved : max 1 1 = 1 := by simp

What this page does not claim

The golden ratio emerges from the minimality of (1, 1) alone. Any hierarchy must use additive composition. The minimality statement applies to non-positive or non-integer coefficients.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/HierarchyForcing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: