Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.Continuum.ForcedJOnCompletion

show as:
view Lean formalization →

Constructs the continuum completion R_δ of the primitive recognition calculus and proves that any calibrated cost on it is forced to the unique J-cost. The continuum is an explicit commitment, not forced by distinction alone; once admitted, the carrier is the null-distance quotient of Cauchy ledgers. Foundation readers cite the forced-J and one-point calibration results. The argument chains completion existence to character rigidity and native cost uniqueness.

claimThe completion $R_\delta$ exists as the null-distance quotient of Cauchy ledgers, with conditional field structure. On $R_\delta$, any calibrated recognition cost equals the unique formula $J(x)=(x+x^{-1})/2-1$. One-point calibration propagates to cyclic subgroups and yields the global identity of the cost with $J$.

background

Primitive Recognition Calculus (PRC) works first on discrete ledgers and field-level cost data before any continuum is assumed. The J-cost is the unique symmetric cost solving the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$. Native cost uniqueness and cost-on-field infrastructure supply the algebraic skeleton; character rigidity supplies the analytic pin that a calibrated multiplicative character cannot deviate from J.

The module's named commitment is that the real line is not forced by distinction alone (cf. RealLineNonNativity). Once the continuum is admitted, the carrier is PRCRealNullClosed: Cauchy ledgers modulo null distance. Addition and negation are proved closed and congruent; multiplication, order, and completeness are reduced to named exact targets rather than smuggled in as axioms.

RealCompleteOrderedField and CharacterRigidityForcing set the ambient ordered-field and rigidity language used throughout.

proof idea

Module-level argument, not a single proof. First, existence of the completion $R_\delta$ with conditional field structure (addition/negation closed; other operations as named targets). Next, the canonical cost on the completion is identified with the J formula and shown reciprocal-symmetric; a generated-cost formula records how costs extend from generators. Character rigidity then forces any calibrated character to J. Calibration at one point propagates along cyclic subgroups, yielding the global identity of the cost with J on the completion and existence of the forced cost. Downstream packaging theorems assemble these into the forced-J-on-completion statement.

why it matters in Recognition Science

Closes the continuum step of J-forcing in the PRC foundation: once $R_\delta$ is admitted, T5-style J-uniqueness holds on the completion, not only on discrete or field fragments. Sibling results (forced J on completion, forced cost exists, global identity from one-point calibration) are the concrete landing points. No downstream used_by edges are recorded yet; the module is a leaf supplier for continuum-level Recognition Composition Law and cost uniqueness arguments. It makes explicit that continuum structure is a commitment with named exact targets, not a free gift of distinction, which keeps the forcing chain honest relative to RealLineNonNativity.

scope and limits

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (9)