Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostSelection

show as:
view Lean formalization →

Selects the canonical native cost as the J-cost with the unit orbit mapped to the literal zero representative. That object is the non-vacuity witness for the full zero-calibrated prime-signed strengthened hypothesis class. The module also builds the constant-zero and linear decoys and proves they fail the native hypotheses, so the selection is not vacuous. Downstream minimality arguments cite this witness as the concrete cost that survives.

claimThe module fixes a canonical selected native cost $C_\star$: the Recognition $J$-cost with the unit orbit sent to the literal zero representative. It records that $C_\star$ satisfies the native and full zero-calibrated prime-signed strengthened hypotheses, and that the constant-zero and linear candidates fail those hypotheses and are therefore excluded.

background

In the Primitive Recognition Calculus, a native cost is a real-valued functional on the positive ratio orbit that obeys the Recognition Composition Law and the zero-calibration / prime-signed strengthenings used in the forcing chain. The classical $J$-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) is the unique continuous solution forced at T5; here the module works at the discrete native level before continuum extension.

PublicSpine supplies the dual $\delta$-stratified forcing surface (the public counterpart of UnifiedForcingChain): the $\delta$-only tower lives over $\mathbb{N}/\mathbb{Z}/\mathbb{Q}$, with continuum cut deferred to classicalExtension. PRCNativeCostUniqueness is the immediate upstream uniqueness layer this selection sits on.

The module's job is selection plus non-vacuity: name one concrete cost that meets the full hypothesis package, and exhibit standard decoys (constant zero, linear) that do not.

proof idea

Definition-first module. It introduces canonicalSelectedNativeCost as the $J$-cost with unit-orbit zero representative, then packages conversion-to-rationals, cross-equation on the ratio orbit, and the native / full hypothesis bundles as lemmas about that object. Parallel definitions constantZeroNativeCost and linearNativeCost are shown not to satisfy the native hypotheses and are excluded. A strengthened zero-flat prime-signed hypothesis bundle is recorded for the selected cost. No deep new uniqueness proof lives here; uniqueness is imported, selection and exclusion are local.

why it matters in Recognition Science

Without an explicit selected witness, the native-cost hypothesis class could be empty and every uniqueness or minimality theorem would be vacuous. This module closes that gap: the canonical $J$-cost with literal zero on the unit orbit is the non-vacuity witness for the full zero-calibrated prime-signed strengthened class. PRCNativeCostMinimality imports the module and uses that witness as the concrete cost against which minimality is stated. In the broader RS chain this sits under T5 $J$-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, feeding the public $\delta$-spine rather than replacing UnifiedForcingChain.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (22)