Foundation Posting Extensivity Closure Forces Additive

What closure forces

A geometric scale sequence is a ladder of levels where each rung is a fixed multiple of the one below it: level 1 equals σ times level 0, level 2 equals σ times level 1, and so on. The real number σ is the ratio between neighboring levels. Classical mathematics has long studied such ladders; the Fibonacci numbers, for instance, form a sequence where each term is the sum of the two before it.

In Recognition Science, the framework models recognition events as entries in a ledger, a discrete record of events, and assigns each event a cost. The framework's central theorem forces the cost function J(x) = ½(x + x⁻¹) − 1 from five plain conditions. From that cost function, a chain of results derives structure. This page concerns one link in that chain: the declaration closure_forces_additive.

The theorem states: if a geometric scale sequence is closed under the first composition step, meaning that composing a level-0 event with a level-1 event produces a level-2 event, then the level sizes satisfy level 2 = level 1 + level 0. The proof is a one-line arithmetic step: the closure condition is exactly the statement that level 0 plus level 1 equals level 2, and the theorem restates it. The theorem does not derive the closure condition from anything more basic; it takes closure as a hypothesis.

The significance is that the additive structure is not assumed as a separate axiom. Earlier versions of the framework posited additive composition directly. This theorem replaces that postulate with a conditional statement: given closure, additivity follows. The framework's library, a machine-checked collection of formal theorems, verifies the step. The theorem is tagged THEOREM because it is proved in the library with no unproved assumptions beyond the standard axioms of the ambient type theory.

What the theorem does not claim is equally important. It does not claim that closure holds in the physical world; that is a separate empirical or modeling question. It does not claim that the ratio σ is the golden ratio; that conclusion requires the further theorem additive_closure_golden, which combines closure with the uniform ladder condition to derive σ² = σ + 1. And it does not claim that the coefficients in a general additive recurrence are 1 and 1; that is the separate result discrete_fibonacci_from_minimality, which assumes natural-number coefficients with max(a, b) = 1.

The practical upshot: within the framework, one can now say that additive scale composition is a consequence of closure under composition, not a free choice. The theorem tightens the derivation chain from the cost function to the golden ratio. It is a small step, but it removes an assumption that previously had to be taken on faith.

/-- **Theorem**: Closure of a geometric scale sequence under additive
composition forces `scale 0 + scale 1 = scale 2`.

This is the RS-internal replacement for the `HasAdditiveComposition`
axiom.  The additive structure is not assumed; it follows from the
physical requirement that composing level-0 and level-1 events must
produce a level-2 event.

The "additive" nature of scale composition comes from the ledger's
posting rule: total recognition work sums, so scales (which measure
work at each level) add when events compose. -/
theorem closure_forces_additive (levels : ℕ → ℝ)
    (_levels_pos : ∀ k, 0 < levels k)
    (_σ : ℝ) (_hσ : 1 < _σ)
    (_uniform : ∀ k, levels (k + 1) = _σ * levels k)
    (closure : levels 0 + levels 1 = levels 2) :
    levels 2 = levels 1 + levels 0 := by
  linarith [closure]

/-- **Theorem**: Closure of a geometric scale sequence under additive
composition forces `scale 0 + scale 1 = scale 2`.

This is the RS-internal replacement for the `HasAdditiveComposition`
axiom.  The additive structure is not assumed; it follows from the
physical requirement that composing level-0 and level-1 events must
produce a level-2 event.

The "additive" nature of scale composition comes from the ledger's
posting rule: total recognition work sums, so scales (which measure
work at each level) add when events compose. -/
theorem closure_forces_additive (levels : ℕ → ℝ)
    (_levels_pos : ∀ k, 0 < levels k)
    (_σ : ℝ) (_hσ : 1 < _σ)
    (_uniform : ∀ k, levels (k + 1) = _σ * levels k)
    (closure : levels 0 + levels 1 = levels 2) :
    levels 2 = levels 1 + levels 0 := by
  linarith [closure]

/-- **Theorem**: Closure of a geometric scale sequence under additive
composition forces `scale 0 + scale 1 = scale 2`.

This is the RS-internal replacement for the `HasAdditiveComposition`
axiom.  The additive structure is not assumed; it follows from the
physical requirement that composing level-0 and level-1 events must
produce a level-2 event.

The "additive" nature of scale composition comes from the ledger's
posting rule: total recognition work sums, so scales (which measure
work at each level) add when events compose. -/
theorem closure_forces_additive (levels : ℕ → ℝ)
    (_levels_pos : ∀ k, 0 < levels k)
    (_σ : ℝ) (_hσ : 1 < _σ)
    (_uniform : ∀ k, levels (k + 1) = _σ * levels k)
    (closure : levels 0 + levels 1 = levels 2) :
    levels 2 = levels 1 + levels 0 := by
  linarith [closure]

What this page does not claim

The closure condition itself is not derived from the cost function; it is assumed as a hypothesis. The golden ratio conclusion is not established by this theorem alone, but by the separate additive_closure_golden result. The coefficients in a general additive recurrence are not shown to be 1 and 1 here; that is the separate discrete_fibonacci_from_minimality theorem. The framework does not claim that closure holds empirically in any particular physical system.

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/PostingExtensivity.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: