Documentation

CsdLean4.SigmaLayer.SectorPostulateNoGo

SigmaLayer/SectorPostulateNoGo: the single-flow limit — a deterministic flow does not pin the sector #

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

The localized sector posit (SO-1) result (SigmaLayer/LocalisedTypicality.lean) shows the typicality measure is forced by the U(N) SYMMETRY. This module makes precise WHY the universal sector origin (SO-1) — deriving the Born measure μ_FS from a single deterministic flow — is not reachable: a single projective flow does not uniquely determine an invariant measure, so it cannot single out μ_FS.

The mechanism: a fixed ray of the flow supports an invariant Dirac measure. A projective unitary flow with two DISTINCT fixed rays therefore has (at least) two distinct invariant probability measures — so its invariant measure is not unique, and at least one of them is not μ_FS (flow_admits_invariant_ne_fubiniStudy). Since a projective flow with an eigen-ray always has such Diracs, and every unitary on ℂ^N (N ≥ 2) has orthogonal eigen-rays (spectral theorem), the conclusion is generic; phaseFlip_admits_invariant_ne_fubiniStudy exhibits it on a concrete NON-trivial flow (the phase-flip diag(1,-1) on ℂℙ¹).

What this establishes #

μ_FS is invariant under the flow (fubiniStudyMeasure_smul_invariant), but it is NOT distinguished among the flow's invariant measures — the flow admits others. So "the CSD sector is posited (SO-1)" is not a temporary formalisation gap but a proved statement about the limit: the deterministic flow underdetermines the sector's typicality measure. Pinning μ_FS needs the full U(N) symmetry (IsForcedKahlerVolume's uniqueness), which a single one-parameter flow does not carry. This matches Paper C (§A/§3.6): Σ, π, and the quantum-effective sector (selected by Axiom A5) are assumed, not derived — the sector's deeper origin (SO-1) is left open.

References: specs/connectivity-manifest.md (L7 / SO-1), specs/reconstruction-status.md (frontier), SigmaLayer/LocalisedTypicality.lean (region_measure_symmetry_forced, the positive companion), LF4/KahlerVolumeForced.lean (IsForcedKahlerVolume).

source
theorem CSD.SigmaLayer.flow_admits_invariant_ne_fubiniStudy {N : ℕ} (p₀ : LF4.CPN N) (V : ↥(Matrix.unitaryGroup (Fin N) ℂ)) {p q : LF4.CPN N} (hpq : p ≠ q) (hp : V • p = p) (hq : V • q = q) :
∃ (μ : MeasureTheory.Measure (LF4.CPN N)), MeasureTheory.IsProbabilityMeasure μ ∧ MeasureTheory.MeasurePreserving (fun (x : LF4.CPN N) => V • x) μ μ ∧ μ ≠ Matrix.UnitaryGroup.fubiniStudyMeasure p₀

The single-flow limit (no-go for universal sector origin (SO-1)). If a projective unitary flow x ↦ V • x fixes two DISTINCT rays p ≠ q, it admits an invariant probability measure that is NOT the Fubini–Study / Born measure. The two fixed-ray Diracs are both invariant and distinct, so at least one differs from μ_FS. Hence the flow does not uniquely determine the sector's typicality measure.

source
noncomputable def CSD.SigmaLayer.phaseFlip :
↥(Matrix.unitaryGroup (Fin 2) ℂ)

The phase-flip unitary diag(1, -1) on ℂ² (a genuine Φ ≠ id element: it fixes the poles [e₀], [e₁] but moves [e₀ + e₁]).

Equations
Instances For
    source
    theorem CSD.SigmaLayer.phaseFlip_smul_single (i : Fin 2) (hi : EuclideanSpace.single i 1 ≠ 0) :
    phaseFlip • Projectivization.mk ℂ (EuclideanSpace.single i 1) hi = Projectivization.mk ℂ (EuclideanSpace.single i 1) hi

    phaseFlip fixes the ray of a standard basis vector.

    source
    theorem CSD.SigmaLayer.phaseFlip_admits_invariant_ne_fubiniStudy (p₀ : LF4.CPN 2) :
    ∃ (μ : MeasureTheory.Measure (LF4.CPN 2)), MeasureTheory.IsProbabilityMeasure μ ∧ MeasureTheory.MeasurePreserving (fun (x : LF4.CPN 2) => phaseFlip • x) μ μ ∧ μ ≠ Matrix.UnitaryGroup.fubiniStudyMeasure p₀

    The no-go on a concrete non-trivial flow. The phase-flip flow x ↦ phaseFlip • x on ℂℙ¹ admits an invariant probability measure other than μ_FS: it fixes the two distinct poles [e₀], [e₁], whose Diracs are invariant and distinct. So even a genuine Φ ≠ id deterministic flow does not pin the Born measure.