LF6-A.1: Forced contextuality of the entangled de-isolation tier

Category: 6-Local (first concrete attack on CSD's D1 entangled frontier; the conceptual crux of the entangled-singlet de-isolation tier).

Glossary: https://glossary.constraintsurfacedynamics.com/hidden-variables/ Plain-language, CSD-role and formal statements of hidden variables, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.

The idea

In CSD a measurement is de-isolation (LF5): the deterministic FS-measure-preserving flow carves the ontic space Σ into pointer-outcome volumes. A product (factorising, non-contextual) outcome-partition of Σ — one where Alice's outcome is a function of her setting and the shared microstate alone, RA : SettingA → SigmaSpace → Sign, and Bob's of his setting alone, RB : SettingB → SigmaSpace → Sign, on one shared probability space (SigmaSpace, μ) — is precisely a deterministic local-hidden-variable model. The setting-locality on a shared SigmaSpace (RA a depends on a only, RB b on b only) is the factorisation / non-contextuality being ruled out.

By Bell/CHSH (already in the corpus, E91.lhvCHSH_abs_le_two) no such product partition reproduces the singlet correlations: any product partition obeys |CHSH| ≤ 2, while the singlet at canonical settings reaches 2√2 (Bell.chsh_singlet_at_optimal_angles). So any partition that DOES realise the singlet must be jointly contextual. The non-factorisation is forced, not posited; it lives in the Σ-volume engine's reading of the entangled state.

Conceptual ledger (honest)

• (a) Derived, not posited. The non-factorisation is a property of the Σ-volume engine's reading of the entangled state (the singlet kernel P_st), not a partition put in by hand. engine_joint_nonfactorises is a P_st-arithmetic fact; the correlations are the derived source.
• (b) Contextuality is FORCED (Bell). By no_product_partition_realises_singlet, no setting-local Σ-partition on a shared (SigmaSpace, μ) reproduces the singlet correlations. Hence any de-isolation carve realising the singlet is contextual. This is e91_no_lhv_reproduces_singlet's content re-expressed for setting-local Σ-partitions; it REUSES lhvCHSH_abs_le_two and the singlet 2√2, it does not re-prove Bell.
• (c) Factorisation = measurement. A product outcome-partition would be a setting-local assignment of definite values, i.e. a completed measurement. So factorisation IS the measurement and cannot pre-exist de-isolation. The outcomes are not setting-local definite values waiting to be read; they are produced by the carve.
• (d) Nudge ≠ carve. Pre-measurement nudging (a unitary Φ_U reshaping of the Σ-volumes, e.g. an axis rotation) IS available and is distinct from the carve (the de-isolation flow that fixes the pointer blocks). Nudging is a symmetry of the engine; carving is the irreversible context selection.
• (e) One engine, two outputs. Born weights (LF4/LF5 moment-map / Duistermaat-Heckman volume) and non-locality (this file) are two outputs of the SAME Σ-volume engine. The marginals factorise (no-signalling, engine_marginal_factorises) even though the joint does not.
• (f) Residue: SO-1. This realises the singlet correlations MODULO the posited CSD sector (SO-1) — the entangled sector / the singlet's preparation region Ω₀ is posited, not derived from deterministic dynamics (SO-1: the sector origin, distinct from Paper C Axiom A5). The forced-contextuality no-go is unconditional Bell content; the engine reading of the singlet rests on the posited entangled sector.
• (g) Scope: LF6-A.1 only. THIS file is the conceptual crux (LF6-A.1). Status of the rest of the A-tier, corrected 2026-08-10 (this note previously said A.2 was deferred, which went stale when A.2 and A.3 landed):
  • LF6-A.2 LANDED (SingletDeisolationFlow.lean): the de-isolation flow on ℂℙ¹⁵ with pointer-block volumes = P_st.
  • LF6-A.3 LANDED (LocalDeisolationFlow.lean): the local product dilation, localDeisolation_factorises. ⚠️ The original N = 4 adder flow of A.2 does not factorise; A.3 is a separate local product dilation realising the same pointer statistics.
  • Setting-dependent nudge locality LANDED 2026-08-10 (NudgeLocality.lean): localNudge, localMeasurementChain_factorises. ⚠️ This is a correction, not an addition — nudgedSinglet is not a local-unitary image of the singlet at all.
  • Generic-context restriction REMOVED for the local route (localDeisolation_pointer_volume_local, no hgen); it is retained on the original localDeisolation_pointer_volume.

What is reused (no Bell re-proof)

• CSD.Empirical.QM.E91.lhvCorrelation / lhvCHSH / lhvCHSH_abs_le_two (the LHV CHSH ≤ 2 bound on any shared probability space with ±1 local responses).
• CSD.Empirical.Bell.correlation / chshOperator / chsh_singlet_at_optimal_angles (the singlet's −a·b correlation and the canonical −2√2 CHSH value).
• CSD.LF3.P_st / marginal_a_eq_half / marginal_b_eq_half / no_signalling_strong_readout_a / no_signalling_strong_readout_b.

All exports are foundational-triple-only (the machinery is measure-theoretic, no Busch).

The singlet correlation target

noncomputable def CSD.LF6.singletCorrelation (a b : LF3.DetectorSetting) : ℝ

The singlet correlation function, taken verbatim from the corpus (Bell.correlation a b = −(a·b), Bell.correlation_eq_neg_dot). This is the target a Σ-partition must reproduce; it is the singlet's −a·b, not a reinvention.

Equations

• CSD.LF6.singletCorrelation a b = CSD.Empirical.Bell.correlation a b

theorem CSD.LF6.singletCorrelation_eq_neg_dot (a b : LF3.DetectorSetting) : singletCorrelation a b = -LF3.dotR a b

singletCorrelation a b = −(a·b), re-stating LF3.correlation_eq_neg_dot.

The product-partition predicate

A product partition of the shared ontic space (SigmaSpace, μ) is a pair of setting-local ±1 measurable response functions. RA a depends only on Alice's setting a, RB b only on Bob's setting b: that setting-locality on a shared SigmaSpace is exactly the factorisation / non-contextuality assumption — it is a deterministic local-hidden-variable model.

def CSD.LF6.IsProductPartition {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] (RA RB : LF3.DetectorSetting → SigmaSpace → ℝ) : Prop

RA, RB form a product (non-contextual) partition of the shared ontic space (SigmaSpace, μ): setting-local, measurable, ±1-valued responses. The load-bearing structural point is the setting-locality — RA a is a function of Alice's setting a and the shared microstate alone, RB b of Bob's setting b alone.

Equations

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

def CSD.LF6.ReproducesSinglet {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] (μ : MeasureTheory.Measure SigmaSpace) (RA RB : LF3.DetectorSetting → SigmaSpace → ℝ) : Prop

A product partition reproduces the singlet correlations if its factorisable LHV correlation ∫ RA(a,·)·RB(b,·) dμ matches the singlet's −a·b at every pair of settings.

Equations

• CSD.LF6.ReproducesSinglet μ RA RB = ∀ (a b : CSD.LF3.DetectorSetting), CSD.Empirical.QM.E91.lhvCorrelation μ RA RB a b = CSD.LF6.singletCorrelation a b

theorem CSD.LF6.lhvCHSH_eq_chshOperator {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] (μ : MeasureTheory.Measure SigmaSpace) (RA RB : LF3.DetectorSetting → SigmaSpace → ℝ) (hRep : ReproducesSinglet μ RA RB) (a a' b b' : LF3.DetectorSetting) : Empirical.QM.E91.lhvCHSH μ RA RB a a' b b' = Empirical.Bell.chshOperator a a' b b'

A reproducing product partition's CHSH combination is literally the singlet CHSH operator: rewrite each LHV correlation by the reproduction hypothesis.

The forced-contextuality no-go

theorem CSD.LF6.no_product_partition_realises_singlet {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] (μ : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μ] (RA RB : LF3.DetectorSetting → SigmaSpace → ℝ) (hPP : IsProductPartition RA RB) (hRep : ReproducesSinglet μ RA RB) : False

no_product_partition_realises_singlet (LF6-A.1, load-bearing). There is NO product (setting-local, non-contextual) partition of any shared probability space (SigmaSpace, μ) whose factorisable correlations reproduce the singlet correlations.

Proof: such a partition gives lhvCHSH = chshOperator = −2√2 at the canonical settings (lhvCHSH_eq_chshOperator + Bell.chsh_singlet_at_optimal_angles), hence |lhvCHSH| = 2√2; but lhvCHSH_abs_le_two caps it at 2, and 2 < 2√2.

This is e91_no_lhv_reproduces_singlet's content re-expressed for setting-local Σ-partitions: it reuses lhvCHSH_abs_le_two and the singlet 2√2 directly and does NOT re-prove Bell. The forced contextuality: any Σ-partition realising the singlet must be jointly contextual.

Notation bridge. The binder SigmaSpace is named for the intended CSD instantiation, but mathematically it is Bell's Λ: the theorem quantifies over an arbitrary measurable space with a probability measure — no CSD-specific hypothesis anywhere, so it transfers to rival theories of the same shape (its recorded force in necessity-audit.md).

theorem CSD.LF6.productPartition_nonvacuous {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] (μ : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μ] : (IsProductPartition (fun (x : LF3.DetectorSetting) (x_1 : SigmaSpace) => 1) fun (x : LF3.DetectorSetting) (x_1 : SigmaSpace) => 1) ∧ ∀ (a b : LF3.DetectorSetting), Empirical.QM.E91.lhvCorrelation μ (fun (x : LF3.DetectorSetting) (x_1 : SigmaSpace) => 1) (fun (x : LF3.DetectorSetting) (x_1 : SigmaSpace) => 1) a b = 1

Non-vacuity of the no-go. Product partitions exist (the predicate is inhabitable) and reproduce some correlation — just not the singlet's. The all-+1 responses form a product partition whose correlation is the constant 1; since the singlet correlation is non-constant (−a·b), this partition does not reproduce the singlet, so no_product_partition_realises_singlet is a genuine separation, not a vacuous predicate.

The engine's non-factorising joint / factorising marginal pair

theorem CSD.LF6.engine_joint_nonfactorises : ∃ (a : LF3.DetectorSetting) (b : LF3.DetectorSetting) (s : LF3.Sign) (t : LF3.Sign), LF3.P_st a b s t ≠ (∑ t' : LF3.Sign, LF3.P_st a b s t') * ∑ s' : LF3.Sign, LF3.P_st a b s' t

engine_joint_nonfactorises. The singlet kernel does NOT factor: there is a concrete setting and sign pair where the joint P_st(s,t) differs from the product of marginals P_A(s)·P_B(t) = (1/2)·(1/2) = 1/4.

Witness: aligned axes a = b = ẑ̂_x (so a·b = 1) with s = t = +, where P_st = (1 − 1)/4 = 0 ≠ 1/4. A P_st-arithmetic fact; the derived source of the singlet correlations.

theorem CSD.LF6.engine_marginal_factorises : (∀ (a b : LF3.DetectorSetting) (s : LF3.Sign), ∑ t : LF3.Sign, LF3.P_st a b s t = 1 / 2) ∧ (∀ (a b : LF3.DetectorSetting) (t : LF3.Sign), ∑ s : LF3.Sign, LF3.P_st a b s t = 1 / 2) ∧ (∀ (a b b' : LF3.DetectorSetting) (s : LF3.Sign), ∑ t : LF3.Sign, LF3.P_st a b s t = ∑ t : LF3.Sign, LF3.P_st a b' s t) ∧ ∀ (a a' b : LF3.DetectorSetting) (t : LF3.Sign), ∑ s : LF3.Sign, LF3.P_st a b s t = ∑ s : LF3.Sign, LF3.P_st a' b s t

engine_marginal_factorises (no-signalling). Each marginal of the singlet kernel is 1/2, independent of the other side's setting. The marginal factorises even though the joint does not — the operational signature of no-signalling. Reuses LF3.marginal_a_eq_half / marginal_b_eq_half / no_signalling_strong_readout_a / _b.