Dynamic Irrational Observer

Abstract

A dynamic irrational observer has a contractive ratio and an infinite higher jet.

Definition 1.1 (Contractive observer with an infinite jet).

Lean statement: D5/S3/Observer/Dynamics/DynamicIrrationalObserver.Observer

Formalization. D5/S3/Observer/Dynamics/DynamicIrrationalObserver.Observer (✓ std3).

Source. Repository-derived.

Commentary.

The observer records a completed value, a contraction ratio, a linear coefficient, and a genuinely infinite family of higher coefficients indexed directly by every natural number from two onward.

A thread realizes these data when the higher-order terms have the stated infinite sum at every time. This explicit HasSum relation does not silently assign a real value to a non-summable formal series.

The zeroth readout is the completed value, the first readout is the linear coefficient, and every readout from order two is the corresponding higher coefficient.

The golden first observation class is inhabited. Its completed value is the golden ratio, its contraction is minus the inverse golden ratio squared, its linear coefficient is one, and all higher coefficients vanish; the thread is the golden ratio plus the nth power of the contraction.

The source’s full-jet reconstruction sentence is not asserted as injectivity: the displayed readout sequence omits the contraction ratio, and the source gives no convergence condition for arbitrary higher coefficients.

Theorem 1.2 (The golden dynamic irrational observer exists).

$$\begin{gathered} \exists observer:Observer, \\ \mathrm{IsGoldenFirstObservationClass}\left(observer\right)\wedge \mathrm{HasThread}\left(observer,(n:\mathbb{N}\mapsto \mathrm{goldenRatio}\left(\right)+goldenProjectiveMultiplie{r}^n)\right)\wedge \\ \mathrm{readout}\left(observer,0\right)=\mathrm{goldenRatio}\left(\right)\wedge \mathrm{readout}\left(observer,1\right)=1\wedge \\ (\forall k:\mathbb{N},2\le k\Rightarrow \mathrm{readout}\left(observer,k\right)=0). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Dynamics/DynamicIrrationalObserver.exists_golden_dynamic_irrational_observer (✓ std3). ∎

Source. Repository-derived.

Commentary.

There exists an observer in the golden first-observation class with thread n mapped to the golden ratio plus the nth power of the golden projective multiplier.

Its zeroth readout is the golden ratio, its first readout is one, and every readout at an explicitly quantified order k at least two is zero.

References

• Truth anchor: D5/S3/Observer/Dynamics/DynamicIrrationalObserver.Observer
• Truth anchor: D5/S3/Observer/Dynamics/DynamicIrrationalObserver.exists_golden_dynamic_irrational_observer
• Dependency: D5/S3/CompletionDynamics/GoldenMobius/GoldenProjectiveDerivative