LF6-A.2: the full singlet de-isolation flow #

Category: 6-Local (the dynamical realisation of the entangled de-isolation tier; the D1 entangled frontier).

This is LF6-A.2 of specs/lf6-plan.md: an actual deterministic, Fubini–Study-measure-preserving de-isolation flow whose contextual carve reproduces the LF3 singlet kernel P_st, with a.s. pointer-block frequencies converging to P_st. It is the dynamical counterpart of the forced-contextuality no-go LF6-A.1 (ForcedContextuality.lean), which it reuses for the contextuality anchor.

The construction (clean path, reusing LF5 @ N = 4 + LF3 + A.1) #

The system is the joint two-qubit register ℂ⁴ ≅ ℂ² ⊗ ℂ², measured by the LF5 von Neumann de-isolation flow measurementFlow 4 e on the dilated projective ontic space Σ' = ℂℙ¹⁵ = ℙ(EuclideanSpace ℂ (Fin 16)) (e = finProdFinEquiv, 16 = 4·4 = 15 + 1).

⚠️ Not shown to factorise by wing (clarified 2026-08-11). The A.2 N = 4 adder flow reproduces the required contextual statistics, but ℤ/4 ≠ ℤ/2 × ℤ/2, so it is not a product Φ_A ⊗ Φ_B. Product locality is exhibited separately by A.3 (LocalDeisolationFlow.localDeisolation_factorises, V_loc = V_A ⊗ V_B) and extended to the whole finite chain by LF6.localMeasurementChain_factorises. C1's locality claim rests on those, not on calling this joint apparatus interaction "local".

The flow is an apparatus dynamics (it is the single-system LF5 de-isolation at N = 4); the non-locality is not in the flow but in the outcome carve, which is the joint BornRegion moment-subdivision of LF4/BornRegionUncond, and is jointly contextual by A.1.

The prepared state used here is φ = nudgedSinglet a b, whose computational coordinate at the pointer cell (s, t) is the singlet's joint-spin-eigenstate amplitude φ_{stIdx (s,t)} = ⟨ψ⁻, singletJointEig s t a b⟩.

⚠️ nudgedSinglet is the MODULI, not a locally rotated singlet (corrected 2026-08-10; this paragraph previously read it as (U_A^x ⊗ U_B^y)† ψ⁻, which is false). singletJointEig normalises by the real √P_st, so every coordinate here is real and non-negative and all relative phase is discarded. At a ⊥ b that gives ½(1,1,1,1), a product state, while ψ⁻ is maximally entangled — so it is a local-unitary image of the singlet only at a·b = ±1. Nothing below is affected, because everything here consumes only ‖·‖².

What is valid here: the probability results — nudgedSinglet_norm, nudgedSinglet_born, and the pointer-volume headline — all of which are statements about moduli and all of which carry hgen.

Where to go for locality: LF6.localNudgeVec (NudgeLocality.lean), defined as (U_A(a) ⊗ U_B(b))ᴴ ψ⁻ for the proved-unitary wingBasisUnitary, with the same Born statistics and no hgen. Then the headline:

pointer-block (s,t) FS volume  =  ‖⟨e_{stIdx (s,t)}, φ⟩‖²        -- LF5 vnDilation_pointer_volume @ N=4
                               =  ‖⟨ψ⁻, singletJointEig s t a b⟩‖² -- nudge coordinate identity
                               =  P_st a b s t                     -- LF3 singletJointEig_born

So the reproduction is LF5@N=4 + a coordinate (unitary-invariance) step + LF3's Born identity. The basis-change vectors are the genuine joint spin eigenstates of LF3/Singlet/JointEig.lean; the Born identity singletJointEig_born is the proof behind MeasurementJointEig.born_eq_P_st.

Honest scope (the A.2 ledger) #

