Pith. sign in
module module high

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostSelection

show as:
view Lean formalization →

Selects the canonical native recognition cost as the J-cost with the unit orbit sent to the literal zero representative. It is the non-vacuity witness for the full zero-calibrated prime-signed strengthened hypothesis class, and it excludes constant-zero and linear competitors. Minimality arguments import this selection. The module is definition-and-exclusion packaging, not a deep derivation.

claimThe module fixes the canonical selected native cost as the J-cost with the unit orbit mapped to the literal zero representative, records that this cost satisfies the native and full zero-calibrated prime-signed strengthened hypothesis packages, and proves that the constant-zero and linear candidates fail those packages (hence are excluded).

background

In Recognition Science the cost functional is forced by the Recognition Composition Law and J-uniqueness (T5): $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. Native-cost selection sits in the Primitive Recognition Calculus layer after uniqueness and before minimality.

PublicSpine is the public dual of UnifiedForcingChain: a $\delta$-stratified forcing surface (tower on $\mathbb{N}/\mathbb{Z}/\mathbb{Q}$, continuum cut via classical extension). This module takes the unique J-shape and chooses the zero-calibrated representative on the unit orbit so the strengthened prime-signed class is non-vacuous.

Sibling objects include the canonical selected cost, its rational restriction and cross-equation on the ratio orbit, the native and full hypothesis bundles it meets, and the constant-zero and linear counter-candidates with their exclusion lemmas.

proof idea

Definition-and-witness module, not a multi-step derivation. It introduces the canonical selected native cost as $J$ with unit-orbit zero, packages the native and full hypothesis records that cost satisfies, and discharges exclusion lemmas for constant-zero and linear costs by showing they fail the native hypothesis package. Negative checks are elementary failures of the stated hypotheses; positive content is selection and packaging that feed the minimality layer.

why it matters in Recognition Science

Feeds PRCNativeCostMinimality, which imports this module for a concrete zero-calibrated witness and the excluded competitors. Closes non-vacuity for the full zero-calibrated prime-signed strengthened class after PRCNativeCostUniqueness. Ties directly to T5 J-uniqueness and the RCL: once $J$ is unique up to calibration, sending the unit orbit to the literal zero representative is the natural normalization before proving minimality among native costs. Without this selection, the strengthened hypothesis class could be empty and minimality would have no witness.

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)