Pith. sign in
module module high

IndisputableMonolith.Foundation.RHatFixedPoint

show as:
view Lean formalization →

The module establishes that a contraction on a finite lattice strictly decreases J-cost at each step. Researchers studying convergence in discrete recognition models cite it to guarantee unique minima. The structure imports J-cost definitions and builds the decrease property from the core recognition composition law.

claimLet $L$ be a finite lattice and $f:L o L$ a contraction. Then $J(f(x))<J(x)$ for all $x$ not the global minimum, where $J$ is the J-cost satisfying the recognition composition law.

background

The module resides in the Foundation domain and imports JcostCore, which defines the J-cost via the recognition composition law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. It introduces contractions as maps on finite lattices that reduce this cost strictly per step. The setting concerns fixed-point behavior on discrete structures prior to causal ordering arguments.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the contraction property to CausalPropagationOrdering, which examines whether SpMV propagation preserves causal ordering and whether the eight-tick octave suffices for multi-hop propagation. It supports the forcing chain by ensuring J-cost minima are reached on finite lattices.

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)