Pith. sign in
module module high

IndisputableMonolith.Foundation.RHatFromJCostGradient

show as:
view Lean formalization →

The module introduces the midpoint map as a linear contraction toward 1 to support J-cost analysis in Recognition Science. Researchers studying fixed-point emergence and Lyapunov behavior in cost functions would cite its sibling declarations for establishing contraction and uniqueness results. The module structure consists of direct definitions and algebraic verifications that rely on the imported Cost and Constants modules.

claimThe midpoint map defined by $m(x) = \frac{x + 1}{2}$ is a linear contraction toward 1.

background

The module imports the fundamental RS time quantum $\tau_0 = 1$ tick from Constants. It draws on the Cost module for J-cost definitions and gradient analysis. The supplied doc-comment states that the midpoint map $x \mapsto (x + 1)/2$ is a linear contraction toward 1, providing the core object for subsequent fixed-point and Lyapunov results listed among the siblings.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supports derivation of RHat from the J-cost gradient by supplying the contraction map and its fixed-point certificates. It feeds the sibling results on midpointMap_fixed_point, midpointMap_decreases_jcost, and jcost_lyapunov_unique_fixed_point that in turn enable RHatEmergenceCert.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (6)