pith. sign in
module module high

IndisputableMonolith.Foundation.RHatFixedPoint

show as:
view Lean formalization →

The RHatFixedPoint module defines contractions on finite lattices such that the J-cost strictly decreases at each iteration. Researchers analyzing fixed-point convergence in Recognition Science causal models would cite it when establishing uniqueness of minima. The module structures its results around lattice order and the J-cost properties imported from JcostCore.

claimA map $C$ on a finite lattice $L$ is a contraction when $J(C(x)) < J(x)$ for every non-fixed $x$, where $J$ denotes the J-cost function.

background

The module imports JcostCore to access the J-cost definition derived from the Recognition functional equation. It introduces Contraction as the central object together with supporting results on convergence, global minima uniqueness, and component-bounded local minima. The setting is the discrete lattice model used to study step-wise cost reduction ahead of causal propagation arguments.

proof idea

This is a definition module whose internal theorems establish contraction properties via the imported J-cost axioms. Key lemmas include contraction_converges, global_minimum_unique, and topology_creates_minima, each reducing the lattice ordering to strict J-cost decrease.

why it matters in Recognition Science

The module supplies the contraction machinery required by CausalPropagationOrdering to decide whether SpMV preserves causal ordering and whether the eight-tick octave supports multi-hop propagation. It therefore anchors the fixed-point analysis that feeds the T7 octave and downstream causal questions in the Recognition framework.

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)