bornHolds
plain-language theorem explainer
Names the proposition that the empty two-outcome Born certificate verifies: for every two-branch rotation, normalized recognition path weights equal the cos²/sin² Born probabilities. Spec and closure authors cite it as the Born-compliance slot in the dimensionless pack and honest-closure certificate. It is a one-line abbreviation of the upstream verified predicate on the default certificate.
Claim. Let $\mathsf{bornHolds}$ be the proposition that the default two-outcome Born certificate is verified: for every two-branch rotation, the normalized recognition path weights equal the Born probabilities $\cos^2$ and $\sin^2$.
background
In the RecogSpec layer, dimensionless physics is packaged as explicit witnesses (units from anchors, band matching, Born compliance) rather than free parameters. The Born slot records that recognition path weights on a binary branch reproduce the textbook Born rule.
Upstream, TwoOutcomeBornCert is a unit structure whose verification predicate asserts: for every two-branch rotation, the normalized two-outcome probabilities match $\cos^2/\sin^2$. The empty certificate {} is the canonical instance; the predicate does not depend on certificate fields.
Locally this module assembles those witnesses into the universal dimensionless pack and related inevitability scaffolding, with constants drawn from the RS $\varphi$-ladder and display cores.
proof idea
Definitional abbreviation only: bornHolds is definitionally equal to TwoOutcomeBornCert.verified {}. No tactics or lemmas run at this site. The actual proof that the predicate holds is the sibling theorem born_from_TruthCore, which applies TwoOutcomeBornCert.verified_any to the empty certificate.
why it matters
Fills the Born-rule compliance slot in the RecogSpec witness stack. Downstream, born_from_TruthCore discharges it; UD_explicit and dimlessPack_explicit thread related dimensionless data; inevitability_dimless_holds builds the multi-conjunct inevitability package; and HonestClosureCert includes honest framing of what is proven (φ-closed observables and related certificates).
In Recognition Science terms this is the formal claim that path weights on the recognition ledger match Born probabilities on two-outcome branches, so the dimensionless closure does not smuggle an independent measurement postulate. It does not itself derive the eight-tick octave or $D=3$; those live in the forcing chain (T7, T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.