Documentation

ConnesLean.Stage6.Irreducibility

Semigroup Irreducibility #

Wraps the invariant ideal null-or-conull result into a semigroup irreducibility predicate, plus one axiom recording the Schaefer classification of closed ideals.

Reference: lamportform.tex, Proposition 10 (line 1442), Corollary 15 (lines 1455–1460).

Section 1: Irreducibility predicate #

source
structure ConnesLean.IsSemigroupIrreducible (cutoffLambda : ℝ) :
Prop

Semigroup irreducibility: every EnergyFormSplit has trivial B (either null or conull in the log-interval).

Reference: lamportform.tex, Corollary 15 (line 1455).

Instances For

    Section 2: Proposition 10 conclusion #

    source
    theorem ConnesLean.invariant_ideal_trivial {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) (inv : EnergyFormSplit cutoffLambda) :
    MeasureTheory.volume inv.B = 0 ∨ MeasureTheory.volume (logInterval (Real.log cutoffLambda) \ inv.B) = 0

    Proposition 10 conclusion. Every invariant ideal B arising from an EnergyFormSplit is either null or conull.

    Reference: lamportform.tex, Proposition 10 (line 1442).

    Section 3: Closed ideal classification axiom #

    source
    axiom ConnesLean.closed_ideal_classification (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) (B : Set ℝ) (hB_meas : MeasurableSet B) (hB_sub : B ⊆ logInterval (Real.log cutoffLambda)) (hB_inv : IndicatorTranslationInvariant B (logInterval (Real.log cutoffLambda)) (2 * Real.log cutoffLambda)) :
    ∃ (inv : EnergyFormSplit cutoffLambda), inv.B = B

    Closed ideal classification (Schaefer III.1 + Lemma 14 bridge). If B ⊆ I is measurable and 1_B is translation-invariant on I, then there exists an EnergyFormSplit with that B.

    The mathematical argument (lamportform.tex, Steps 2–6 of Lemma 14) derives energy splitting from semigroup invariance via: (1) Laplace transform → resolvent commutativity, (2) spectral functional calculus → A_λ^{1/2} commutativity, (3) Pythagorean theorem → energy splitting.

    Why axiom: Requires Bochner integration of operator-valued semigroups and Borel functional calculus for unbounded self-adjoint operators, neither available in Mathlib.

    Soundness: The IndicatorTranslationInvariant hypothesis prevents inconsistency: without it, one could produce EnergyFormSplit for arbitrary measurable B ⊆ I, proving every such B is null or conull (contradicting Lebesgue measure). The invariance guard restricts to genuinely semigroup-invariant ideals. Preconditions are 1 < cutoffLambda, MeasurableSet B, B ⊆ I, and IndicatorTranslationInvariant B I ε.

    Section 4: Corollary 15 #

    source
    theorem ConnesLean.semigroup_irreducible {cutoffLambda : ℝ} (hLam : 1 < cutoffLambda) :
    IsSemigroupIrreducible cutoffLambda

    Corollary 15: Semigroup irreducibility. The translation semigroup on L²(I) is irreducible: every EnergyFormSplit has trivial B.

    Direct from the proof chain (does not use the axiom).

    Reference: lamportform.tex, Corollary 15 (lines 1455–1460).

    Section 5: Soundness tests #