SuperpositionCostCert
plain-language theorem explainer
Certificate structure bundling three properties of RS superposition cost: equal-amplitude pairs have vanishing domain cost, domain cost is nonnegative on positive reals, and the canonical threshold is positive. Downstream code cites it via the inhabited witness `cert`. Pure structure definition with no proof body; the three fields are the mathematical content.
Claim. A superposition-cost certificate is a triple of facts: (i) for every nonzero real $r$, the domain cost of the equal pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
In this module the recognition cost of a two-level superposition $\psi=\alpha|0\rangle+\beta|1\rangle$ is the $J$-cost of the amplitude ratio, $J(|\alpha|/|\beta|)$. The unique minimum of $J$ sits at argument $1$, so equal superposition ($|\alpha|=|\beta|$) has zero recognition cost and is called maximally coherent.
The domain cost is the concrete real-valued function implementing that $J$-cost on positive pairs. The canonical threshold is the positive cutoff used to separate free (zero-cost) coherent states from costly unbalanced ones. Upstream, ObserverForcing already records that every recognition-event cost is nonnegative via $J$-cost nonnegativity on positive states.
The local status line marks the module as a structural theorem: zero sorry, zero axioms.
proof idea
No proof body: this is a structure whose three fields are propositions. Inhabitation is deferred to the sibling definition that fills the fields with domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. The structure itself only names the interface.
why it matters
Packages the three algebraic facts needed to treat equal superposition as the zero-cost coherent state in RS. Downstream, the module builds a concrete inhabitant and proves the type is nonempty, so later foundation lemmas can assume a single certificate rather than three separate lemmas.
Framework link: $J(1)=0$ is the minimum forced by T5 $J$-uniqueness ($J(x)=(x+x^{-1})/2-1$). The certificate therefore records, in Lean, that maximally coherent states sit at that forced minimum and that the threshold used to gate costly superpositions is positive. It does not yet derive measurement or Born-rule weights; it only locks the cost geometry those arguments will use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.