pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.RHatFixedPoint

show as:
view Lean formalization →

The module defines contractions on finite lattices where the J-cost strictly decreases at each step and proves convergence to a unique global minimum fixed point. Recognition Science researchers cite it when tracing causal propagation through the phi-ladder and eight-tick octave. The argument imports J-cost algebraic identities from JcostCore and applies them to lattice maps via repeated strict decrease and finiteness.

claimLet $C$ be a contraction on a finite lattice $L$ with J-cost $J$. Then $J(C(x)) < J(x)$ for $x$ not the fixed point, the iteration converges, and the limit is the unique global minimum of $J$.

background

The module sits in the Foundation layer and imports JcostCore, which supplies the J-cost function $J(x) = (x + x^{-1})/2 - 1$ together with the Recognition Composition Law. A contraction is a map on the lattice that reduces this cost strictly at every non-fixed point. The setting uses the self-similar fixed point phi forced at T6 of the UnifiedForcingChain and prepares results for the eight-tick octave at T7.

proof idea

The module first introduces the Contraction predicate. It proves contraction_converges by showing that strict J-cost decrease on a finite set must terminate. global_minimum_unique and fixed_point_is_minimum then follow by applying the algebraic identities from JcostCore to the limit point, confirming it achieves the global minimum.

why it matters in Recognition Science

The results feed directly into CausalPropagationOrdering, which uses them to check whether SpMV propagation preserves causal order and whether the eight-tick octave suffices for multi-hop propagation. The module closes the fixed-point step between T6 (phi) and T7 (octave) in the forcing chain and supplies the uniqueness needed for deterministic derivation of D = 3.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)