Exhibited. A genuine deterministic FS-measure-preserving de-isolation flow Φ ≠ id (singletDeisolation_*, inherited from LF5-B), whose joint BornRegion pointer-block volumes equal P_st (singletDeisolation_pointer_volume) and whose a.s. block frequencies converge to P_st (singletDeisolation_frequency).
Imported, not re-derived. Born = FS-volume is derived one layer down (the moment-map / Duistermaat–Heckman cluster, fs_born_volume_ratio_N, Gleason-free, no Born put in) and imported through vnDilation_pointer_volume. The singlet kernel P_st and its joint eigenstates / Born identity are LF3. The contextuality no-go is LF6-A.1.
Contextual carve, routed through A.1. The outcome is the joint BornRegion cell, not a setting-local {pointer_A = i} ∩ {pointer_B = j} product region. singletDeisolation_carve_contextual proves, through no_product_partition_realises_singlet, that no setting-local ±1 product partition reproduces the carve's correlations; the carve's block-volume correlation is −a·b (singletDeisolation_blockVolume_correlation), the singlet's, which A.1 forbids any product partition to produce. The flow may be local; the carve is contextual. Measurement is contextual.
A.3 — LANDED (LocalDeisolationFlow.lean; this bullet previously said "deferred", corrected 2026-08-10). ⚠️ The N = 4 adder flow below still does not factorise (ℤ/4 ≠ ℤ/2 × ℤ/2); A.3 supplies a separate local product dilation V_loc = V_A ⊗ V_B realising the same pointer statistics, and LF6.localMeasurementChain_factorises extends that to the whole finite chain. ★ A.3 does not factorise A.2. It supplies an alternative factorised realisation of the same joint measurement: A.2 gives a joint N = 4 realisation that is not wing-factorised, and A.3 independently gives a factorised local one. The decomposition of the N = 4 joint coupling itself into two wing couplings is not established, and is not needed — the locality claim rests on A.3's construction, not on decomposing A.2's. (Superseded historical status for this bullet is in specs/c1-closure-report.md, not here.) This does not weaken A.2: A.1 already establishes that the locality of the flow is consistent with the contextuality of the carve, and the safety anchor (singletDeisolation_carve_contextual) does not assume the product structure.
Residue: SO-1. The entangled sector / the singlet's preparation region Ω₀ is posited, not derived (SO-1: the sector origin, distinct from Paper C Axiom A5). nudgedSinglet's amplitudes are the singlet's; the typicality law on Σ' is the Fubini–Study measure (SO-1).
Generic context. The four-sector construction needs P_st a b s t > 0 for all (s, t) (hgen), i.e. |a·b| < 1 — the generic non-collinear contexts, which include the four canonical CHSH-optimal pairs. Collinear axes are excluded. ⚠️ Corrected 2026-08-11: the previous wording said they "have a vanishing sector and carry no Born information"; both halves were wrong. At a·b = ±1 two of the four sectors have probability zero and the other two carry 1/2 each — perfect (anti)correlation, which is among the most informative Bell data, not an absence of Born content. They are excluded here only because the legacy singletJointEig normalisation divides by √P_st and so needs all four P_st > 0. LF6.localNudgeVec has no such division and covers them (localDeisolation_pointer_volume_local).

All exports are foundational-triple-only (Gleason-free; the LF5 pointer engine is off Busch, A.1 is measure-theoretic Bell content).

Reference: specs/lf6-plan.md (LF6-A.2).

LF6-A.2: the full singlet de-isolation flow #

The construction (clean path, reusing LF5 @ N = 4 + LF3 + A.1) #

Honest scope (the A.2 ledger) #

Index identification Sign × Sign ≃ Fin 4 #

The legacy singlet-moduli representative #

Deliverable 1: the flow #

Deliverable 2: pointer-block FS volume = P_st (the headline) #

Deliverable 3: a.s. pointer-block frequencies → P_st #

Deliverable 4: the carve is contextual (the safety anchor, via A.1) #

Deliverable 6: the capstone #

Index identification `Sign × Sign ≃ Fin 4` #

Deliverable 2: pointer-block FS volume = `P_st` (the headline) #

Deliverable 3: a.s. pointer-block frequencies → `P_st` #