Documentation

CsdLean4.RecordLayer.SwapClosure

SigmaLayer/SwapClosure: all six dynamical facts on ONE arena #

Category: 7-SigmaLayer (the record layer — arena unification, step 1 of 2).

Why #

DynamicMeasurementClosure was honest about a split: its ready/record/persistence/Born fields were shear-protocol statements on Σ_sel × T²_R, while its Lüders field was a swap-protocol statement on the bank-augmented SwapArena. The external review (2026-08-02) correctly listed "package all six facts on the swap arena alone" as the precursor to the engine migration. This module does that:

Two genuine upgrades over the shear-side bundle, beyond the arena move:

What remains for the engine migration (step 2, recorded) #

The operational closure (FiniteQMClosure) still lives on productDynamics over ℂℙ^M × T². CsdFiniteQMClosure remains a conjunction over two arenas; this module removes the split within the dynamical bundle only. See specs/BACKLOG.md.

References #

SigmaLayer/DynamicMeasurementClosure.lean (the predecessor bundle, untouched); SigmaLayer/SwapWitness.lean (swapProtocol, selReadyBank, swap_correlates, swap_pointerInvariant); SigmaLayer/SwapLuders.lean (swap_luders_born); SigmaLayer/MeasurementProtocol.lean (measure_outcomeSector_eq_of_correlates); SigmaLayer/DynamicBorn.lean (basinIndex, measure_basinIndex_fibre); Empirical/CSD/SequentialMeasurement.lean (the empirical consumer); specs/BACKLOG.md.

The canonical preparation and its bank #

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

The canonical sequential-round preparation: system at the ontic point p, register in the ready arc. (Moved from Empirical/CSD/SequentialMeasurement.lean, 2026-08-02 — it is SigmaLayer machinery.)

