no_moduli_forces_uniform_ratios
plain-language theorem explainer
In a ClosedObservableFramework whose observable realizes every positive real, any sequence of positive hierarchy levels must have identical adjacent ratios. Researchers closing the T5-to-T6 bridge in Recognition Science cite it to remove free scale parameters from the hierarchy. The proof is a short contradiction that invokes nonuniform_ratios_yield_moduli to produce a forbidden injection into the carrier, which the framework's no_continuous_moduli axiom immediately rules out.
Claim. Let $F$ be a closed observable framework with positive observable $r:S→ℝ$ that attains every positive real value. For any sequence of positive reals $ℓ:ℕ→ℝ$, the adjacent ratios are uniform: $∀j,k∈ℕ$, $ℓ(j+1)/ℓ(j)=ℓ(k+1)/ℓ(k)$.
background
A ClosedObservableFramework consists of a state space $S$, deterministic dynamics $T:S→S$, and positive observable $r:S→ℝ$ together with the axiom that no continuous moduli exist (no injection $ℝ↪S$). This module internalizes abstract hierarchy levels as values of $r$ on carrier states, converting earlier external bridge hypotheses into native fields of the framework. The upstream nonuniform_ratios_yield_moduli theorem states that non-uniform ratios plus the lifting property for perturbations imply the existence of such an injection into $S$.
proof idea
The proof proceeds by contradiction. Assume the ratios are not all equal. Apply the nonuniform_ratios_yield_moduli theorem (with the given positivity, carrier-lifting, and perturbation-lifting hypotheses) to obtain an embedding of the reals into the carrier together with an injection. This immediately contradicts the no_continuous_moduli axiom of the ClosedObservableFramework.
why it matters
This corollary supplies the uniform-ratio conclusion required by NontrivialMultilevelComposition in HierarchyForcing. It completes the internal derivation of the T5-to-T6 bridge inside the ClosedObservableFramework, forcing self-similar ratios without external parameters and aligning with the J-cost uniqueness that selects the phi ladder. The result touches the open question whether the framework alone suffices or whether an earlier geometric-scale witness remains necessary.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.