nonuniform_ratios_yield_moduli
plain-language theorem explainer
Non-uniform successive ratios in a hierarchy realized inside a ClosedObservableFramework force an injective embedding of the reals into the carrier states whenever the observable can hit every positive real. Researchers closing the T5-to-T6 bridge in Recognition Science cite this to show that deviation from self-similar ratios requires continuous moduli. The proof fixes one level with a non-uniform ratio, lifts exponential perturbations of its value to carrier states via the given hypothesis, and recovers injectivity from the injectivity of the
Claim. Let $F$ be a closed observable framework with state space $S$ and positive observable $r:S→ℝ$. Let $ℓ:ℕ→ℝ$ be positive with each value $ℓ(k)$ realized by $r$ on some state in $S$, and suppose every positive real is likewise realized by $r$. If the ratios $ℓ(k+1)/ℓ(k)$ are not all equal, then there exists an injective map $ℝ→S$.
background
The HierarchyRealization module internalizes the earlier free-floating levels interface by tying each level value directly to a carrier state via the observable $r$ of a ClosedObservableFramework. That structure supplies states $S$, deterministic dynamics $T$, and a positive observable $r$ obeying non-trivial observability and closure. The module doc notes that the sensitivity bridge (non-uniform ratios imply an injection $ℝ→S$) and additive composition are now native fields rather than external hypotheses on a ZeroParameterComparisonLedger.
proof idea
Assume non-uniform ratios and pick index $j$. The carrier_lifts_perturbations hypothesis supplies a lift function realizing the family levels$(j+1)⋅exp(t)$ for every real $t$. Equal images under $r$ then give equal scaled exponentials; cancellation against the nonzero level value followed by injectivity of exp forces the parameters $t$ to coincide, establishing injectivity of the lift.
why it matters
The theorem supplies the forward half of the sensitivity bridge and is invoked directly by the sibling corollary no_moduli_forces_uniform_ratios, which concludes that uniform ratios are forced once continuous moduli are forbidden. It therefore closes one direction of the T5 J-uniqueness to T6 phi-fixed-point step in the forcing chain, using the self-similarity of the J-cost functional. The result touches the open question whether the ClosedObservableFramework alone suffices or whether the stronger GeometricScaleSequence.isClosed witness from the companion file is required.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.