Equations
plain-language theorem explainer
Equations defines the structure of quasi-static Maxwell equations on an abstract mesh with coboundary and Hodge operators. Discrete electromagnetism modelers and recognition-science derivations of field equations would reference this for the parameterized form-degree constraints under n=3. The declaration is a pure structure definition with no proof obligations.
Claim. Let $n$ be the dimension, $d$ the coboundary operator, and $⋆$ the Hodge star on discrete forms over a type equipped with these operators. Let $M$ be a medium with permittivity $ε$ and permeability $μ$. An instance consists of 1-forms $E,H$, 2-forms $B,D$, and sources $ρ,J$ satisfying $dE=0$, $dB=0$, $dH=⋆J$ when $n=3$, $dD=⋆ρ$ when $n=3$, $D=ε⋆E$ when $n=3$, and $B=μ⋆H$ when $n=3$.
background
DForm α k denotes the space of discrete k-forms, assigning a real value to each oriented k-simplex. HasCoboundary provides the coboundary operator d mapping k-forms to (k+1)-forms with the zero-preservation property. HasHodge supplies the Hodge star operator ⋆ mapping k-forms to (n-k)-forms together with linearity, zero preservation, and the involution law ⋆⋆ = signature(k) · id. Medium encodes the linear constitutive parameters ε and μ. Sources bundles the charge density ρ (0-form) and current density J (1-form). The module sets the local context of oriented simplices with these operators.
proof idea
The declaration is a structure definition with no proof body.
why it matters
This structure supplies the discrete quasi-static Maxwell system that feeds into the d'Alembert status and ODE uniqueness results in the meta-axioms layer. It realizes the electromagnetic sector of the recognition framework by embedding the constitutive and source relations under the dimension hypothesis n=3, aligning with the forced D=3 spatial dimensions from the eight-tick octave. The parent results are ode_cosh_uniqueness and the d'Alembert_status axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.