Pith. sign in
module module moderate

IndisputableMonolith.Physics.RenormalizationGroup2FromJCost

show as:
view Lean formalization →

Packages a domain cost built from the RS J-functional and a two-scale renormalization-group fixed-point certificate. Anyone deriving continuum thresholds or scaling fixed points from cost geometry would cite it. The file is largely definitional: nonnegativity and positivity facts plus an inhabited certificate record over Constants and Cost.

claimFrom the RS cost $J(x)=(x+x^{-1})/2-1$, define a domain cost $C$ on positive scale ratios, prove $C\ge 0$, fix a canonical positive threshold $t_*>0$, and package an inhabited two-scale RG fixed-point certificate witnessing the fixed structure induced by $J$.

background

Recognition Science forces a unique symmetric cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) via the Recognition Composition Law and the T5 uniqueness step. The Cost import supplies that functional; Constants supplies the RS-native tick $\tau_0=1$ and related units.

Renormalization here means coarse-graining scale ratios under that cost, not a QFT counterterm scheme. A domain cost is the cost evaluated on a chosen positive domain (scale window); the canonical threshold is the positive cutoff at which the cost geometry marks a fixed or matching scale.

The module sits in the Physics layer: it turns pure $J$-geometry into named objects a continuum or RG argument can quote without re-deriving nonnegativity each time.

proof idea

Definition-first module, not a deep derivation. It introduces the domain cost as a thin wrapper around $J$ on the working domain, records equality-at-evaluation and nonnegativity (inherited from $J\ge 0$ with equality at $1$), defines a canonical positive threshold, and bundles these into an RG fixed-point certificate structure with an inhabited instance. Supporting lemmas are short algebraic or positivity facts; there is no multi-step forcing argument inside the file.

why it matters in Recognition Science

Gives the Physics layer a named bridge from T5 $J$-uniqueness to two-scale RG language: domain cost, threshold, and a certificate record. Downstream graph edges are empty here, so the module is a leaf packaging step rather than a proved parent theorem. It supports later continuum, matching, or coupling-flow claims that need a cost-derived fixed-point witness without reopening the Cost API. Framework landmarks in play are T5 ($J$ unique) and the RCL that forces $J$; $\phi$-ladder mass formulas and the alpha band are not settled in this file.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)