LF6/NudgeLocality: the setting-dependent nudge, done locally #
Category: 6-Entanglement (the local half of the setting-dependent chain).
Why this exists #
SingletDeisolationFlow.nudgedSinglet is documented as the singlet "transformed
by local basis rotations". That is false. Inside singletJointEig_born,
inner ℂ singlet (singletJointEig s t a b) = (Real.sqrt (P_st a b s t) : ℂ)
so nudgedSinglet a b is the vector (√P_st)_{s,t} — all real, all
non-negative, every phase stripped. Local unitaries preserve Schmidt spectra
and ψ⁻ is maximally entangled; but at a ⊥ b all four P_st = ¼, so
nudgedSinglet = ½(1,1,1,1), a product state. No local unitary carries a
maximally entangled state to a product state, so nudgedSinglet is a
local-unitary image of ψ⁻ only at a·b = ±1 — exactly the endpoint set the
hgen hypothesis excludes.
The defect is in singletJointEig := (√P_st)⁻¹ • (Πˢ(a) ⊗ Πᵗ(b)) ψ⁻, which fixes
each basis vector's phase by projecting ψ⁻ itself: four independent phases,
where a product unitary supplies only separable ones (αₛ + βₜ).
What this module does #
localNudge is the object nudgedSinglet was described as being. It is
defined as the action of a product unitary on the singlet, so locality is
definitional rather than asserted, and there is no phase to get wrong:
localNudge a b := (U_A(a) ⊗ U_B(b))ᴴ ψ⁻
with U_A(a) = wingBasisUnitary a proved unitary in LF3/Spinor.lean.
localNudge_coord— its(k,l)coordinate is⟨u ⊗ w, ψ⁻⟩.- ★★
localNudge_born—‖coordinate‖² = P_st, with no genericity hypothesis. SolocalNudgereproduces exactly the Born statisticsnudgedSingletwas used for, while genuinely being a local-unitary image of the singlet.
References #
LF3/Spinor.lean (spinor, wingBasisUnitary, spinProj_eq_outer,
jointSpinProj_eq_outer); LF3/Singlet/JointProjector.lean
(singlet_jointSpinProj_expectation); LF6/SingletDeisolationFlow.lean (the
object this replaces); specs/c1-correction-plan.md §3b.
The product unitary U_A(a) ⊗ U_B(b) implementing the setting change.
Equations
- CSD.LF6.wingPairUnitary a b = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (CSD.LF3.wingBasisUnitary a) (CSD.LF3.wingBasisUnitary b)
Instances For
wingPairUnitary really is a product unitary. Both wing factors are
unitary (LF3.wingBasisUnitary_mem_unitaryGroup) and the Kronecker product of
unitaries is unitary (Matrix.kronecker_mem_unitary).
Added 2026-08-11. The modules below called this object a "product unitary" in prose while only its factors carried an exported unitarity theorem — leaving the word "unitary" as an inference sitting in documentation. It is now a machine-checked statement, which is the standard the rest of the C1 tier is held to.
The same fact in unitaryGroup form, matching wingBasisUnitary_mem_unitaryGroup.
★ The nudge, done locally. The singlet rotated into the (a,b)
eigenbasis by a product unitary — unitary as a theorem
(wingPairUnitary_mem_unitaryGroup), not by assertion. Locality is
definitional.
Equations
Instances For
The (k,l) coordinate of the local nudge is the overlap of the singlet with
the product eigenvector u ⊗ w.
The Born identity on the local object #
For a rank-one M = v vᴴ, the singlet expectation is |⟨v, ψ⁻⟩|².
★★ The Born identity for the local nudge, with no genericity
hypothesis: the squared modulus of the (k,l) coordinate is the singlet kernel
P_st.
So localNudge reproduces exactly the statistics nudgedSinglet was used for,
while — unlike nudgedSinglet — genuinely being the image of ψ⁻ under a
product unitary.
Transport to the Fin 4 pointer indexing #
The downstream volume machinery indexes pointer cells by Fin 4 through
stIdx. This carries localNudge across, so it is a drop-in replacement for
nudgedSinglet — with the genericity hypothesis gone.
The local nudge in the Fin 4 pointer indexing.
Equations
- CSD.LF6.localNudgeVec a b = WithLp.toLp 2 fun (k : Fin 4) => (CSD.LF6.localNudge a b).ofLp (CSD.LF6.signEquiv (CSD.LF6.stIdx.symm k).1, CSD.LF6.signEquiv (CSD.LF6.stIdx.symm k).2)
Instances For
★ The pointer-cell Born identity, with no genericity hypothesis.
Compare nudgedSinglet_coord_normSq, which needs hgen.
★ Unit norm, with no genericity hypothesis. Compare
nudgedSinglet_norm, which needs hgen.
★ The pointer-cell Born identity in single-basis form, matching
basisPOVM_weight. No genericity hypothesis.
The local nudge is nonzero, with no genericity hypothesis.
The pointer-volume theorem, re-routed and genericity-free #
★★ The local de-isolation reproduces the singlet, at EVERY setting pair.
This is localDeisolation_pointer_volume with nudgedSinglet replaced by
localNudgeVec, and without hgen. The genericity restriction was never
intrinsic to the volume machinery — povm_born_eq_dilated_volume_uncond is
already hpos-free — it entered only through singletJointEig's division by
√P_st. Routing through the local object removes it, so the perfectly
(anti)correlated endpoints a·b = ±1 are now covered.
The complete finite measurement chain factorises #
⚠️ Scope. This is a statement about the finite dilated construction — the
wing de-isolation isometries and the wing basis unitaries — not about arbitrary
ontic Σ. No canonical subsystem decomposition of Σ is used or implied.
★★ The whole setting-dependent chain is a product of wing-local maps.
Composing the context-setting nudge with the apparatus coupling gives
(V_A ⊗ V_B) · (U_A(a) ⊗ U_B(b))ᴴ = (V_A · U_A(a)ᴴ) ⊗ (V_B · U_B(b)ᴴ)
so each wing's operation depends only on that wing's setting. This is work-order
item 8, and it is available only because localNudge replaced nudgedSinglet:
the old object is not a product-unitary image of the singlet at all, so no such
factorisation existed for it.
⚠️ This is dynamical locality of the chain. It is emphatically not Bell
factorisation of outcomes, which no_product_partition_realises_singlet proves
impossible for the singlet.
Operational no-signalling of the explicit construction (item 15) #
The pointer-block volumes reproduce P_st, so summing out one wing gives that
wing's marginal. Because the singlet marginals are 1/2 at every context,
the A-marginal volume does not move when B's setting changes.
⚠️ These are equalities of marginal volumes, never of the underlying
outcome partitions. The microscopic regions differ between contexts; only their
measures agree. And the whole statement sits under measurement independence,
as LF3.OperationalNoSignalling records.
★ The A-wing marginal volume is 1/2. Summing the pointer-block volumes
over the B outcome recovers the A marginal, which the singlet fixes at one half.
No genericity hypothesis.
★ The B-wing marginal volume is 1/2, symmetrically.
★★ A-wing operational no-signalling for the explicit construction.
Changing B's setting from b to b' leaves the A-marginal volume unchanged.
The two sides are built from different prepared states, so the underlying pointer regions differ; what agrees is their measure.
★★ B-wing operational no-signalling for the explicit construction.