The two-wing record of the local de-isolation flow

Category: 3-Local (the entangled de-isolation tier). BACKLOG #131, obligation (1), second half: tying the record events to LF6's pointer blocks.

What was missing, and it was not a number

LF6's clause (3) already says the de-isolation reproduces the singlet, and NudgeLocality's localDeisolation_A_marginal_volume_eq_half already says each wing's marginal is 1/2 at every setting pair. Those numbers are not re-proved here, they are imported. What was missing is that every one of those statements is about a sum over an index set —

∑ n : Fin 4, (epistemicMeasure p (globalBasin (momentContext (M+1)) (e (n, stIdx (s,t))))).toReal

— and a sum of numbers is not an event. There was no set whose measure is "the two wings recorded (s, t)", so there was nothing to transport along the flow, nothing to intersect, and nothing to factor through a macroscopic coordinate. #131's blocker (I) having been resolved by option I1, TwoWingCoarsening.lean supplies those sets as coarsenings of the fine basins, and this file identifies the coarsening that LF6's index map realises.

What is proved

• pointerDecode e — the decoding LF6 was using implicitly: a basin index i : Fin (M+1) records the wing pair stIdx⁻¹ (e⁻¹ i).2, the system index n being exactly what the pointer block sums over. ★ filter_pointerDecode is the index transport of the audit's §3: the fine cells the decoding sends to (s,t) are precisely LF6's pointer block {e (n, stIdx (s,t)) | n};
• ★★★ toReal_measure_wingEvent_eq_P_st — the two-wing record event's Born weight is the singlet's joint distribution, P_st a b s t, at every setting pair (no genericity hypothesis, routing through localDeisolation_pointer_volume_local). This is clause (3) restated about one event rather than a sum, which is what makes everything below possible;
• ★★★ toReal_measure_preimage_wingEvent_eq_P_st — one physical record history. The probability, in the prepared pre-measurement epistemic measure, that the run ends with the two wings recording (s, t) is P_st a b s t. The Born clause was only ever available at the post-measurement ray; composing it with measure_preimage_liftBase and clause (6) (localDeisolationFlow_realises_localNaimark) moves it to the prepared ray, which is where an experiment starts. This is the obligation;
• ★★★ toReal_measure_wingAEvent_eq_half / ★★★ toReal_measure_wingBEvent_eq_half and ★★ toReal_measure_preimage_wingAEvent_eq_half — each wing's marginal is 1/2, as an event probability and then along the flow from the prepared ray. The arithmetic is LF3.marginal_a_eq_half, imported; what is new is that these are measures of sets and that they hold at the start of the run;
• ★★ toReal_measure_preimage_wingAEvent_eq_of_setting — operational no-signalling along the dynamics: A's wing-event probability is the same for b and b', with each side evaluated in its own prepared measure and after its own flow. It also discharges, for the singlet, the premise that measure_wingAEvent_eq_of_fineSum_eq leaves open — #131 recorded that premise as not discharged, and for this model it now is;
• ★★ factorsThrough_wingEvent_pointerDecode — the two-wing events are macroscopic: preimages of #102's record string, which is obligation (5)'s shape at this instance.

Honest scope

⚠️ The marginals and no-signalling are imported arithmetic, not new content. localDeisolation_A_marginal_volume_eq_half and localDeisolation_no_signalling_A already prove them for the index sums. The contribution here is the event formulation and the prepared-ray formulation, not the numbers.

⚠️ One ontic selector. Everything here inherits option I1's concession: the two wings are two readings of x.2.1. See TwoWingCoarsening.lean and BACKLOG row 132.

⚠️ Not Bell, and not C-1. No CHSH value is computed here and no causal structure is used; obligation (3) (records to causal regions) and obligation (4)'s Bell half are separate, and the missing RemoteSettingLocalityB witness of the audit's §4 is still missing. Nothing here shows that apparent nonlocality is a consequence of projection alone.

⚠️ The preparation is the moduli-free local object. localNudgeVec a b = (U_A(a) ⊗ U_B(b))ᴴ ψ⁻, not nudgedSinglet, which strips every phase — see NudgeLocality's erratum. That is why no genericity hypothesis appears.

⚠️ One flow, one measurement. liftBase localDeisolationFlow moves the base and leaves the record medium fixed, so this says nothing about record writes on the fibre (RecordLayer.sigmaShift) or about record stability over time, which is obligation (2).

References: NudgeLocality.lean (localNudgeVec, localDeisolation_pointer_volume_local, localDeisolation_A_marginal_volume_eq_half), LocalDeisolationFlow.lean (localDeisolationFlow, localDeisolationFlow_realises_localNaimark, localEmbedGround, localDeisolation_capstone), SingletDeisolationFlow.lean (stIdx), TwoWingCoarsening.lean (coarseEvent, wingEvent, measure_coarseEvent, measure_wingAEvent_eq_sum, factorsThrough_coarseEvent), FlowRecordHistory.lean (liftBase, measure_preimage_liftBase), LF3/Singlet/Kernel.lean (P_st), Empirical/QM/Bell.lean (marginal_a_eq_half); specs/BACKLOG.md #131 obligation (1), #132; specs/two-wing-experiment-scoping.md §3 (the index transport) and §6.

