uniform_scaling_forced
plain-language theorem explainer
Uniform scaling is forced in any nontrivial multilevel composition once adjacent ratios are required to be independent of the choice of level. A researcher deriving hierarchical structure from a zero-parameter ledger would cite this result to rule out free scale parameters. The short tactic proof selects the first ratio as the common value and propagates it using the uniformity assumption together with positivity to clear denominators.
Claim. Let $M$ be a nontrivial multilevel composition, that is, a function levels$: ℕ → ℝ$ with levels$(k) > 0$ for all $k$ and at least three positive initial levels. Suppose the adjacent ratios are constant across all pairs of levels, levels$(j+1)$/levels$(j)$ = levels$(k+1)$/levels$(k)$ for all $j,k$, and the first ratio exceeds one. Then there exists $σ > 1$ such that levels$(k+1) = σ · levels$(k)$ for every $k$.
background
The module addresses Gap 2 in the axiom-closure plan: deriving hierarchical structure from a nontrivial zero-parameter ledger. Phase 3 focuses on forcing uniform scaling. NontrivialMultilevelComposition is the structure consisting of a levels map from naturals to positive reals with at least three initial positive values. The theorem states that the zero-parameter condition (no free scale) forces all adjacent ratios to be identical. Upstream, it relies on the definition of NontrivialMultilevelComposition.
proof idea
The proof is a short tactic sequence. It instantiates the existential with the ratio of the first two levels. The inequality is given by hypothesis. For the universal quantifier it invokes the no_free_scale hypothesis at (k,0), rewrites using div_eq_div_iff and positivity, then applies field_simp and linarith to obtain the scaled equality.
why it matters
This declaration establishes the first theorem in the HierarchyForcing module, showing that non-uniform ratios are incompatible with the zero-parameter condition in Phase 3 of the axiom-closure plan. It supports the derivation of self-similar hierarchies that later connect to the phi fixed point. The result is cited in the module documentation as the core statement that uniform ratios follow from the absence of continuous moduli.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 3 of 3)
-
Hybrid CNN-state space model tops CNNs and Transformers on medical segmentation
"Moreover, U-Mamba enjoys a self-configuring mechanism, allowing it to automatically adapt to various datasets without manual intervention."
-
Qwen3-VL-Embedding-8B leads MMEB-V2 multimodal benchmark with 77.8
"supports Matryoshka Representation Learning, enabling flexible embedding dimensions, and handles inputs up to 32k tokens"
-
Muon reaches 2x efficiency of AdamW on large LLMs
"we scale Muon’s update RMS to this range by the following adjustment: Wt = Wt−1 − ηt(0.2 · Ot · √max(A, B) + λWt−1)"