NontrivialMultilevelComposition
NontrivialMultilevelComposition is a structure that packages a positive real sequence levels : ℕ → ℝ together with the explicit requirement that the first three terms are positive. Researchers deriving uniform scaling from zero-parameter conditions in Recognition Science cite it as the minimal input type for forcing theorems. The definition is a direct record of three fields with no computational content or proof obligations.
claimA nontrivial multilevel composition is a function $levels : ℕ → ℝ$ such that $levels(k) > 0$ for every natural number $k$, together with the additional stipulation that $levels(0) > 0$, $levels(1) > 0$ and $levels(2) > 0$.
background
The HierarchyForcing module treats Gap 2 of the axiom-closure plan: a nontrivial zero-parameter ledger must produce hierarchical structure. The structure supplies the concrete data that downstream statements convert into a uniform scale ladder. Upstream, RealizedHierarchy (HierarchyRealization) supplies the RS-native replacement for bare multilevel composition: it records a base state, the iterated levels $levels(k) = F.r(F.T^[k] baseState)$, positivity, and the growth condition $1 < levels(1)/levels(0)$. The companion theorem realized_uniform_ratios then asserts that every adjacent ratio equals every other adjacent ratio inside any such realized hierarchy.
proof idea
This is a structure definition with an empty proof body. It simply declares the three fields levels, levels_pos and at_least_three; no tactics or lemmas are applied.
why it matters in Recognition Science
The structure is the explicit input to uniform_scaling_forced, hierarchy_forced and hierarchy_forced_gives_phi. It therefore supplies the data that converts the Recognition Composition Law and the self-similar fixed-point condition (T6) into a concrete phi-ladder with D = 3. By feeding hierarchy_forced_gives_phi it closes the step that extracts the numerical value σ = φ from the forced hierarchy, completing one link in the T0–T8 forcing chain.
scope and limits
- Does not prescribe any particular value for the common ratio between consecutive levels.
- Does not require the levels to be generated by an observable carrier or dynamics T.
- Does not impose additivity or any other composition rule on the levels.
- Does not assume the existence of a self-similar fixed point or the value φ.
formal statement (Lean)
78structure NontrivialMultilevelComposition where
79 levels : ℕ → ℝ
80 levels_pos : ∀ k, 0 < levels k
81 at_least_three : 0 < levels 0 ∧ 0 < levels 1 ∧ 0 < levels 2
82
83/-- **Theorem**: No free scale parameters forces uniform adjacent ratios.
84
85The canonical derivation now uses `HierarchyRealization.realized_uniform_ratios`
86which derives uniform ratios from the `RealizedHierarchy.ratio_self_similar`
87field, with `no_continuous_moduli` as backup
88(`HierarchyRealization.no_moduli_forces_uniform_ratios`). -/