Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCChainBridge

show as:
view Lean formalization →

Bridge module linking the Recognition Science cost functional to the Primitive Recognition Calculus chain. It records that J-cost in log coordinates is the unit-curvature member of the δ-forced family, J(e^t)=cosh(t)-1, places φ in the minimal field, and shows every RS-chain rung lives in that field. Downstream certificate modules import it to shrink the formal footprint of the forcing chain.

claimIn log coordinates the Recognition cost satisfies $J(e^t)=\cosh(t)-1$, i.e. the $c=1$ member of the $\delta$-forced cost family. The golden ratio $\varphi$ lies in the PRC minimal field, the $\delta$-cost feeds the RS forcing chain, and every rung of that chain is an element of the same field.

background

Recognition Science forces a unique nonnegative cost $J$ on ratios by the Recognition Composition Law and normalization; the closed form is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$ (forcing step T5). Working in the additive coordinate $t=\log x$ therefore yields $J(e^t)=\cosh(t)-1$, the curvature-$c=1$ slice of the one-parameter family of hyperbolic costs.

Primitive Recognition Calculus (PRC) isolates a minimal ordered field large enough to host the self-similar fixed point $\varphi$ and the discrete rungs of the RS ladder. Calibration targets fix the numerical identification between the abstract $\delta$-cost and the concrete $J$-cost used elsewhere in the monolith.

This module sits between those two layers: it imports the global Cost API, the PRC calibration target, and the PRC minimal-field construction, then exports the equalities and membership facts needed by later certificate modules.

proof idea

The module is a thin bridge, not a long development. Sibling lemmas equate the log-coordinate $J$-cost to the $c=1$ hyperbolic cost (direct expansion of $\cosh$), record the matching second-derivative (curvature) identity at the origin, prove $\varphi$ inhabits the PRC minimal field, and discharge the two chain-level claims that the $\delta$-cost feeds the RS forcing sequence and that every rung of that sequence remains inside the field. Each fact is a short algebraic or membership argument; no deep tactic search is required.

why it matters in Recognition Science

Without the log-coordinate identification $J(e^t)=\cosh(t)-1$, the PRC cost calculus cannot be glued to the T5 uniqueness theorem that forces $J$ globally. Placing $\varphi$ and all RS rungs inside the minimal field lets later modules reason about the entire forcing chain (T5–T8 and the mass ladder) inside a single small carrier, which is exactly what PRCShrunkCertificate imports this module to obtain. The bridge therefore shrinks the trusted base of the Recognition formalization while preserving the link from the abstract $\delta$-family to the concrete constants $c=1$, $\hbar=\varphi^{-5}$, and the eight-tick octave.

scope and limits

used by (1)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (5)