PRCSlimSansRclUniquenessTarget_refuted
plain-language theorem explainer
Uniqueness of the canonical native cost fails if the slim ledger drops the nonzero Recognition Composition Law: the rational 5-spike is a kernel-checked impostor. Cited by the slim-ledger minimality certificate to show the RCL field is necessary, not optional. Proof feeds the uniqueness hypothesis the 5-spike witness and invokes non-canonicity of that spike.
Claim. It is not the case that every map $F$ on ratio orbits satisfying the slim hypotheses without the nonzero Recognition Composition Law agrees with the canonical native cost on every ratio orbit (in the cross-equality sense). Equivalently, the sans-RCL uniqueness target is false.
background
The Primitive Recognition Calculus (PRC) studies cost maps on ratio orbits: discrete multiplicative data that carry the native recognition cost. The canonical display is the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced in the unified chain by T5 and the Recognition Composition Law (RCL) $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
The slim ledger is a minimal hypothesis package that still forces this canonical cost. Its removable calibration fields are tested one at a time: drop a field, and an explicit impostor should appear. The sans-RCL uniqueness target asserts that every $F$ obeying the slim package without the nonzero RCL still matches the canonical native cost on every orbit.
Local setting is the PRC native-cost minimality certificate module: field-by-field necessity for the slim ledger, with discrete RatioOrbit arithmetic and no continuum premises in the witnesses.
proof idea
Term-mode reductio. Assume the sans-RCL uniqueness target. Instantiate it at the native 5-spike cost map, using the lemma that this map satisfies the slim-sans-RCL hypotheses, and evaluate on the ratio orbit of the rational $5$. The resulting cross-equality would force the 5-spike to be canonical. Discharge by the already-proved fact that the 5-spike native cost is not canonical. No further case analysis.
why it matters
Closes the RCL-core necessity bonus in the slim-ledger certificate: dropping the nonzero RCL admits the 5-spike, so RCL cannot be removed from the minimal package. Downstream, slim_ledger_minimality_certificate_tagged deposits the full field-by-field certificate (canonical J forced; each removable calibration field necessary via an explicit impostor). That certificate is tagged deltaOnly: discrete ratio-orbit domains, arithmetically explicit witnesses, no completed carrier or continuity premise.
Framework landmark: RCL is the functional equation that forces J-uniqueness (T5) in the forcing chain. Showing the slim package without RCL fails uniqueness ties the ledger certificate directly to that chain step, rather than treating RCL as decorative calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.