P5: Dirac index (skeleton with light API)

We model a minimal Fredholm operator with an integer index, a Dirac system carrying such an operator, and provide a zero-order invariance lemma (by definition) together with a placeholder statement for the torus index formula.

structure Frourio.Fredholm : Type

Minimal Fredholm operator model carrying only its index.

• index : ℤ

structure Frourio.ZeroOrderBoundedOp (bundle : Type u_1) : Type

Zero-order bounded perturbations (placeholder over a bundle).

• dummy : Unit

structure Frourio.DiracSystem : Type (max (max (u_1 + 1) (u_2 + 1)) (u_3 + 1))

Dirac system skeleton: base space, torus tag, bundle, connection, and the principal Dirac operator as a Fredholm element. Also stores a placeholder RHS value for the torus index formula (e.g. Chern number).

• M : Type u_1
• isTorus2 : Prop
• bundle : Type u_2
• connection : Type u_3
• D_A : Fredholm
• indexRHS_T2 : ℤ

def Frourio.index (T : Fredholm) : ℤ

Extract the integer index.

Equations

• Frourio.index T = T.index

noncomputable def Frourio.addZeroOrder (S : DiracSystem) (_V : ZeroOrderBoundedOp S.bundle) : Fredholm

Add a zero-order bounded perturbation (skeleton keeps the same Fredholm operator to model invariance at the API level).

Equations

• Frourio.addZeroOrder S _V = S.D_A

@[simp]

theorem Frourio.index_invariance_zero_order (S : DiracSystem) (V : ZeroOrderBoundedOp S.bundle) : index (addZeroOrder S V) = index S.D_A

Index invariance under zero-order bounded perturbations (definitional).

def Frourio.index_formula_T2 (S : DiracSystem) (_hT2 : S.isTorus2) : Prop

Torus index formula placeholder: states equality of the analytical index with a stored RHS (e.g. Chern number) under a torus hypothesis.

Equations

• Frourio.index_formula_T2 S _hT2 = (Frourio.index S.D_A = S.indexRHS_T2)