Equations
Instances For
    source
    instance CSD.RecordLayer.instIsProbabilityMeasureProdKSigmaKTorusReadyPrep {N : ℕ} (p : LF4.CPN N) :
    MeasureTheory.IsProbabilityMeasure (readyPrep p)
    source
    noncomputable def CSD.RecordLayer.calibratedBank (N : ℕ) [NeZero N] :
    MeasureTheory.Measure (Fin N → LF4.KSigma N)

    The vertex-calibrated ancilla bank of the swap witness.

    Equations
    Instances For
      source
      instance CSD.RecordLayer.instIsProbabilityMeasureForallFinKSigmaCalibratedBank {N : ℕ} [NeZero N] :
      MeasureTheory.IsProbabilityMeasure (calibratedBank N)
      source
      noncomputable def CSD.RecordLayer.swapPrep {N : ℕ} [NeZero N] (p : LF4.CPN N) :
      MeasureTheory.Measure (SwapArena (LF4.KSigma N) N)

      The full swap-arena preparation: system-and-register at readyPrep p, bank calibrated.

      Equations
      Instances For
        source
        instance CSD.RecordLayer.instIsProbabilityMeasureSwapArenaKSigmaSwapPrep {N : ℕ} [NeZero N] (p : LF4.CPN N) :
        MeasureTheory.IsProbabilityMeasure (swapPrep p)

        hpos as a theorem (moved from the empirical layer) #

        source
        theorem CSD.RecordLayer.readyMeasure_readyArc (K : ℕ) :
        (readyMeasure K) (readyArc K) = 1

        The ready arc has full conditional measure.

        source
        theorem CSD.RecordLayer.prep_outcome_pos {N : ℕ} [NeZero N] (p : LF4.CPN N) (i : Fin N) (hpos : LF4.momentMap p i ≠ 0) :
        (readyPrep p) ((shearProtocol (basinIndex (momentContext N)) ⋯).outcomeSector i) ≠ 0

        hpos is a theorem for the canonical ready preparation. The outcome-i sector has nonzero measure whenever the Born weight momentMap p i is nonzero: the selector-and-ready set sits inside the sector (shear_correlates) and factors as (basin fibre) × (ready arc), both of nonzero measure. Generalises vertex_outcome_pos. (Moved from Empirical/CSD/SequentialMeasurement.lean, 2026-08-02.)

        The selector-and-ready-and-bank partition, measured #

        source
        theorem CSD.RecordLayer.measurableSet_selReadyBank {N : ℕ} [NeZero N] (c : ContextField N) (i : Fin N) :
        MeasurableSet (selReadyBank (basinIndex c) i)
        source
        theorem CSD.RecordLayer.selReadyBank_pairwiseDisjoint {N : ℕ} [NeZero N] (c : ContextField N) :
        Pairwise (Function.onFun Disjoint (selReadyBank (basinIndex c)))
        source
        theorem CSD.RecordLayer.swapPrep_selReadyBank {N : ℕ} [NeZero N] (p : LF4.CPN N) (i : Fin N) :
        (swapPrep p) (selReadyBank (basinIndex (momentContext N)) i) = ENNReal.ofReal (LF4.momentMap p i)

        The canonical preparation weights the selector-and-ready-and-bank set with exactly the Born weight.

        source
        theorem CSD.RecordLayer.swapPrep_selReadyBank_cover {N : ℕ} [NeZero N] (p : LF4.CPN N) :
        ∑ i : Fin N, (swapPrep p) (selReadyBank (basinIndex (momentContext N)) i) = 1

        The dynamical Born on the swap arena #

        source
        theorem CSD.RecordLayer.swap_sector_born {N : ℕ} [NeZero N] (p : LF4.CPN N) (i : Fin N) :
        (swapPrep p) ((swapProtocol (basinIndex (momentContext N)) ⋯).outcomeSector i) = ENNReal.ofReal (LF4.momentMap p i)

        ★ The dynamical Born weight, on the swap arena. The measure of the outcome-i sector — the initial states destined to display record i — equals the Born weight momentMap p i, for every preparation. Proved through measure_outcomeSector_eq_of_correlates, so the correlation theorem (swap_correlates) is genuinely consumed: this is Born as a consequence of the dynamics, stated where the Lüders update also lives.

        The dynamical Born for an arbitrary context (Q25, 2026-08-21) #

        The two-time composition (RecordLayer/TwoTimeLuders.lean) needs the sector Born for the SECOND measurement's context, which is arbitrary. The assembly is swap_sector_born's, with globalBasin_prob consumed at a general ContextField — the momentContext statement above stays as the canonical special case.

        source
        theorem CSD.RecordLayer.swapPrep_selReadyBank_ctx {N : ℕ} [NeZero N] (c : ContextField N) (p : LF4.CPN N) (i : Fin N) :
        (swapPrep p) (selReadyBank (basinIndex c) i) = ENNReal.ofReal (c.rate p i)

        The canonical preparation weights the selector-and-ready-and-bank set of an ARBITRARY context with that context's rate. Generalises swapPrep_selReadyBank.

        source
        theorem CSD.RecordLayer.swapPrep_selReadyBank_cover_ctx {N : ℕ} [NeZero N] (c : ContextField N) (p : LF4.CPN N) :
        ∑ i : Fin N, (swapPrep p) (selReadyBank (basinIndex c) i) = 1
        source
        theorem CSD.RecordLayer.swap_sector_born_ctx {N : ℕ} [NeZero N] (c : ContextField N) (p : LF4.CPN N) (i : Fin N) :
        (swapPrep p) ((swapProtocol (basinIndex c) ⋯).outcomeSector i) = ENNReal.ofReal (c.rate p i)

        ★ The dynamical Born weight for an arbitrary context, on the swap arena. The measure of the outcome-i sector of the swap protocol built on ANY context field c equals that context's rate at the preparation — swap_sector_born with the context general. This is what lets a SECOND measurement, in whatever basis, read its Born weights off the relocated state (RecordLayer/TwoTimeLuders.lean).

        The closure: six facts, one arena, one preparation #

        source
        structure CSD.RecordLayer.SwapMeasurementClosure (N : ℕ) [NeZero N] (ψ : EuclideanSpace ℂ (Fin N)) :
        Prop

        The swap-arena measurement closure. The six dynamical facts, every one a statement about swapProtocol on SwapArena at the canonical preparation swapPrep [ψ] — the single-arena bundle DynamicMeasurementClosure could not honestly be.

        Instances For
          source
          theorem CSD.RecordLayer.swapMeasurementClosure {N : ℕ} [NeZero N] (ψ : EuclideanSpace ℂ (Fin N)) :
          SwapMeasurementClosure N ψ

          ★ The swap-arena closure holds — for every state, with CorrelatesOn and PointerInvariantOn proved of the constructed propagator, never assumed.