BornRuleDerivationCert
plain-language theorem explainer
Packages the two-outcome Born rule as an axiom-free verification certificate: when squared complex amplitudes match the geometric cos²/sin² of a two-branch rotation and sum to one, recognition-cost probabilities equal those squares. Citation target for anyone wiring the derived Born rule into the verification layer. The accompanying verified predicate is discharged by a one-line wrapper around the upstream Born-rule theorem.
Claim. A Born-rule derivation certificate is verified when the following holds: for all complex amplitudes $\alpha_1,\alpha_2$ and every two-branch rotation with starting angle $\theta_s$, if $\|\alpha_1\|^2+\|\alpha_2\|^2=1$, $\|\alpha_1\|^2=\cos^2\theta_s$, and $\|\alpha_2\|^2=\sin^2\theta_s$, then there exists a two-outcome measurement (built from nonnegative recognition costs) whose outcome probabilities equal $\|\alpha_1\|^2$ and $\|\alpha_2\|^2$ respectively. Every such certificate is verified.
background
The module packages the two-outcome Born rule from the measurement layer without hidden typeclass axioms. A two-branch rotation is a geometric measurement path fixed by a starting angle $\theta_s\in(0,\pi/2)$ and a positive duration; its geometric amplitudes are $\sin^2\theta_s$ (initial) and $\cos^2\theta_s$ (complement). A two-outcome measurement is a pair of nonnegative recognition costs $C_1,C_2$ whose normalized weights define the outcome probabilities.
Upstream, born_rule_from_C states that whenever the squared norms of complex amplitudes match those geometric amplitudes and sum to one, there exists such a measurement whose probabilities equal the squared norms. The certificate simply freezes that statement into a Prop-valued verified flag on a unit structure, so downstream verification code can assert the Born-rule claim without importing measurement internals.
proof idea
The structure itself is empty (only Repr). The verified predicate is the universal closure of the Born-rule statement: quantify over amplitudes and a two-branch rotation, assume normalization and matching to complement/initial amplitude squares, and demand existence of a two-outcome measurement with matching probabilities.
verified_any is a one-line wrapper: introduce the hypotheses and apply born_rule_from_C with the same amplitudes, rotation, and matching equalities. No extra algebra.
why it matters
Places the derived two-outcome Born rule into the verification certificate layer so the claim can be checked as a closed Prop without measurement-layer typeclass baggage. The module doc states the intent explicitly: package the statement from Measurement.BornRule axiom-free, with probabilities matching quantum amplitude squares once the geometric cos²/sin² match is given.
No downstream consumers are wired yet (used_by is empty); the certificate is a leaf ready for higher-level audit bundles. In the Recognition framework it records that Born probabilities are not postulated but recovered from recognition costs along a two-branch geodesic, once amplitudes are identified with the rotation geometry. It does not touch the forcing chain (T0–T8) or the RCL directly; it sits in the measurement/verification bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.