Pith. sign in
theorem

admissibleOrbitReflection_of_minimalClosedScaleOrbit

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

plain-language theorem explainer

Any minimal closed-scale orbit on a closed observable framework yields admissible-orbit reflection at its base state: first-step growth and constant adjacent ratios. Cited when routing minimal hierarchy data into the φ-uniform normal-form package. Proof is a two-step term composition: build the realized closed-scale model from the orbit, then apply the realized-scale reflection lemma.

Claim. Let $F$ be a closed observable framework (positive observables, dynamics $T$, ratio map $r$). Let $O$ be a minimal closed-scale orbit on $F$: a base state $s$, amplitude $A>0$, and a minimal hierarchy such that $r(T^k s)=A\cdot\mathrm{scale}(k)$ for all $k$. Then the orbit at $s$ is admissible: $r(Ts)/r(s)>1$, and adjacent ratios are self-similar, $r(T^{k+2}s)/r(T^{k+1}s)=r(T^{k+1}s)/r(T^k s)$ for all $k$.

background

The module UnifiedForcingChain aims at a complete inevitability chain T-1 through T8 from the Recognition Composition Law plus normalization and calibration. Closed observable frameworks package a state space $S$, dynamics $T:S\to S$, and a strictly positive ratio observable $r$, with nontriviality and closure (no external input, countable states).

A minimal closed-scale orbit records that some orbit realizes a minimal geometric hierarchy: $r(T^k s)=A\cdot\mathrm{scale}(k)$ with $A>0$. Growth and closedness are not extra fields; they come from the underlying minimal hierarchy. Admissible-orbit reflection is the missing exact data that turns a bare closed framework into the φ-uniform normal form: first-step growth and constant successive ratios (self-similarity along the orbit), plus the additive seed-posting side of the package.

Upstream, the scale ladder is the φ-power sequence $\mathrm{scale}(k)=\varphi^k$. The present lemma sits between hierarchy realization and the admissible-orbit bridge used for T6-style self-similarity forcing.

proof idea

Term-mode composition, two applications. First, realizedClosedScaleModel_of_minimalOrbit converts the minimal closed-scale orbit $O$ on $F$ into a realized closed-scale model (the theorem-backed intermediate that packages the same orbit as a closed-scale realization). Second, admissibleOrbitReflection_of_realizedClosedScale is applied to that model, producing AdmissibleOrbitReflection F O.baseState. No extra case splits or algebraic work; the growth and ratio identities are inherited from the realized-model lemma.

why it matters

This is the orbit-to-admissibility leg of the minimal closed-scale bridge package. Downstream, MinimalClosedScaleOrbitBridge asserts that minimal closed-scale orbit, realized closed-scale model, admissible orbit, and φ-normal form are one package; canonical_minimal_closed_scale_orbit_bridge builds that package and routes into the φ-uniform normal-form equivalence.

In the forcing chain this supports the T6 step (φ forced as the self-similar fixed point of the discrete ledger): admissible reflection supplies the exact growth-plus-constant-ratio data that the normal-form route needs. It does not itself pin φ or D=3; it only certifies that minimal closed-scale orbits already carry the reflection property required for that route.

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