cert
plain-language theorem explainer
Packages three elementary cost facts into a single no-information-loss certificate: domain cost vanishes on the diagonal, is nonnegative for positive mass and energy, and the canonical threshold is positive. Anyone citing the RS structural claim that recognition events preserve ledger information would point here. The definition is a pure structure assembly of three already-proved field lemmas.
Claim. There is a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ obeys $T>0$.
background
The module treats information preservation in Recognition Science: every recognition event is reversible because the J-cost is symmetric, $J(x)=J(1/x)$, and the ledger trace is preserved exactly. Status is structural (zero sorry, zero axiom). The black-hole section is the intended physical landing for unitary evolution.
Domain cost is the local cost functional on pairs of positive reals used to score recognition mismatch. The certificate structure RSNoInfoLossCert packages three properties: vanishing self-cost on the diagonal, nonnegativity off the identity, and a strictly positive canonical threshold. Upstream, ObserverForcing already records that the cost of any recognition event is nonnegative via $J$-cost nonnegativity.
proof idea
One-line structure instance. The three fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishes), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (threshold positivity). No extra algebra is performed at this site.
why it matters
This is the concrete witness that the no-information-loss structural theorem is inhabited. It sits under the module claim that RS proves information preservation and that recognition events are reversible via $J(x)=J(1/x)$. In the forcing chain, that symmetry is the content of T5 J-uniqueness ($J(x)=(x+x^{-1})/2-1$). The certificate is the bookkeeping object a later unitary-evolution or black-hole argument would consume. No downstream users are wired yet; the definition closes the local certificate interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.