Inversion Symmetry & Even Ground State

Formalizes Corollary 16: the ground-state eigenfunction is even.

Reference: lamportform.tex, lines 1559–1676.

Section 1: Reflection operator

def ConnesLean.reflectionOp (φ : ℝ → ℂ) : ℝ → ℂ

Reflection operator: (Rφ)(u) = φ(-u).

Equations

• ConnesLean.reflectionOp φ u = φ (-u)

@[simp]

theorem ConnesLean.reflectionOp_apply (φ : ℝ → ℂ) (u : ℝ) : reflectionOp φ u = φ (-u)

@[simp]

theorem ConnesLean.reflectionOp_reflectionOp (φ : ℝ → ℂ) : reflectionOp (reflectionOp φ) = φ

Section 2: Symmetric interval and ae helper

theorem ConnesLean.logInterval_neg_mem {L x : ℝ} (hx : x ∈ logInterval L) : -x ∈ logInterval L

theorem ConnesLean.ae_neg {f g : ℝ → ℂ} (h : f =ᵐ[MeasureTheory.volume] g) : (fun (x : ℝ) => f (-x)) =ᵐ[MeasureTheory.volume] fun (x : ℝ) => g (-x)

Almost-everywhere transfer through negation: if f =ᵐ g then f ∘ Neg.neg =ᵐ g ∘ Neg.neg, using the neg-invariance of Lebesgue measure.

Section 3: Resolvent-reflection axiom

axiom ConnesLean.resolvent_commutes_reflection (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) (φ : ℝ → ℂ) : ∀ᵐ (x : ℝ), (kato_operator cutoffLambda hLam).resolvent (reflectionOp φ) x = reflectionOp ((kato_operator cutoffLambda hLam).resolvent φ) x

Resolvent commutes with reflection (Proposition 14). The resolvent (A_λ + I)⁻¹ commutes with the reflection operator R defined by (Rφ)(u) = φ(-u).

The mathematical argument (lamportform.tex, lines 1559–1618):

1. The energy form satisfies E(Rφ, Rψ) = E(φ, ψ) (reflection invariance)
2. By polarization and the Kato representation theorem, the operator A_λ commutes with R
3. Therefore the resolvent (A_λ + I)⁻¹ commutes with R

Why axiom: Steps 1-3 require bilinear form polarization identity, Kato representation theorem, and resolvent functional calculus — none in Mathlib.

Soundness: Sole precondition 1 < cutoffLambda. Conclusion is a nontrivial a.e. equality between two function compositions that cannot be vacuously satisfied. Precondition: 1 < cutoffLambda.

theorem ConnesLean.ae_of_ae_neg {P : ℝ → Prop} (h : ∀ᵐ (x : ℝ), P x) : ∀ᵐ (x : ℝ), P (-x)

Almost-everywhere transfer of predicates through negation: if P holds a.e. then P ∘ Neg.neg holds a.e.

Section 4: Reflected eigenfunction is eigenfunction

theorem ConnesLean.reflection_eigenfunction (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) : have gs := ground_state_exists cutoffLambda hLam; have T := kato_operator cutoffLambda hLam; ∀ᵐ (x : ℝ), T.resolvent (reflectionOp gs.eigenfunction) x = (1 / (gs.eigenvalue + 1)) • reflectionOp gs.eigenfunction x

The reflected ground-state eigenfunction R(ψ) satisfies the same resolvent eigenvalue equation as ψ. This chains the resolvent-reflection axiom with the ground-state resolvent eigenvalue equation transferred through negation.

Section 5: Even ground state

theorem ConnesLean.ground_state_even (cutoffLambda : ℝ) (hLam : 1 < cutoffLambda) : reflectionOp (ground_state_exists cutoffLambda hLam).eigenfunction =ᵐ[MeasureTheory.volume] (ground_state_exists cutoffLambda hLam).eigenfunction

Ground state is even (Corollary 16). The ground-state eigenfunction ψ satisfies ψ(-u) = ψ(u) a.e.

Reference: lamportform.tex, Corollary 16 (lines 1648–1676).

Section 6: Soundness tests