Documentation

CsdLean4.RecordLayer.GlobalBasin

SigmaLayer/GlobalBasin: context-fixed measurement basins on Σ = ℂℙⁿ⁻¹ × T² #

Category: 7-SigmaLayer (the record layer — Paper C A7).

Glossary: https://glossary.constraintsurfacedynamics.com/outcome-region/ and https://glossary.constraintsurfacedynamics.com/epistemic-measure/ Plain-language, CSD-role and formal statements of the outcome regions and the epistemic measure, with this module as their Lean anchor. Kept symmetric by scripts/check-glossary.sh.

The problem this addresses #

Paper C A7 asks for measurement regions Ωᵢ(M) fixed by the apparatus alone. The corpus's record layer does not supply that: its partition is cdfCell (bornRate ψ), built from the preparation. LF4/QubitBorn.lean discharges the genuine context-fixed form at N = 2, and the general-N base-only question is ⏸ parked (specs/sigma-fibre-contextuality.md) — the ContextFixedA7* chain shows a base-only density is heavily constrained, without settling it in either direction.

This file takes the fibred route that chain points at. The construction is due to an external review of 29c6afd:

Bᵢ(M) = {(p, θ₁, θ₂) : θ₁ ∈ circleCell (m_M p) i}

with the rate vector read off at the ontic point p, not at the preparation. No ψ appears anywhere in the definition, so the basin is a function of the context alone — which is what A7 asks.

★ Why this is not circular. One might object that the Born weights are being put in by using the moment map. They are not put in by hand: bornRate_eq_momentMap (SigmaLayer/MomentMapRace.lean) already identifies the record-layer rates with the Fubini–Study torus moment map, forced by the Kähler structure and the Tⁿ action rather than carved to a target.

★ Why it does not collide with the parked N ≥ 3 chain. That chain constrains base-only densities. This partition is genuinely fibred — the cell is an arc in θ₁ — which is exactly where sigma-fibre-contextuality.md concluded contextuality has to live at N ≥ 3.

What is proved #

Scope — read before citing #

⚠️ δ_p ⊗ Haar is the EPISTEMIC measure, not the sector's Liouville measure. Conditioning on a preparation means conditioning on p = [ψ], a null set for μ_FS; the isolation-conditioned state is taken to be the Dirac product outright — the corpus's "isolation is conditioning" reading (P6). a modelling choice stated as a definition, not a theorem SUPERSEDED 2026-08-21 (Q26): the choice is now the theorem epistemicMeasure_eq_disintegration (RecordLayer/EpistemicDisintegration.lean) — kMuL disintegrates along the base projection and its disintegration kernel is μ_FS-a.e. the constant Haar kernel, so δ_p ⊗ Haar is the fibre of the arena's own disintegration, planted at its base point. kMuL = μ_FS ⊗ vol remains the Liouville measure, and nothing here claims δ_p ⊗ Haar is one.

⚠️ This is KINEMATIC. No interaction Hamiltonian H_int(M) generating these basins is constructed — that is the open Paper D obligation (SigmaLayer/DeIsolationFlow.lean), and it is untouched here. A context-fixed partition is not a dynamical account of measurement.

⚠️ A7 at general N is not thereby closed ANSWERED 2026-08-02 (author decision): the fibred reading is canonical, so this construction — with the dynamical layer of v0.7.0 on top — DOES discharge A7 at every N. The parked ContextFixedA7 chain now characterises whether a base-only realisation also exists (the qubit-special-case question); it no longer gates the axiom. See reconstruction-status.md §2.

⚠️ KSigma is still not proved Kähler, and the fibre measure is still exhibited as Haar rather than shown Liouville. See the ★★ specs/BACKLOG.md row.

References #

