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

IndisputableMonolith.Foundation.RHatFromJCostGradient

show as:
view Lean formalization →

The module introduces the midpoint map as the linear contraction x maps to (x+1)/2 with fixed point at 1, supplying the discrete step that decreases J-cost. Researchers deriving the recognition hat from cost minimization in the Recognition Science chain would cite it. The argument rests on algebraic verification of the contraction property together with fixed-point and Lyapunov lemmas.

claimThe midpoint map $m(x) = (x + 1)/2$ is a linear contraction toward the fixed point 1 that decreases the J-cost.

background

Recognition Science derives physics from the J-cost functional whose level sets encode deviation from self-similarity. The midpoint map supplies a canonical discrete gradient step on that landscape. The Constants module fixes the RS time quantum at one tick; the Cost module supplies the J-cost definition and its composition law.

proof idea

This is a definition module. It contains the midpoint map definition together with sibling lemmas that verify the fixed point at 1 and the strict decrease of J-cost under iteration.

why it matters in Recognition Science

The contraction supplies the mechanism that certifies RHat emergence from the J-cost gradient. It feeds the RHatEmergenceCert and rHatEmergenceCert siblings and closes the step from J-uniqueness to the recognition structure in the forcing chain.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)