theorem proved term proof

`deficitLinearizationCert`

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

formal statement (Lean)

 188theorem deficitLinearizationCert : DeficitLinearizationCert where
 189  linear_vanishes := fun W η => linear_regge_vanishes W η

Term-mode proof.

 190
 191end
 192
 193end DeficitLinearization
 194end Geometry
 195end IndisputableMonolith

Lean names referenced from this declaration's body.

DeficitLinearizationCert in IndisputableMonolith.Geometry.DeficitLinearization decl_use
linear_regge_vanishes in IndisputableMonolith.Geometry.DeficitLinearization decl_use
W in IndisputableMonolith.Masses.Anchor decl_use
W in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
W in IndisputableMonolith.Physics.MassTopology decl_use