Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostMinimality

show as:
view Lean formalization →

The signed-strengthened native-cost uniqueness target is false: the ledger of base cost, pair terms, and signed unit (no zero field) admits a zero-flat countermodel on nonzero orbits. The module then isolates zero-calibrated hypotheses under which uniqueness holds, and shows the slim and full admissible classes coincide for the canonically selected native cost. Cite it when auditing which native-cost axioms actually force the RS cost functional.

claimThe signed-strengthened native-cost uniqueness target (base $+$ pairs $+$ signed unit, no zero field) is refuted by a zero-flat countermodel. Under zero-calibrated signed-strengthened hypotheses, uniqueness of the native cost is recovered. The slim admissible class is equivalent to the full class for the canonically selected native cost, and the constant-zero cost is excluded from the slim class.

background

Primitive Recognition Calculus treats the native cost as a functional on ledger data built from a base term, pair contributions, and optional signed or zero fields. The Recognition Composition Law and the forced $J$-cost $J(x)=(x+x^{-1})/2-1$ sit upstream in the forcing chain; here the question is which minimal axiom packages pin that cost uniquely among admissible candidates.

The parent selection module supplies the candidate native-cost classes and the canonically selected cost. This module distinguishes the signed-strengthened package (base, pairs, signed unit, deliberately omitting a zero field) from a zero-calibrated strengthening. Sibling material also compares a slim hypothesis class to the full class and records that constant-zero cost fails slim admissibility.

The module doc states the launch target is refuted: every field of the signed-strengthened ledger lives on nonzero orbits, so a zero-flat countermodel exists.

proof idea

Argument structure is refutation then repair. First, explicit countermodels refute the signed-strengthened uniqueness target and the related signed-admissible character-factorization target (zero-flat data on nonzero orbits). Case analysis on pair-two configurations and character-pair calibration reduces pair data to prime-axis calibration, showing redundancy of full prime-axis fields.

Zero-calibrated signed-strengthened hypotheses are then packaged; under them the uniqueness target is proved and shown to recover the intended native cost. Finally, slim and full admissible classes are identified for the canonically selected cost, and constant-zero is excluded from the slim class. The module is theorem-heavy, not a pure definition dump.

why it matters in Recognition Science

Native-cost uniqueness is the bridge from abstract ledger axioms to the forced $J$-cost of the Recognition forcing chain (T5). Without knowing which strengthenings work, later mass-ladder and constant derivations rest on the wrong interface.

This module clears a false target (signed-strengthened uniqueness without zero calibration) and installs the corrected zero-calibrated uniqueness theorem plus slim/full equivalence. Downstream, PRCNativeCostMinimalityCertificate imports the module to package a certificate that the selected native cost is minimal under the surviving hypotheses. That certificate is what higher PRC layers should cite rather than the refuted launch prompt.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (19)