ManyWorlds3Cert
plain-language theorem explainer
Certificate record packaging three analytic facts used by the many-worlds-from-J-cost argument: diagonal domain cost vanishes, domain cost is nonnegative on positive arguments, and the canonical threshold is positive. Downstream code builds a concrete inhabited instance from sibling lemmas. Pure structure definition with no proof body.
Claim. A many-worlds certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ equals $0$; (ii) whenever $m>0$ and $e>0$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold (the $J$-cost cutoff at $\varphi$) is strictly positive.
background
The module treats many-worlds branching as a consequence of the Recognition Science $J$-cost. Branches multiply when the cost of an amplitude exceeds $J(\varphi)$; amplitudes with $J < J(\varphi)$ stay recognition-undetectable, so only super-threshold branches are macroscopically distinct.
Domain cost is the local cost functional on a pair of positive reals (measure and amplitude scale), built from the standard $J$-cost $J(x)=(x+x^{-1})/2-1$. The canonical threshold is the positive cutoff tied to $\varphi$, the self-similar fixed point forced in the T5–T6 chain. Upstream, recognition-event cost is already known to be nonnegative via $J$-cost nonnegativity on positive states.
This structure does not re-prove those facts; it names the three interface obligations any many-worlds certificate must discharge.
proof idea
No proof: the declaration is a structure (record type). Its three fields are Prop-valued obligations. The concrete witness cert fills them by pointing at the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos; cert_inhabited then packages that witness as Nonempty.
why it matters
Gives a single named interface for the structural many-worlds claim in this module (status: structural theorem, zero sorry). Downstream, cert assembles the three sibling proofs into one certificate, and cert_inhabited records that the type is nonempty.
In the broader framework this sits under the J-uniqueness and $\varphi$-forcing landmarks (T5–T6): the threshold is the $J(\varphi)$ cutoff that separates recognition-undetectable micro-branches from macroscopically distinct ones. The certificate is the bookkeeping object that lets later arguments cite “cost vanishes on the diagonal, stays nonnegative, and the $\varphi$-threshold is positive” without reopening those lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.