entanglement_implies_interference
plain-language theorem explainer
Under the ledger entanglement-ontology hypothesis, the squared modulus of a sum of two complex amplitudes expands with the usual interference cross term. Anyone deriving Born-rule interference from RS ledger structure would cite this. The proof is a one-line application of that hypothesis to the two amplitudes.
Claim. If the entanglement-ontology-from-ledger hypothesis holds, then for all complex amplitudes $\psi_1,\psi_2$, $\|\psi_1+\psi_2\|^2 = \|\psi_1\|^2 + \|\psi_2\|^2 + 2\,\mathrm{Re}(\psi_1\overline{\psi_2})$.
background
This module treats structural entanglement content as the presence of interference cross terms in amplitude arithmetic. The governing hypothesis, entanglement-ontology-from-ledger, is the proposition that every pair of complex amplitudes obeys the classical expansion of $|\psi_1+\psi_2|^2$ with the real part of the product against the conjugate.
Squared-norm primitives appear throughout the stack: finite amplitude vectors sum component squares; finite Hilbert displays reuse the complex squared norm; planar carriers use Euclidean $|p|^2$; metric certificates use the quadratic form $g(v,v)$. Here the ambient objects are plain complex numbers with Mathlib's Complex.normSq.
The local setting is quantum structure imported from Born-rule material: interference is not postulated as a separate physical law but read off as the algebraic content of the ledger ontology hypothesis.
proof idea
One-line term proof: apply the hypothesis entanglement_ontology_from_ledger directly to the pair $(\psi_1,\psi_2)$. No rewriting, no lemmas beyond that universal quantifier. The conclusion is definitionally the body of the hypothesis.
why it matters
In Recognition Science, entanglement ontology is framed as structural interference content rather than an extra postulate. This theorem packages that framing as a usable implication: once the ledger hypothesis is assumed, the standard two-amplitude cross-term identity is available for Born-rule and interference arguments.
No downstream consumers are recorded yet (used_by is empty), so the declaration is presently a leaf export of the module. It sits beside the sibling structure definitions that name the same cross-term identity as the ontology content. Framework-wise it supports the quantum layer that must eventually connect ledger recognition to measurable interference, without yet touching the forcing chain (T5–T8), RCL, or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.