born_from_TruthCore
plain-language theorem explainer
Born-rule compliance for two-outcome recognition paths is a theorem, not a hypothesis: normalized path weights equal cos²/sin² on every two-branch rotation. Anyone assembling the dimensionless inevitability pack or an honest-closure certificate cites this fact. The proof is a one-line discharge of the empty certificate via the existing verified_any lemma.
Claim. The Born-rule compliance proposition holds: for every two-branch rotation, the normalized two-outcome recognition probabilities equal $\cos^2$ and $\sin^2$ of the branch angle.
background
In RecogSpec, physical claims are packaged as named propositions that a certificate structure can discharge. The Born-rule slot is the proposition that recognition path weights reproduce Born probabilities. Concretely it is defined as the verification predicate of an empty TwoOutcomeBornCert: for every two-branch rotation, the two normalized outcome weights match $\cos^2/\sin^2$.
That certificate lives in the TwoOutcomeBorn verification module and is the only Born content required at the RecogSpec layer. Upstream, the same module supplies a universal witness verified_any that proves the predicate for the empty certificate, so no extra calibration data is needed. The surrounding Spec module also packages speed, units, bands, and calibration witnesses; Born compliance is the quantum-measurement leg of that pack.
proof idea
One-line term proof. The goal is exactly TwoOutcomeBornCert.verified {}. Apply TwoOutcomeBornCert.verified_any to the empty certificate value {}; that lemma already establishes the universal quantification over two-branch rotations. No local algebra or case split is required.
why it matters
Born compliance is one of the named legs of the dimensionless inevitability scaffold: inevitability_dimless_holds conjoins matches-eval, $k$-gate, and related witnesses, and this theorem supplies the Born conjunct without extra hypotheses. It is also consumed by HonestClosureCert, whose verification predicate records an honest framing of what is actually proved (φ-closed observables and related closure facts).
In the broader Recognition chain this is the measurement-side counterpart to the forcing landmarks (J-uniqueness, φ, eight-tick octave). It does not derive the Born rule from T0–T8 here; it certifies that the two-outcome specialization already verified upstream is available as a simp-normal proposition inside RecogSpec.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.