SigmaLayer/TheoremTargets: the quantum reconstruction targets as uninhabited predicates

Category: 7-SigmaLayer (the projective-sector layer (Paper C)).

The quantum content of the reconstruction (Born rule, unitary and Schrödinger dynamics, ergodic frequency convergence, Lüders update, no-signalling, Bell) is represented as well-typed Prop predicates, NOT as axioms and NOT as structure fields. A target predicate is not a postulate: it is a statement whose inhabitants are theorems to be proved for concrete models. This module defines the targets whose types are supported by the current SigmaLayer core; the measurement- and composition-dependent targets (Lüders update, no-signalling, contextuality, Bell) are defined in their own modules once the DeisolationModel and CompositeSector types exist.

We deliberately provide no inhabitants of these predicates here. Concrete proofs live with the concrete models (see SigmaLayer/LiftedMeasurement.lean and SigmaLayer/ForwardCapstone.lean, and the existing LF4/LF5/LF6 theorems they connect to).

def CSD.SigmaLayer.BornFromVolume {N : ℕ} {Sigma : Type u} [MeasurableSpace Sigma] [Nonempty Sigma] {D : ConstraintDynamics Sigma} (Q : ProjectiveSector N D) (P : Preparation D) {ι : Type u_1} (region : ι → Set (ProjectiveState N)) (weight : ι → ENNReal) : Prop

T1: Born from volume. The projective preparation law assigns each outcome region its Born weight. Generic over the region/weight family; instantiated against the LF4 Born regions and weights in concrete models.

Equations

• CSD.SigmaLayer.BornFromVolume Q P region weight = ∀ (i : ι), (Q.projectivePreparationLaw P) (region i) = weight i

def CSD.SigmaLayer.BornFromFlow {Sigma : Type u} [MeasurableSpace Sigma] (D : ConstraintDynamics Sigma) (region : Set Sigma) (value : ENNReal) : Prop

T3: Born from deterministic flow. For almost every initial ontic state (with respect to muL), the time average along the flow trajectory of the outcome-region indicator converges to the region's measure. The ergodic route to Born frequencies for a single deterministic trajectory.

Equations

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

def CSD.SigmaLayer.IsErgodicForOutcomeRegions {Sigma : Type u} [MeasurableSpace Sigma] (D : ConstraintDynamics Sigma) : Prop

B7 (ergodic branch): the flow is ergodic on the outcome regions. Every measurable set invariant under the time-1 flow map, among the relevant sigma-algebra, is null or co-null under muL. Defined, not assumed. BornFromFlow WOULD follow from this together with the pointwise (Birkhoff) ergodic theorem — which Mathlib does not have (SigmaLayer/UniqueErgodicity.lean names the gap precisely), so NOTHING in the corpus proves BornFromFlow, conditionally or otherwise; T3 is open (= the SO-1 face, reconstruction-status.md T3/L7). (Corrected 2026-08-13: this line previously said "is proved from this ... in concrete models" — prose stronger than the corpus; the contradictions sweep caught it against UniqueErgodicity.lean's honest note.)

Equations

• CSD.SigmaLayer.IsErgodicForOutcomeRegions D = ∀ (A : Set Sigma), MeasurableSet A → D.flow 1 ⁻¹' A = A → ↑D.muL A = 0 ∨ ↑D.muL Aᶜ = 0

def CSD.SigmaLayer.HasUnitaryRealisation {N : ℕ} (projectedFlow : OnticTime → ProjectiveState N → ProjectiveState N) : Prop

T4: the projected flow has a unitary realisation. There is a one-parameter family of unitary matrices whose projective action equals the projected flow at every time.

Equations

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

def CSD.SigmaLayer.HasHamiltonianRealisation {N : ℕ} (projectedFlow : OnticTime → ProjectiveState N → ProjectiveState N) : Prop

T5: Hamiltonian (Schrödinger) realisation. The unitary family is generated by a Hermitian operator, U t = exp(-i t H) (reusing the existing schrodingerUnitary).

Equations

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

def CSD.SigmaLayer.HasProjectivePushforward {N : ℕ} {Sigma : Type u} [MeasurableSpace Sigma] {D : ConstraintDynamics Sigma} (Q : ProjectiveSector N D) (targetMeasure : MeasureTheory.Measure (ProjectiveState N)) : Prop

B1: the ontic measure pushes forward to a target projective measure. Named bridge assumption: pi_* muL = targetMeasure. Proved for concrete product models (see SigmaLayer/MeasureBridge.lean).

Equations

• CSD.SigmaLayer.HasProjectivePushforward Q targetMeasure = (MeasureTheory.Measure.map Q.pi ↑D.muL = targetMeasure)