Root-Pulse Refinement Depth

Abstract

The root-pulse chain raises and then lowers completion depth while attaining the finite-state bound.

Theorem 1.1 (Refinement depth is nonmonotone and the bound is sharp).

$$\begin{array}{c}\forall n\in \mathbb{N},3\le n\Rightarrow \\ m_{\ast }(r)=0\wedge \\ m_{\ast }(q)=n-2\wedge \\ m_{\ast }(e)=0\wedge \\ |Z_r|=1\wedge \\ |Z_q|=n\wedge \\ |Z_e|=n\wedge \\ ((\exists hr:Bool\to PUnit,r=hr\circ q)\wedge m_{\ast }(r)=0\wedge m_{\ast }(r)<m_{\ast }(q)\wedge m_{\ast }(q)=n-2)\wedge \\ ((\exists hq:\mathrm{Fin}(n)\to Bool,q=hq\circ e)\wedge m_{\ast }(q)=n-2\wedge m_{\ast }(e)=0\wedge m_{\ast }(e)<m_{\ast }(q))\wedge \\ m_{\ast }(q)=n-2\wedge \\ n-2=|\mathrm{Fin}(n)|-|\mathrm{range}(q)|.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Separation/RootPulseRefinementDepth.root_pulse_refinement_depth_counterexample (✓ std3). ∎

Source. Repository-derived.

Commentary.

For n at least three, the state carrier is Fin n and the update is truncated predecessor. The three readouts are the constant map r, the root-pulse map q, and the identity map e.

For each readout, the completion state Z is constructed as the quotient by equality of every future readout coordinate. Its depth is the repository observationStabilityDepth, the least index at which two successive finite-word relations agree.

The factorization r = hr composed with q states that q refines r; its depth rises strictly from zero to n minus two. The factorization q = hq composed with e states that e refines q; its depth falls strictly back to zero.

The imported root-pulse sharpness theorem supplies the exact middle depth. Separating future profiles identify the root-pulse and identity completion quotients with Fin n, while the constant completion is a singleton. Surjectivity of q gives a two-element range and hence equality in the finite-state bound.

References

• Truth anchor: D5/S3/Observer/Separation/RootPulseRefinementDepth.root_pulse_refinement_depth_counterexample
• Dependency: D5/S3/Observer/Separation/RootPulseSharpness