Pith. sign in
theorem

uniformClosedLevels_eq_original_of_uniform_scale

proved
show as:
module
IndisputableMonolith.Foundation.UnifiedForcingChain
domain
Foundation
line
2070 · github
papers citing
none yet

plain-language theorem explainer

If a multilevel hierarchy already obeys the canonical uniform-scale law (each adjacent level is the previous times the hierarchy's own base ratio), uniform closure leaves every level unchanged. Hierarchy-forcing and scale-rigidity arguments cite this as the "already uniform" direction of the closure characterization. The proof is induction on the level index, feeding the uniform step identity into the closure recurrence.

Claim. Let $M$ be a nontrivial multilevel composition: a strictly positive real sequence $(M_k)_{k\in\mathbb{N}}$ with at least three levels. Suppose $M$ satisfies the canonical uniform-scale law, i.e. $M_{k+1}=r_M\,M_k$ for every $k$, where $r_M$ is the canonical base ratio of $M$. Then the uniformly closed multilevel composition $\overline{M}$ of $M$ agrees with $M$ at every level: $\overline{M}_k=M_k$ for all $k$.

background

This sits in the Unified Forcing Chain module, which derives the full T-1 through T8 ladder from the Recognition Composition Law plus normalization and calibration. Multilevel compositions encode discrete scale hierarchies: a positive real sequence of levels with a nontriviality floor (at least three positive levels).

The canonical uniform-scale law is the theorem-shaped replacement for a raw all-pairs "no free scale" hypothesis. It asserts that every adjacent step is generated by one fixed base ratio of the hierarchy itself: $M_{k+1}=r_M M_k$. Uniform closure rebuilds a hierarchy so that its levels obey that recurrence; the present result says that if the input already obeys the law, closure is the identity on levels.

Upstream, nontrivial multilevel compositions supply the ambient object; the uniform-scale structure packages the step identity used at each successor. Related scale constructions elsewhere in the stack (phi-powers, self-similar dressings) motivate why a single base ratio is the forced rigid form, but the argument here is purely about the level sequence and its closure operator.

proof idea

Term-mode proof by induction on the level index $k$.

Base case $k=0$: unfold the definition of the uniformly closed multilevel composition; the ground level is copied, so equality is immediate by simplification.

Successor: rewrite the closed level at $k+1$ via the closure step recurrence, replace the closed step by the assumed uniform-scale identity $M_{k+1}=r_M M_k$, and finish with the inductive hypothesis that closed and original levels already agree at $k$. The three rewrites chain to equality at $k+1$.

why it matters

This is the "forward" half of the characterization that uniform closure preserves the original level sequence if and only if the hierarchy already satisfies the canonical uniform-scale law. The parent biconditional packages both directions; the sibling idempotence theorem (closing twice changes no levels) uses the same circle of facts to show closure is a true projection onto the uniform-scale class.

In the forcing chain, free scale parameters are ruled out so that discrete self-similarity can pin $\varphi$ (T6) and the octave structure (T7/T8). A closure operator that is idempotent and fixes exactly the uniform hierarchies is the algebraic witness that "no free scale" has a canonical, non-ad-hoc realization. Without this identity-on-uniforms lemma, one could not cleanly separate already-rigid hierarchies from those that still need to be projected.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.