Documentation

CsdLean4.RecordLayer.DynamicMeasurementClosure

SigmaLayer/DynamicMeasurementClosure: the dynamical capstone (item 8) #

Category: 7-SigmaLayer (the record layer — the capstone).

★ Additive, not destabilising #

The plan is explicit: do not immediately destabilise the working capstone. So FiniteQMClosure is untouched — it still runs on unifiedDeisolationModel / vnPointerOutcome ψ' / preparation-indexed bornRegion, and every one of its theorems stands exactly as before. This file adds a second, independent bundle and a combining capstone; it deprecates nothing and migrates nothing.

⚠️ FiniteQMClosure is operational finite-QM closure, and should be described that way rather than as finite-QM closure simpliciter: its readout is preparation-indexed and its records are not dynamically created. CsdFiniteQMClosure below is what the combined claim looks like.

What is proved #

⚠️ What the combined capstone does and does not assert #

It asserts the two bundles hold. It does not assert they are about the same arena — the operational closure lives on productDynamics over ℂℙ^M × T² and the dynamical one on Σ_sel × T²_R. Unifying the arenas is the engine migration, and is not done. Read CsdFiniteQMClosure as "both hold", not as "one theory covers both".

⚠️ And the standing residue of item 3 is unchanged: the propagator is explicit and every property is proved of it, but the Hamiltonian generation is stated, not formalised. A capstone cannot launder that.

References #

SigmaLayer/FiniteQMClosure.lean (the operational closure, untouched); SigmaLayer/ShearWitness.lean, SigmaLayer/DynamicBorn.lean, SigmaLayer/RecordPersistence.lean.

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

The dynamical measurement closure. The five facts a measurement must exhibit as a process, as against as a partition.

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

    ★ The dynamical measurement closure holds — for every state, with no hypotheses about the dynamics.

    ★ Note what is absent from the hypotheses: CorrelatesOn and PointerInvariantOn do not appear. ShearWitness discharged them from an explicitly constructed propagator, so this bundle rests on a construction rather than on assumed physics. That is the difference between this and every earlier record-layer bundle in the corpus.

    source
    structure CSD.RecordLayer.CsdFiniteQMClosure {Nsys : ℕ} [NeZero Nsys] (ψsys : EuclideanSpace ℂ (Fin Nsys)) {Nsub M : ℕ} [NeZero Nsub] (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (e : Fin Nsub × Fin Nsub ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'0 : ψ' ≠ 0) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) :
    Prop

    The combining capstone: operational finite-QM closure and dynamical measurement.

    ⚠️ It asserts that both bundles hold. It does NOT assert they are about the same arena. The operational closure lives on productDynamics over ℂℙ^M × T² for a composite system indexed by Fin Nsub × Fin Nsub ≃ Fin (M+1); the dynamical one lives on Σ_sel × T²_R in dimension Nsys. The parameter lists are disjoint, and that is not an accident of the encoding — it is the honest state of the corpus. Unifying the arenas is the engine migration, and it is not done.

    Read this as "both hold", not "one theory covers both". A capstone that bundled them while implying otherwise would be exactly the kind of claim this project keeps having to retract.

    Instances For
      source
      theorem CSD.RecordLayer.csdFiniteQMClosure {Nsys : ℕ} [NeZero Nsys] (ψsys : EuclideanSpace ℂ (Fin Nsys)) {Nsub M : ℕ} [NeZero Nsub] (H : Matrix (Fin (M + 1)) (Fin (M + 1)) ℂ) (hH : H.IsHermitian) (p₀ : LF4.CPN (M + 1)) (e : Fin Nsub × Fin Nsub ≃ Fin (M + 1)) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'0 : ψ' ≠ 0) (ψ : EuclideanSpace ℂ (Fin (M + 1))) (hψ0 : ψ ≠ 0) (hψ' : ‖ψ'‖ = 1) (hψ : ‖ψ‖ = 1) :
      CsdFiniteQMClosure ψsys H hH p₀ e ψ' hψ'0 ψ hψ0

      The combining capstone holds.