Positivity Improving Semigroup & Ground State

Formalizes Proposition 13 and its Perron-Frobenius consequences.

Reference: lamportform.tex, lines 1462–1556.

Section 1: Positivity-improving predicate

def ConnesLean.IsPositivityImproving (cutoffLambda : ℝ) (T : KatoOperator cutoffLambda) : Prop

Resolvent positivity improving: the resolvent (A_λ + I)⁻¹ maps nonneg, nonzero, real-valued functions to strictly positive functions a.e. on I.

Resolvent positivity improving is equivalent to semigroup positivity improving via the Laplace transform representation. Uses logInterval (= Ioo (-L) L) matching Stage 6 conventions.

Reference: lamportform.tex, Proposition 13, Step 4 (line 1502).

Equations

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

Section 2: Ground state structure

structure ConnesLean.GroundState (cutoffLambda : ℝ) (T : KatoOperator cutoffLambda) : Type

Ground state data for A_λ: an eigenvalue μ₀ ≥ 0 and eigenfunction ψ₀ that is strictly positive a.e., simple, and satisfies the resolvent eigenvalue equation (A_λ + I)⁻¹ψ₀ = (1/(μ₀+1))ψ₀.

Reference: lamportform.tex, Proposition 13 consequence (lines 1530–1556).

• eigenvalue : ℝ
• eigenfunction : ℝ → ℂ
• eigenvalue_nonneg : 0 ≤ self.eigenvalue
• eigenfunction_in_domain : self.eigenfunction ∈ formDomain cutoffLambda
• eigenfunction_nonzero : ∃ (x : ℝ), self.eigenfunction x ≠ 0
• eigenfunction_pos_ae : ∀ᵐ (x : ℝ), x ∈ logInterval (Real.log cutoffLambda) → 0 < (self.eigenfunction x).re
• resolvent_eigenvalue : ∀ᵐ (x : ℝ), T.resolvent self.eigenfunction x = (1 / (self.eigenvalue + 1)) • self.eigenfunction x
• eigenvalue_simple (g : ℝ → ℂ) : (∀ᵐ (x : ℝ), T.resolvent g x = (1 / (self.eigenvalue + 1)) • g x) → ∃ (c : ℂ), ∀ᵐ (x : ℝ), g x = c • self.eigenfunction x

Section 3: Semigroup positivity improving (axiom)

axiom ConnesLean.semigroup_positivity_improving (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) : IsPositivityImproving cutoffLambda (kato_operator cutoffLambda hLam)

Semigroup positivity improving (Proposition 13). The translation semigroup T(t) = e^{-tA_λ} is positivity improving.

The mathematical argument chains four deep results:

1. Markov property (energyForm_comp_normalContraction_le, Stage 4) → Dirichlet form (FOT Definition 1.4.1)
2. m-sectoriality → holomorphic semigroup (Kato, Theorem IX.1.24)
3. Sub-Markov semigroup + irreducibility (semigroup_irreducible, Stage 6) → positivity improving (ABHN Theorem 2.3)
4. Resolvent = Laplace transform of semigroup → resolvent positivity improving

Why axiom: Requires Dirichlet form ↔ semigroup correspondence (FOT 1.4.1) and the Arendt-Batty-Hieber-Neubrander positivity theorem (ATG 2.3), neither available in Mathlib.

Soundness: Sole precondition 1 < cutoffLambda follows existing axiom convention. The conclusion IsPositivityImproving is non-trivially satisfiable: it requires the resolvent to map nonneg nonzero inputs to strictly positive outputs a.e. Precondition: 1 < cutoffLambda.

Section 4: Ground state existence (axiom)

axiom ConnesLean.ground_state_simple (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) (h_pos : IsPositivityImproving cutoffLambda (kato_operator cutoffLambda hLam)) : GroundState cutoffLambda (kato_operator cutoffLambda hLam)

Simple ground state (Perron-Frobenius, ATG Proposition 2.4). Positivity improving + compact resolvent → A_λ has a simple ground state: the bottom of the spectrum μ₀ ≥ 0 is a simple eigenvalue with a strictly positive eigenfunction.

Why axiom: Requires the abstract Perron-Frobenius theorem for positivity-improving semigroups on L² spaces (ATG Proposition 2.4). This is a deep result in positive operator semigroup theory not available in Mathlib.

Soundness: Takes IsPositivityImproving as an explicit hypothesis, which is non-trivially constructible (requires axiom 1 above). The GroundState conclusion has 7 nontrivial fields including domain membership, strict positivity a.e., resolvent eigenvalue equation, and simplicity. Preconditions: 1 < cutoffLambda and IsPositivityImproving.

Section 5: Main theorem

def ConnesLean.ground_state_exists (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) : GroundState cutoffLambda (kato_operator cutoffLambda hLam)

Ground state existence (Proposition 13 + Perron-Frobenius). The operator A_λ has a simple ground state with strictly positive eigenfunction.

Chains axiom 1 (positivity improving) into axiom 2 (Perron-Frobenius).

Reference: lamportform.tex, lines 1530–1556.

Equations

• ConnesLean.ground_state_exists cutoffLambda hLam = ConnesLean.ground_state_simple cutoffLambda hLam ⋯

Section 6: Soundness tests