theorem proved term proof

`hodge_structure`

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

formal statement (Lean)

  19theorem hodge_structure : hodge_from_ledger := bsd_structure

Term-mode proof.

  20
  21/-- Hodge-structure scaffold implies BSD-side structural input. -/

Lean names referenced from this declaration's body.

bsd_structure in IndisputableMonolith.Mathematics.BirchSwinnertonDyerStructure decl_use
hodge_from_ledger in IndisputableMonolith.Mathematics.HodgeConjectureStructure decl_use