additive_posting_of_realized_closed_scale
plain-language theorem explainer
In a closed observable framework, if an orbit realizes a closed geometric scale sequence then the observable on the second iterate of the base state equals the sum of the observables on the first and zeroth iterates. Researchers deriving the realized hierarchy interface from scale primitives cite this result. The short tactic proof extracts the additive closure of the scale values at steps 0-1-2, rewrites via the realization map, and finishes with ring arithmetic.
Claim. Let $F$ be a closed observable framework and let $H$ be a realized closed scale model for $F$. Then the observable satisfies $F.r(F.T^{[2]} H.baseState) = F.r(F.T^{[1]} H.baseState) + F.r(F.T^{[0]} H.baseState)$.
background
A ClosedObservableFramework consists of a state space $S$, transition map $T$, and positive observable $r$ obeying nontriviality together with closure and finite description. A RealizedClosedScaleModel for such an $F$ packages a base state, positive amplitude, a GeometricScaleSequence whose values are closed under ledgerCompose, and the realization map equating $F.r$ on each iterated state to amplitude times the corresponding scale value. The module isolates the strongest derivation currently available: once a closed scale sequence is realized, both ratio_self_similar and additive_posting become theorems rather than assumptions. Upstream, the ClosedObservableFramework encodes the three conditions of non-trivial observability, closure with no external input, and finite description with countable states and no continuous moduli.
proof idea
The tactic proof first applies simpa to the scales_closed field using GeometricScaleSequence.isClosed and ledgerCompose to obtain scale 0 plus scale 1 equals scale 2. A linarith step symmetrizes the equality. It then rewrites the three instances of the realize map at steps 2, 1 and 0, substitutes the additive relation on the scales, and closes with ring.
why it matters
This theorem supplies the additive_posting field required by the toRealizedHierarchy construction that packages the closed-scale model into the full RealizedHierarchy interface. It fills the derivation step described in the module documentation, where closure of the geometric scale sequence makes additive posting a theorem rather than an assumption. The remaining open question is proving existence of such a realized closed scale model from the ClosedObservableFramework axioms alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.