J
plain-language theorem explainer
J is the strain or cost functional on states in the Reality Recognition Framework. Modelers of recognition processes and strain minimization cite it as the canonical cost measure. The definition is a one-line abbreviation that projects the J component from any StrainFunctional record.
Claim. Let $J(S)$ denote the strain functional on a state $S$, where $S$ is an instance of the strain functional type.
background
The RRF Core Glossary module supplies the single source of truth for vocabulary in the Reality Recognition Framework. J stands for the strain/cost functional, with the explicit convention that strain vanishes at balance. Upstream results include the inflaton potential defined as $V(φ_inf) = J(1 + φ_inf)$ and the full ILG action that incorporates analogous cost terms.
proof idea
One-line abbreviation that extracts the J field from the StrainFunctional record.
why it matters
This definition supplies the standard notation for the cost measure that appears throughout RRF derivations, including the law that J approaches zero at equilibrium. It supports consistent use in models of the forcing chain and phi-ladder structures. No downstream theorems are listed for this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.