slimLedgerMinimalityCertificate_holds
plain-language theorem explainer
The slim ledger forces the canonical J-cost, and each of its four removable calibration fields is necessary: drop any one and a kernel-checked impostor appears. Anyone citing field-by-field minimality of the native recognition cost (round-2 uniqueness) uses this certificate. The proof is pure structure assembly of one uniqueness theorem and four refuted uniqueness targets.
Claim. There is a field-by-field minimality certificate for the slim ledger: under zero-calibrated signed strengthened native cost data the cost is unique (the canonical $J$), and uniqueness fails if one drops the two-point anchor, the pair field, the signed unit, or the zero orbit.
background
In Recognition Science the native cost on positive ratios is the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$, forced under the Recognition Composition Law (forcing-chain T5). The Primitive Recognition Calculus packages a slim ledger of discrete calibration data on ratio orbits: a two-point anchor, a pair field, a signed unit, and a zero orbit. Together these pin the cost to canonical $J$.
The certificate structure asserts both uniqueness under the full slim ledger and necessity of each removable field. Necessity is witnessed by explicit impostors named in the structure documentation: Liouville twist, two-adic twist, absolute-value cost, and zero-flat cost respectively. Cost domains and displays stay on discrete ratio-orbit arithmetic; no continuum carrier or continuity premise enters.
Direct inputs are the proved zero-calibrated signed strengthened native-cost uniqueness target and the four refuted "slim sans field" uniqueness targets.
proof idea
Term-mode structure constructor with no new algebra. Slim uniqueness is filled by the already-proved zero-calibrated signed strengthened native-cost uniqueness target. The four necessity fields are filled by the corresponding refuted uniqueness targets: slim-without-two-point-calibration, slim-without-pair, slim-without-sign, and signed-strengthened uniqueness without the zero orbit. The certificate only packages those five prior results.
why it matters
This is the raw deposit that the public-spine tag theorem wraps under the discrete-only strength tag, recording that all cost domains and codomains are ratio orbits, display arithmetic is discrete, witnesses are arithmetically explicit, and no completed carrier or continuity premise appears. It closes field-by-field minimality for the slim ledger in the Primitive Recognition Calculus and supports the T5 J-uniqueness landmark: canonical $J$ is forced, and each calibration knob is load-bearing. Downstream consumers of the native-cost minimality spine cite the tagged certificate rather than the raw fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.