theorem proved term proof

`polyCost_zero`

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

formal statement (Lean)

  91@[simp] theorem polyCost_zero : polyCost (0 : Polynomial F) = 0 := by

Term-mode proof.

  92  unfold polyCost
  93  simp [normalizedFactors_zero]
  94

Lean names referenced from this declaration's body.

polyCost in IndisputableMonolith.NumberTheory.PrimeCostSpectrumPoly decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use