pith. machine review for the scientific record. sign in
theorem proved term proof

hodge_implies_zero_charge

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 154theorem hodge_implies_zero_charge (h : RSHodgeConjecture)
 155    (L : DefectBoundedSubLedger) (cls : CoarseGrainingStableClass L)
 156    (hzero : ∀ (cyc : JCostMinimalCycle L), cyc.cycle_class.z_charge = 0) :
 157    cls.z_charge = 0 := by

proof body

Term-mode proof.

 158  obtain ⟨cycles, hsum⟩ := h L cls
 159  rw [hsum]
 160  simp [hzero]
 161
 162/-! ## Part 4: Connection to Classical Hodge -/
 163
 164/-- The RS framework recovers the classical Hodge (p,p) type condition:
 165    z_charge ≥ 0 is the RS version of the (p,p) Hodge condition.
 166    Classical (p,p) classes have equal holomorphic and antiholomorphic degree. -/

depends on (16)

Lean names referenced from this declaration's body.