Foundation Hierarchy Realization From Scale Scale Step Ratio

The constant step

A geometric scale sequence is a list of numbers where each entry is the previous one multiplied by a fixed factor, the ratio. The theorem scale_step_ratio states the defining property of such a sequence: the quotient of any term by its predecessor equals that fixed ratio. In symbols, for a sequence S and any step k, S(k+1) / S(k) = S.ratio. This is not an assumption added to the framework; it is a proved consequence of the sequence's definition, verified by the machine-checked library of formal theorems.

The proof is a short algebraic argument. The sequence is defined by powers of the ratio, so S(k) is the ratio raised to the k-th power. Dividing the (k+1)-th power by the k-th power cancels the common factors and leaves the ratio itself, provided the ratio is nonzero, which the framework guarantees. The result is a lemma that the library then uses to derive stronger statements about realized orbits, sequences that arise from a base state under repeated application of a transition rule.

In Recognition Science, the framework models a discrete record of events, its ledger, where each step's value is recorded. The theorem realized_closed_scale_ratio_step applies the lemma to such a ledger: if the ledger's values realize a closed geometric scale sequence, then the ratio of consecutive ledger entries is constant. A further theorem, ratio_self_similar_of_realized_closed_scale, extends this to show that the ratio of differences between consecutive entries is also constant, a property called ratio self-similarity.

What the declaration does not claim is that such a realized closed scale model actually exists. The theorems are conditional: if a ledger realizes a closed geometric scale sequence, then certain properties follow. Proving that a realized closed scale model exists from the framework's foundational assumptions alone remains an open target. The library also proves that closure of the scale sequence yields additive posting, meaning the third ledger entry equals the sum of the first two, but again only under the same conditional hypothesis.

/-- In any geometric scale sequence, each adjacent ratio equals the
base ratio. -/
theorem scale_step_ratio (S : GeometricScaleSequence) (k : ℕ) :
    S.scale (k + 1) / S.scale k = S.ratio := by
  unfold GeometricScaleSequence.scale
  rw [pow_succ]
  have hr : S.ratio ≠ 0 := ne_of_gt S.ratio_pos
  have hk : S.ratio ^ k ≠ 0 := pow_ne_zero k hr
  simpa using (mul_div_cancel_left₀ S.ratio hk)

/-- The realized orbit has constant adjacent ratio. -/
theorem realized_closed_scale_ratio_step
    (F : ClosedObservableFramework) (H : RealizedClosedScaleModel F) (k : ℕ) :
    F.r (F.T^[k + 1] H.baseState) / F.r (F.T^[k] H.baseState) = H.scales.ratio := by
  rw [H.realize (k + 1), H.realize k]
  have ha : H.amplitude ≠ 0 := ne_of_gt H.amplitude_pos
  calc
    H.amplitude * H.scales.scale (k + 1) / (H.amplitude * H.scales.scale k)
      = H.scales.scale (k + 1) / H.scales.scale k := by
          rw [mul_div_mul_left _ _ ha]
    _ = H.scales.ratio := scale_step_ratio H.scales k

/-- Therefore the realized orbit satisfies ratio self-similarity. -/
theorem ratio_self_similar_of_realized_closed_scale
    (F : ClosedObservableFramework) (H : RealizedClosedScaleModel F) :
    ∀ k,
      F.r (F.T^[k + 2] H.baseState) / F.r (F.T^[k + 1] H.baseState) =
        F.r (F.T^[k + 1] H.baseState) / F.r (F.T^[k] H.baseState) := by
  intro k
  rw [realized_closed_scale_ratio_step F H (k + 1), realized_closed_scale_ratio_step F H k]

What this page does not claim

The theorem does not prove that any realized closed scale model exists, only that if one does, these properties follow. The theorem does not claim that every ledger has a constant adjacent ratio, only those that realize a closed geometric scale sequence. The additive posting result does not apply to arbitrary ledgers, only to those realizing a closed geometric scale sequence.

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