Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum.ForcedJOnCompletion

show as:
view Lean formalization →

Once the continuum completion $R_\delta$ is admitted, the recognition cost on its multiplicative group is forced to the unique $J$-formula. The module packages existence of the null-distance Cauchy completion, one-point calibration of characters, and propagation to the full cyclic subgroup. Anyone citing T5-style $J$-uniqueness on the completed reals uses this layer. The argument chains character rigidity with native cost uniqueness on ordered fields.

claimLet $R_\delta$ be the null-distance quotient of Cauchy ledgers (the continuum completion). There exists a recognition cost on the multiplicative structure of $R_\delta$ that coincides with $J(x)=(x+x^{-1})/2-1$. One-point calibration of a character forces this identity on the cyclic subgroup it generates, and hence the canonical cost on the completion is $J$.

background

Recognition Science treats cost as a functional on a multiplicative group obeying the Recognition Composition Law. On discrete or field carriers the native cost is already unique up to the $J$-formula $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The continuum is not forced by distinction alone; that non-nativity is recorded elsewhere. This module makes the named commitment that, once a completion is chosen, the cost on it is still forced.

The carrier is the null-distance quotient of Cauchy ledgers. Addition and negation are closed and congruent on that quotient. Multiplication, order, and completeness are reduced to named exact targets rather than fully discharged here. Upstream modules supply cost-on-field structure, real complete ordered field scaffolding, native cost uniqueness, and character rigidity forcing.

Sibling results include existence of the completion, the canonical cost matching the $J$-formula, reciprocal symmetry, generated-cost formulae, and the statement that a calibrated character forces $J$ after propagation along its cyclic subgroup.

proof idea

The module is a continuum forcing layer, not a single theorem. It first records that the completion $R_\delta$ exists with conditional field structure on the null-distance Cauchy quotient. It then imports character rigidity: a one-point calibration of a multiplicative character determines the cost on the cyclic subgroup that character generates. Native cost uniqueness on ordered fields identifies that determined cost with the closed-form $J$. The top-level forced-$J$-on-completion statements assemble these pieces: existence of a cost on the completion, plus identity with $J$ after calibration propagates. Several siblings are thin wrappers or algebraic reductions around those two ingredients.

why it matters in Recognition Science

This is the continuum half of T5-style $J$-uniqueness inside Primitive Recognition Calculus. Discrete and field carriers already force $J$; without this module the completed real line would be a gap where another cost might hide. Downstream work that needs a unique cost on $\mathbb{R}_{>0}$ (mass ladder, coupling constants, continuum limits of ledger dynamics) depends on the forced identity assembled here.

The module also makes the philosophical boundary explicit: the continuum is a commitment, not a distinction theorem, yet once committed the cost cannot float. That separation keeps the forcing chain honest while still delivering $J(x)=(x+x^{-1})/2-1$ on the completed carrier. No used-by edges are recorded yet; the natural parents are global uniqueness and continuum physics interfaces that quote forced cost on $R_\delta$.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (9)