prc_native_cost_uniqueness_blocker_certificate
plain-language theorem explainer
Packages the Pass-25 status of native cost uniqueness in the Primitive Recognition Calculus: which factorization, rigidity, calibration, and orientation targets are proved versus refuted. Anyone tracking closure of the unique native cost (the discrete precursor of J) would cite it. The proof is a structure assembly that wires named sub-theorems, refutations, and definitional equalities (many by rfl).
Claim. There is a blocker certificate for uniqueness of the native recognition cost on rational orbits: zero-calibrated character factorization holds; the signed-admissible zero-calibrated factorization and the zero-calibration-to-signed-unit implication are refuted; the prime-signed strengthened factorization and uniqueness targets hold; the older (unsigned) factorization and rigidity targets are refuted; two-to-prime and prime-propagation calibration targets are refuted; global orientation from prime calibration is refuted; and the reciprocal-twist / two-prime branch-control coherence identities for ratio characters hold as stated.
background
In the Primitive Recognition Calculus, costs live on ratio orbits: integer numerators over nonzero orbit denominators (RatioOrbit). A ratio character is a multiplicative map on those orbits that fixes the unit; the identity map is the sanity-check character and is rigid against the canonical on-orbit cost. Cost-from-character recovers a native cost functional from any such character.
Native cost uniqueness asks whether every admissible character yields the same cost (up to the cross-equality relation on orbits). The module splits that question into exact Lean targets: zero-calibrated factorization, signed-admissible variants, prime-signed strengthenings, rigidity, and orientation/calibration propagation from the prime 2. Upstream lemmas establish that the identity character is globally oriented, prime-orientation coherent, and rigid, and that normalized ratios are sign-canonical.
The local setting is a certificate layer: rather than a single closed uniqueness theorem, the development records precisely which sub-targets are proved and which candidate routes are refuted, so the remaining gap is explicit.
proof idea
Tactic-mode structure constructor for PRCNativeCostUniquenessBlockerCertificate. Each field is discharged by a named prior result or by rfl:
- Factorization and uniqueness slots cite the corresponding proved or refuted target theorems (zero-calibrated factorization proved; signed-admissible and old factorization refuted; prime-signed strengthened factorization and uniqueness proved; zero-calibrated uniqueness and old rigidity refuted; signed-admissible rigidity proved).
- Calibration/orientation blockers cite the two-to-prime, prime-propagation, and global-orientation refutations.
- Coherence and two-orbit/prime direction fields are definitional (rfl) or the twoOrbit_primeOrbit fact.
- Reciprocal-twist fields introduce a character and apply PRCRatioCharacter.reciprocalTwist and the prime-calibrated / identity-iff-reciprocal family.
- Two-prime branch-control and prime-identity force fields apply the of_coherent / of_local_* / iff_* lemmas that relate local two-prime control, orientation coherence, and reciprocal exclusion.
No new analytic argument appears here; the certificate only aggregates already-proved pieces.
why it matters
Native cost uniqueness is the discrete gate in front of J-uniqueness (forcing-chain T5): the continuous cost J(x)=(x+x^{-1})/2-1 is forced only after the native character-to-cost map is unique under the admissible hypotheses. This certificate does not close that gate; it records that several naive routes (unsigned factorization, zero-calibration forcing signed units, two-to-prime propagation, global orientation from primes) are refuted, while zero-calibrated factorization, prime-signed strengthened uniqueness, and signed-admissible rigidity stand.
Downstream it feeds prc_universal_foundation_conditional_certificate in UniversalFoundation, which bundles kernel, real-complete ordered field, and trace-logic certificates into the conditional universal foundation. The blocker therefore keeps the foundation honest: uniqueness remains conditional on the remaining open targets named inside the structure, not silently assumed.
For the broader RS program this is bookkeeping that matters: RCL and the phi fixed point sit above a unique cost; Pass-25 makes the missing mathematics machine-checkable rather than narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.