SigmaLayer/TorusFibre.lean (torusCell, volume_torusCell, loSum_add_self_le_one); LF4/MomentMap.lean (momentMap, measurable_momentMap, momentMap_mk_eq_inner_sq); SigmaLayer/MomentMapRace.lean (bornRate_eq_momentMap — the rates are forced, not carved); LF4/KahlerInstance.lean (KSigma, KTorus); specs/BACKLOG.md (the ★★ row's successor target); specs/sigma-fibre-contextuality.md.

A measurement context as a rate field on the base #

source
structure CSD.RecordLayer.ContextField (N : ℕ) :
Type

A measurement context, as the data it actually contributes: a rate field on the ontic base. The apparatus assigns to each base point p a probability vector over outcomes; the preparation plays no part in the assignment.

This is the object Paper C A7 needs and the corpus's bornContext ψ is not: rate is a function of the ontic point, so any region built from it depends on the context alone.

  • rate : LF4.CPN N → Fin N → ℝ

    The rate assigned to each ontic base point.

  • measurable_rate (i : Fin N) : Measurable fun (p : LF4.CPN N) => self.rate p i

    Each coordinate is measurable — the regularity that makes the basins measurable.

  • nonneg (p : LF4.CPN N) (i : Fin N) : 0 ≤ self.rate p i

    The rates are non-negative.

  • sum_one (p : LF4.CPN N) : ∑ i : Fin N, self.rate p i = 1

    The rates are normalised: the field lands in the simplex.

Instances For
    source
    theorem CSD.RecordLayer.ContextField.loSum_le_one {N : ℕ} (c : ContextField N) (p : LF4.CPN N) (i : Fin N) :
    loSum (c.rate p) i + c.rate p i ≤ 1
    source
    theorem CSD.RecordLayer.ContextField.measurable_loSum {N : ℕ} (c : ContextField N) (i : Fin N) :
    Measurable fun (p : LF4.CPN N) => loSum (c.rate p) i

    p ↦ loSum (rate p) i is measurable: a finite sum of measurable coordinates.

    The basin #

    source
    noncomputable def CSD.RecordLayer.globalBasin {N : ℕ} (c : ContextField N) (i : Fin N) :
    Set (LF4.KSigma N)

    The context-fixed basin of outcome i. A point of Σ = ℂℙⁿ⁻¹ × T² is in the basin when its first torus coordinate lies in the CDF arc determined by the rate field at its own base point.

    The definition mentions no preparation. That is the whole point: Bᵢ is fixed by c, i.e. by the apparatus.

    Equations
    Instances For
      source
      theorem CSD.RecordLayer.measurableSet_globalBasin {N : ℕ} (c : ContextField N) (i : Fin N) :
      MeasurableSet (globalBasin c i)

      The basin is measurable. The three ingredients are the measurability of the canonical representative (measurable_rep), of the rate field (ContextField.measurable_rate), and of its partial sums — combined by measurableSet_lt / measurableSet_le, since the basin is cut out by two inequalities between measurable real functions.

      ⚠️ This is where LF4.measurable_momentMap is needed for the canonical instance; before it was proved, momentMap's definition through the choice-based Projectivization.rep blocked this step.

      source
      theorem CSD.RecordLayer.globalBasin_pairwiseDisjoint {N : ℕ} (c : ContextField N) :
      Pairwise (Function.onFun Disjoint (globalBasin c))

      Distinct outcomes are mutually exclusive. Fibrewise from circleCell_pairwiseDisjoint: at a fixed base point the two arcs are disjoint, and both basins read the same base point.

      Conditioning on the preparation #

      source
      noncomputable def CSD.RecordLayer.epistemicMeasure {N : ℕ} (p : LF4.CPN N) :
      MeasureTheory.Measure (LF4.KSigma N)

      The isolation-conditioned epistemic state at preparation p: the base is known to be p, the fibre microstate is unknown and Haar-distributed.

      ⚠️ This is the epistemic measure, not the Liouville measure kMuL = μ_FS ⊗ vol. Conditioning on p conditions on a μ_FS-null set, so the Dirac product is taken as the definition rather than obtained by disintegration.

      Equations
      Instances For
        source
        instance CSD.RecordLayer.instIsProbabilityMeasureKSigmaEpistemicMeasure {N : ℕ} (p : LF4.CPN N) :
        MeasureTheory.IsProbabilityMeasure (epistemicMeasure p)
        source
        theorem CSD.RecordLayer.preimage_globalBasin {N : ℕ} (c : ContextField N) (i : Fin N) (p : LF4.CPN N) :
        Prod.mk p ⁻¹' globalBasin c i = torusCell (c.rate p) i

        The slice of a basin over its own base point is a torus cell. The bridge between the global basin and TorusFibre's fibrewise statements.

        source
        theorem CSD.RecordLayer.globalBasin_prob {N : ℕ} (c : ContextField N) (i : Fin N) (p : LF4.CPN N) :
        (epistemicMeasure p) (globalBasin c i) = ENNReal.ofReal (c.rate p i)

        ★ Conditioning on the preparation returns the rate. The basin was defined without reference to any preparation; conditioning the epistemic state on p gives it probability rate p i.

        source
        theorem CSD.RecordLayer.globalBasin_ae_total {N : ℕ} (c : ContextField N) (p : LF4.CPN N) :
        (epistemicMeasure p) (Set.univ \ ⋃ (i : Fin N), globalBasin c i) = 0

        A.e. microstate lands in some basin, so the readout is a.e. total.

        The canonical context: the torus moment map #

        source
        noncomputable def CSD.RecordLayer.momentContext (N : ℕ) :
        ContextField N

        The canonical measurement context: the Fubini–Study torus moment map. Its regularity is LF4.measurable_momentMap, its simplex constraints LF4.momentMap_nonneg and LF4.momentMap_sum_eq_one.

        This is the context for a measurement in the standard basis; a general apparatus enters by transporting the base point with the corresponding unitary.

        Equations
        Instances For
          source
          @[simp]
          theorem CSD.RecordLayer.momentContext_rate {N : ℕ} (p : LF4.CPN N) :
          (momentContext N).rate p = LF4.momentMap p
          source
          theorem CSD.RecordLayer.globalBasin_born {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin N) :
          (epistemicMeasure (Projectivization.mk ℂ ψ hψ0)) (globalBasin (momentContext N) i) = ENNReal.ofReal (‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2)

          ★★ The Born rule from a partition that never mentions the preparation.

          At preparation ψ, the epistemic probability of the context-fixed basin Bᵢ is exactly the Born weight ‖⟨eᵢ, ψ⟩‖². The basin is a function of the apparatus context alone (momentContext), the preparation enters only through which point of Σ's base the system is at, and the probability is the Haar measure of an arc in the fibre.

          This is the fibred form of Paper C A7, at every N. ⚠️ It is kinematic: no H_int(M) generating these basins is constructed.