absValueGeneratedNativeCost_sans_sign_hypotheses
plain-language theorem explainer
The absolute-value native cost satisfies the slim sans-sign ledger: strengthened base-and-pairs axioms plus zero calibration of the doubled trace. Anyone arguing that the signed-unit field is optional will cite this as the counterexample witness. The proof is a two-field structure assembly from parent-module certificates.
Claim. The absolute-value generated native cost $F$ satisfies the slim sans-sign hypotheses: it meets the strengthened native-cost axioms (base and pairs) and its doubled-trace cost is zero-calibrated.
background
In the Primitive Recognition Calculus, native costs are maps on ratio orbits scored by a doubled J-cost (the recognition cost $J(x)=(x+x^{-1})/2-1$ from the forcing chain). The full slim ledger for uniqueness packages several fields; the sans-sign fragment drops the signed-unit constraint and keeps only strengthened hypotheses (base plus pairs) and zero calibration of the doubled trace.
PRCSlimSansSignHypotheses F is exactly that fragment: a Prop-structure with a strengthened native-cost certificate and a zero-calibration certificate for nativeCostDoubledTrace F. The absolute-value generated native cost is the candidate that ignores sign and scores by magnitude alone.
Upstream cost notions (observer J-cost, multiplicative-recognizer derived cost, rung-coarsen weighted sums) all feed the same doubled-trace scoring used here; the parent module already proves the two component certificates for the absolute-value cost.
proof idea
Term-mode structure construction. Fill strengthened by the parent certificate absValueGeneratedNativeCost_strengthened_hypotheses, and fill zero_calibrated by absValueGeneratedNativeCost_doubled_trace_zero_calibrated. No new algebra: pure assembly of two already-proved fields into PRCSlimSansSignHypotheses.
why it matters
This is the positive half of signed-unit necessity. Downstream, PRCSlimSansSignUniquenessTarget_refuted applies uniqueness of the sans-sign class to this witness and obtains that the absolute-value cost is canonical on every orbit, then contradicts the parent fact that it fails at the negative-one (signed-unit) orbit. The doc-comment states the moral: base + pairs + zero admit the absolute-value cost, so the sign field cannot be dropped.
In the Recognition framework this protects the signed structure of the native cost that sits under T5 J-uniqueness and the Recognition Composition Law: without the signed unit, the ledger is too weak to force the genuine J-cost against absolute-value impostors. It closes a minimality gap in the PRC native-cost certificate chain rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.