cert
plain-language theorem explainer
Packages three elementary facts about the RS superposition domain cost into a single certificate: the cost vanishes on equal nonzero amplitudes, stays nonnegative for positive amplitudes, and the canonical threshold is positive. Anyone needing a SuperpositionCostCert instance cites this. The body is a pure structure assembly of three already-proved sibling lemmas.
Claim. There is a certificate recording that the superposition domain cost $C$ satisfies $C(r,r)=0$ for every nonzero real $r$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical threshold $T$ obeys $T>0$.
background
In Recognition Science the J-cost of a two-level superposition $\psi=\alpha|0\rangle+\beta|1\rangle$ is taken to be $J(|\alpha|/|\beta|)$, where $J$ is the unique nonnegative cost forced by the Recognition Composition Law (T5: $J(x)=(x+x^{-1})/2-1$). Equal amplitudes give ratio $1$, and $J(1)=0$, so a maximally coherent equal superposition sits at the global cost minimum.
This module formalizes that picture via a domain cost $C(m,e)$ on positive amplitude magnitudes, together with a positive canonical threshold used as a recognition cutoff. The certificate structure bundles the three structural properties needed downstream: vanishing on the diagonal, nonnegativity off it, and positivity of the threshold.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing (cost_nonneg: every recognition event has nonnegative J-cost).
proof idea
One-line structure construction. The three fields of SuperpositionCostCert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No new calculation occurs here.
why it matters
Gives a single named inhabitant of the superposition-cost certificate used as the module's structural anchor. The module doc marks the development as a structural theorem (zero sorry, zero axiom): equal superposition has zero recognition cost, matching the J-minimum at ratio $1$.
No downstream consumers are wired yet in the graph, so the certificate presently stands as the export surface of Superposition_Cost_RS rather than a lemma inside a larger forcing step. It sits in Foundation beside ObserverForcing and the J-uniqueness chain (T5), ready for any later argument that needs a packaged witness that coherent equal superpositions are cost-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.