Documentation

CsdLean4.RecordLayer.SingletSkewTables

The singlet on the I3 record basins is operationally no-signalling, by the primitive #

Category: 7-SigmaLayer (the record layer — Paper C A7). BACKLOG #157 (out of #137): the concrete instance.

#137 instantiated the local-setting-aware primitive at the I3 basins for an arbitrary family of no-signalling 2 × 2 tables. The corpus's singlet kernel supplies the family: P_st a b s t = (1 − s t a·b)/4 (LF3/Singlet/Kernel.lean), with both marginals exactly 1/2 at every context (marginal_a_eq_half, marginal_b_eq_half). This file packages it and takes the corollary.

Honest scope #

References: SkewReroute.lean (skewOutcomeMaps, skewLocalSettingLocalityB, operationalNoSignalling_skew), LF3/Singlet/Kernel.lean (P_st, P_st_nonneg, marginal_a_eq_half, marginal_b_eq_half), LF3/OperationalNoSignalling.lean (singlet_operational_no_signalling, the kernel-level verification this now derives from a primitive); specs/BACKLOG.md #157, #137.

source
@[simp]
theorem CSD.RecordLayer.signOfFin_zero :
signOfFin 0 = LF3.Sign.plus
source
@[simp]
theorem CSD.RecordLayer.signOfFin_one :
signOfFin 1 = LF3.Sign.minus

The singlet's table at a context #

source
noncomputable def CSD.RecordLayer.singletJointRates (a b : LF3.DetectorSetting) :
JointRates 2 2

The singlet's joint table at the context ⟨a, b⟩, outcomes indexed by Fin 2 through signOfFin.

Equations
Instances For
    source
    @[simp]
    theorem CSD.RecordLayer.singletJointRates_rate (a b : LF3.DetectorSetting) (s t : Fin 2) :
    (singletJointRates a b).rate s t = LF3.P_st a b (signOfFin s) (signOfFin t)
    source
    theorem CSD.RecordLayer.singletJointRates_rowSum (a b : LF3.DetectorSetting) (s : Fin 2) :
    (singletJointRates a b).rowSum s = 1 / 2

    A's marginal is 1/2 at every context.

    source
    theorem CSD.RecordLayer.singletJointRates_colSum (a b : LF3.DetectorSetting) (t : Fin 2) :
    (singletJointRates a b).colSum t = 1 / 2

    B's marginal is 1/2 at every context.

    source
    noncomputable def CSD.RecordLayer.singletTables (C : LF3.MeasurementContext) :
    JointRates 2 2

    The singlet's tables, one per context.

    Equations
    Instances For
      source
      theorem CSD.RecordLayer.singletTables_rowSum_eq (a b b' : LF3.DetectorSetting) :
      (singletTables { a := a, b := b }).rowSum = (singletTables { a := a, b := b' }).rowSum

      A's marginal does not depend on B's setting.

      source
      theorem CSD.RecordLayer.singletTables_colSum_eq (a a' b : LF3.DetectorSetting) :
      (singletTables { a := a, b := b }).colSum = (singletTables { a := a', b := b }).colSum

      B's marginal does not depend on A's setting.

      The skew cells carry the singlet's law #

      source
      theorem CSD.RecordLayer.volume_skewCell_singlet (a b : LF3.DetectorSetting) (s t : Fin 2) :
      MeasureTheory.volume (skewCell (singletJointRates a b) s t) = ENNReal.ofReal (LF3.P_st a b (signOfFin s) (signOfFin t))

      ★ The skew cells carry the singlet's joint probabilities exactly.

      ★★★ The instance #

      source
      noncomputable def CSD.RecordLayer.skewLocalSettingLocalityBSinglet :
      LF3.LocalSettingLocalityB MeasureTheory.volume (skewOutcomeMaps singletTables)

      ★★★ The rectangle exchange is a B-wing reroute for the singlet.

      Equations
      Instances For
        source
        noncomputable def CSD.RecordLayer.skewLocalSettingLocalityASinglet :
        LF3.LocalSettingLocalityA MeasureTheory.volume (skewOutcomeMaps singletTables)

        ★★★ The identity is an A-wing reroute for the singlet.

        Equations
        Instances For
          source
          theorem CSD.RecordLayer.operationalNoSignalling_skew_singlet :
          LF3.OperationalNoSignalling MeasureTheory.volume (skewOutcomeMaps singletTables)

          ★★★ The singlet on the I3 record basins is operationally no-signalling, derived from the primitive — on the fibre partition whose cells carry the Bell-violating joint law (volume_skewCell_singlet).