theorem proved term proof

`mkSampledMesh_charge_zero`

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

formal statement (Lean)

 124theorem mkSampledMesh_charge_zero (cert : ZeroWindingCert) (N : ℕ) :
 125    ∀ n, ((mkSampledMesh cert N).rings n).winding = 0 :=

proof body

Term-mode proof.

 126  (mkSampledMesh cert N).charge_zero
 127
 128/-! ### §5. Bridge to AnnularTrace -/
 129
 130/-- Build an `AnnularTrace` from a `ZeroWindingCert`: a refinement family
 131of zero-charge meshes at every depth N. -/

depends on (12)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
winding in IndisputableMonolith.Masses.Ribbons decl_use
AnnularTrace in IndisputableMonolith.NumberTheory.AnnularCost decl_use
ZeroWindingCert in IndisputableMonolith.NumberTheory.EulerCarrierComplex decl_use
mkSampledMesh in IndisputableMonolith.NumberTheory.SampledTrace decl_use
refinement in IndisputableMonolith.Papers.DraftV1 decl_use
Bridge in IndisputableMonolith.RecogSpec.Core decl_use