nonuniform_ratios_yield_moduli
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
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of non-uniform ratios in any concrete hierarchy.
- Does not derive uniform ratios without the no-continuous-moduli hypothesis.
- Does not apply to frameworks lacking the carrier_lifts_perturbations property.
- Does not address finite or discrete carrier spaces.
formal statement (Lean)
145theorem nonuniform_ratios_yield_moduli
146 (F : ClosedObservableFramework)
147 (levels : ℕ → ℝ)
148 (levels_pos : ∀ k, 0 < levels k)
149 (_levels_from_carrier : ∀ k, ∃ s : F.S, F.r s = levels k)
150 (carrier_lifts_perturbations :
151 ∀ (_k : ℕ) (v : ℝ), 0 < v →
152 ∃ s : F.S, F.r s = v) :
153 (∃ j k, levels (j + 1) / levels j ≠ levels (k + 1) / levels k) →
154 ∃ (embed : ℝ → F.S), Function.Injective embed := by
proof body
Tactic-mode proof.
155 intro ⟨j, _, _⟩
156 have h_pos : 0 < levels (j + 1) := levels_pos (j + 1)
157 have h_ne : levels (j + 1) ≠ 0 := ne_of_gt h_pos
158 choose lift h_lift using fun (t : ℝ) =>
159 carrier_lifts_perturbations (j + 1) (levels (j + 1) * Real.exp t)
160 (mul_pos h_pos (Real.exp_pos t))
161 refine ⟨lift, fun t₁ t₂ h_eq => ?_⟩
162 have h1 : F.r (lift t₁) = levels (j + 1) * Real.exp t₁ := h_lift t₁
163 have h2 : F.r (lift t₂) = levels (j + 1) * Real.exp t₂ := h_lift t₂
164 have h3 : F.r (lift t₁) = F.r (lift t₂) := by rw [h_eq]
165 rw [h1, h2] at h3
166 exact Real.exp_injective (mul_left_cancel₀ h_ne h3)
167
168/-- **Corollary**: In a `ClosedObservableFramework` where the observable
169can realize all positive values, non-uniform ratios are impossible. -/