cert
plain-language theorem explainer
Packages the three algebraic facts needed for the many-worlds J-cost certificate: domain cost vanishes on the diagonal, stays non-negative for positive measure and energy, and the canonical threshold is positive. Anyone citing the structural many-worlds theorem from J-cost will use this inhabited certificate. The body is a pure structure assembly from three sibling lemmas.
Claim. There is a certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module treats many-worlds branching as a J-cost phenomenon. Recognition cost is the standard RS functional $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain. Domain cost is the two-argument cost used to compare measure and energy on a branch; the certificate requires it to vanish when the two arguments coincide and to stay non-negative off the diagonal for positive inputs.
The canonical threshold is the positive cutoff that separates recognition-undetectable micro-branches from macroscopically distinct ones. In the module framing, branches multiply only when $J(\mathrm{amplitude})\ge J(\varphi)$; amplitudes below that floor are invisible to recognition.
Upstream, non-negativity of recognition-event cost is already available from ObserverForcing (cost_nonneg: every recognition event has non-negative cost via $J$-cost non-negativity).
proof idea
One-line structure construction. The three fields of ManyWorlds3Cert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No extra rewriting or case analysis.
why it matters
This is the inhabited certificate that turns the many-worlds-from-J-cost story into a zero-sorry structural theorem. The module status line marks the whole development as structural (0 sorry, 0 axiom): small-amplitude branches with $J<J(\varphi)$ are recognition-undetectable, and only branches at or above $J(\varphi)$ count as macroscopically distinct.
It sits on the foundation side of the forcing chain, using the T5 uniqueness of $J$ and the self-similar fixed point $\varphi$ (T6) as the natural amplitude floor. Downstream consumers of the certificate (e.g. inhabitedness of the cert type) can treat the three algebraic side-conditions as a single package rather than re-proving diagonal vanishing, non-negativity, and threshold positivity separately.
No open scaffold remains here; the declaration is pure packaging of already-proved sibling facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.