740noncomputable def eulerZeroTrace : AnnularTrace where 741 charge := 0
proof body
Definition body.
742 mesh := fun N => uniformChargeMesh N 0 743 charge_spec := by 744 intro N 745 simp [uniformChargeMesh] 746 747/-- The Euler carrier admits a concrete realizable `BudgetedCarrier` witness: 748the zero-charge trace has zero annular excess, so the excess budget is 749uniformly bounded with budget constant `0`. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.