The decoding LF6 was using implicitly

def CSD.LF6.pointerDecode {M : ℕ} (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (i : Fin (M + 1)) : LF3.Sign × LF3.Sign

The pointer decoding. A basin index i : Fin (M+1) carries a system index and a pointer index through e; the pointer half is the two-wing outcome, and the system half is exactly what LF6's pointer-block sum traces out.

Equations

• CSD.LF6.pointerDecode e i = CSD.LF6.stIdx.symm (e.symm i).2

@[simp]

theorem CSD.LF6.pointerDecode_apply {M : ℕ} (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (n : Fin 4) (st : LF3.Sign × LF3.Sign) : pointerDecode e (e (n, stIdx st)) = st

theorem CSD.LF6.pointerDecode_eq_iff {M : ℕ} (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (i : Fin (M + 1)) (st : LF3.Sign × LF3.Sign) : pointerDecode e i = st ↔ ∃ (n : Fin 4), i = e (n, stIdx st)

theorem CSD.LF6.filter_pointerDecode {M : ℕ} (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (st : LF3.Sign × LF3.Sign) : {i : Fin (M + 1) | pointerDecode e i = st} = Finset.image (fun (n : Fin 4) => e (n, stIdx st)) Finset.univ

★ The index transport of the audit's §3. The fine cells the pointer decoding sends to (s, t) are precisely LF6's pointer block — so the coarsening of TwoWingCoarsening.lean and the index map of clause (3) describe the same set of basins, and nothing has been quietly re-indexed.

theorem CSD.LF6.injOn_pointerBlock {M : ℕ} (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (st : LF3.Sign × LF3.Sign) : Set.InjOn (fun (n : Fin 4) => e (n, stIdx st)) ↑Finset.univ

The pointer block is one event

theorem CSD.LF6.measure_wingEvent_pointerDecode {M : ℕ} (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (p : LF4.CPN (M + 1)) (st : LF3.Sign × LF3.Sign) : (RecordLayer.epistemicMeasure p) (RecordLayer.wingEvent (RecordLayer.momentContext (M + 1)) (pointerDecode e) st) = ∑ n : Fin 4, (RecordLayer.epistemicMeasure p) (RecordLayer.globalBasin (RecordLayer.momentContext (M + 1)) (e (n, stIdx st)))

The two-wing record event's weight is the pointer-block sum. The left-hand side is the measure of a set; the right-hand side is the sum LF6's clause (3) is stated in.

theorem CSD.LF6.toReal_measure_wingEvent_pointerDecode {M : ℕ} (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (p : LF4.CPN (M + 1)) (st : LF3.Sign × LF3.Sign) : ((RecordLayer.epistemicMeasure p) (RecordLayer.wingEvent (RecordLayer.momentContext (M + 1)) (pointerDecode e) st)).toReal = ∑ n : Fin 4, ((RecordLayer.epistemicMeasure p) (RecordLayer.globalBasin (RecordLayer.momentContext (M + 1)) (e (n, stIdx st)))).toReal

The singlet's joint law, as one event's Born weight

theorem CSD.LF6.toReal_measure_wingEvent_eq_P_st {M : ℕ} (a b : LF3.DetectorSetting) (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin localDeisolationV) (localNudgeVec a b))) (hψ'0 : ψ' ≠ 0) (s t : LF3.Sign) : ((RecordLayer.epistemicMeasure (Projectivization.mk ℂ ψ' hψ'0)) (RecordLayer.wingEvent (RecordLayer.momentContext (M + 1)) (pointerDecode e) (s, t))).toReal = LF3.P_st a b s t

★★★ The two-wing record event reproduces the singlet. The Born weight of "the two wings recorded (s, t)" is P_st a b s t, at every setting pair.

This is LF6's clause (3) restated about a single event instead of a sum over a pointer block, and that restatement is the point: an event can be transported along the flow, which is what the next theorem does. The arithmetic is localDeisolation_pointer_volume_local, imported.

theorem CSD.LF6.toReal_measure_wingAEvent_eq_half {M : ℕ} (a b : LF3.DetectorSetting) (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin localDeisolationV) (localNudgeVec a b))) (hψ'0 : ψ' ≠ 0) (s : LF3.Sign) : ((RecordLayer.epistemicMeasure (Projectivization.mk ℂ ψ' hψ'0)) (RecordLayer.wingAEvent (RecordLayer.momentContext (M + 1)) (pointerDecode e) s)).toReal = 1 / 2

★★★ The A-wing's event probability is 1/2, at every setting pair. The marginal arithmetic is LF3.marginal_a_eq_half; what is new is that the left-hand side is the measure of a set, obtained from the joint events by measure_wingAEvent_eq_sum rather than by summing numbers.

theorem CSD.LF6.toReal_measure_wingBEvent_eq_half {M : ℕ} (a b : LF3.DetectorSetting) (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin localDeisolationV) (localNudgeVec a b))) (hψ'0 : ψ' ≠ 0) (t : LF3.Sign) : ((RecordLayer.epistemicMeasure (Projectivization.mk ℂ ψ' hψ'0)) (RecordLayer.wingBEvent (RecordLayer.momentContext (M + 1)) (pointerDecode e) t)).toReal = 1 / 2

★★★ The B-wing's event probability is 1/2, symmetrically.

theorem CSD.LF6.factorsThrough_wingEvent_pointerDecode {M : ℕ} (e : Fin 4 × Fin 4 ≃ Fin (M + 1)) (st : LF3.Sign × LF3.Sign) : RecordLayer.FactorsThrough (RecordLayer.recordString fun (x : Fin 1) => RecordLayer.momentContext (M + 1)) (RecordLayer.wingEvent (RecordLayer.momentContext (M + 1)) (pointerDecode e) st)

★★ The two-wing events are macroscopic: each is a preimage of #102's record string, so the wing reading is visible at the level of the coarse projection and not only on the microstate. This is obligation (5)'s shape at this instance.

One physical record history

The flow carries the prepared ray to the dilated one (clause (6)), and measure_preimage_liftBase carries the record event back, so the Born statement moves from the post-measurement ray to where an experiment actually starts.

noncomputable def CSD.LF6.preparedRay (a b : LF3.DetectorSetting) : LF4.CPN (4 * 4)

The prepared, pre-measurement ray: the singlet in the wings' own bases, both pointers in their ground state.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CSD.LF6.dilatedRay (a b : LF3.DetectorSetting) : LF4.CPN (4 * 4)

The post-measurement ray, where LF6's Born clause is stated.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.LF6.localDeisolationFlow_preparedRay (a b : LF3.DetectorSetting) : localDeisolationFlow (preparedRay a b) = dilatedRay a b

The local product flow carries the prepared ray to the dilated one: clause (6) at the local preparation.

theorem CSD.LF6.measurable_localDeisolationFlow : Measurable localDeisolationFlow

theorem CSD.LF6.toReal_measure_preimage_wingEvent_eq_P_st (a b : LF3.DetectorSetting) (s t : LF3.Sign) : ((RecordLayer.epistemicMeasure (preparedRay a b)) (RecordLayer.liftBase localDeisolationFlow ⁻¹' RecordLayer.wingEvent (RecordLayer.momentContext (4 * 4)) (pointerDecode finProdFinEquiv) (s, t))).toReal = LF3.P_st a b s t

★★★ One physical record history. The probability, in the prepared epistemic measure, that the run ends with the two wings recording (s, t) is the singlet's joint distribution P_st a b s t.

LF6's Born clause is stated at the post-measurement ray; this is the same statement about the run that starts at the prepared ray, which is what an experiment is. It is obligation (1) of #131, and it needs all three pieces: clause (6) for the dynamics, measure_preimage_liftBase for the measure, and the coarsening for the event.

theorem CSD.LF6.toReal_measure_preimage_wingAEvent_eq_half (a b : LF3.DetectorSetting) (s : LF3.Sign) : ((RecordLayer.epistemicMeasure (preparedRay a b)) (RecordLayer.liftBase localDeisolationFlow ⁻¹' RecordLayer.wingAEvent (RecordLayer.momentContext (4 * 4)) (pointerDecode finProdFinEquiv) s)).toReal = 1 / 2

★★ The A-wing's marginal, along the flow from the prepared ray, is 1/2.

theorem CSD.LF6.toReal_measure_preimage_wingAEvent_eq_of_setting (a b b' : LF3.DetectorSetting) (s : LF3.Sign) : ((RecordLayer.epistemicMeasure (preparedRay a b)) (RecordLayer.liftBase localDeisolationFlow ⁻¹' RecordLayer.wingAEvent (RecordLayer.momentContext (4 * 4)) (pointerDecode finProdFinEquiv) s)).toReal = ((RecordLayer.epistemicMeasure (preparedRay a b')) (RecordLayer.liftBase localDeisolationFlow ⁻¹' RecordLayer.wingAEvent (RecordLayer.momentContext (4 * 4)) (pointerDecode finProdFinEquiv) s)).toReal

★★ Operational no-signalling along the dynamics. A's record-event probability is the same whether B's setting is b or b', with each side evaluated in its own prepared measure and after its own flow — so nothing B does can be read off A's record statistics.

This also discharges, for the singlet, the premise that RecordLayer.measure_wingAEvent_eq_of_fineSum_eq leaves open: there the summed fine weights were assumed equal, and here LF3.marginal_a_eq_half supplies that equality. #131 recorded the premise as not discharged; for this model it now is.