lemma proved wrapper

`G_zero_of_unit`

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

formal statement (Lean)

  51lemma G_zero_of_unit (F : ℝ → ℝ) (hUnit : F 1 = 0) : G F 0 = 0 := by

One-line wrapper that applies simpa.

  52  simpa [G] using hUnit
  53

From the project-wide theorem graph. These declarations reference this one in their body.

normalized_implies_G_zero in IndisputableMonolith.Cost.FunctionalEquation decl_use
washburn_uniqueness in IndisputableMonolith.Cost.FunctionalEquation decl_use
washburn_uniqueness_aczel in IndisputableMonolith.Cost.FunctionalEquation decl_use
T5_uniqueness_complete in IndisputableMonolith.CostUniqueness decl_use
full_inevitability_explicit in IndisputableMonolith.Foundation.DAlembert.FullUnconditional decl_use
full_unconditional_inevitability in IndisputableMonolith.Foundation.DAlembert.FullUnconditional decl_use

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use