Maxwell Dec Equations

Discrete Maxwell equations

Maxwell's equations are the four laws linking electric and magnetic fields to their sources: electric charge and electric current. In their usual continuous form, they are differential equations. The declaration Equations in the Recognition Science library defines a discrete, or mesh-based, version of these laws. Instead of smooth fields, it works with values assigned to the elementary pieces of a subdivided space: points, edges, faces, and volumes. This is the standard setup of discrete exterior calculus, a way to do calculus on a lattice that preserves the geometric meaning of the original operations.

The discrete equations mirror the continuous ones. Faraday's law becomes the statement that the discrete curl of the electric field is zero, meaning no time-varying magnetic field in the quasistatic limit. Gauss's law for magnetism states that the discrete divergence of the magnetic field is zero, so there are no magnetic monopoles. The remaining two laws, Ampère's law and Gauss's law for electricity, relate the fields to the current and charge sources through the Hodge star, a discrete version of the metric that encodes the geometry of the mesh. These two, along with the constitutive relations linking the electric and magnetic fields to the medium, require the space to have exactly three dimensions for the mathematical pieces to line up correctly.

The framework also defines a measure of field energy density on each two-dimensional face. A proved theorem in the library, energy2_nonneg_pointwise, states that for a medium with positive electric permittivity and magnetic permeability, this energy density is never negative at any point. This is a sanity check: the discrete model does not produce negative energy, a property that holds regardless of the metric signature, whether the mesh represents a Riemannian or a Lorentzian spacetime.

In Recognition Science, this declaration is a ledger, a discrete record of events, for electromagnetism. It is a definitional choice, a model, not a derived theorem. The library uses it as a bridge between the abstract forcing chain that produces three spatial dimensions and the concrete physics of electric and magnetic fields on a lattice. The declaration does not, by itself, prove that Maxwell's equations are the only possible ones, nor does it derive the values of the constants involved. It provides a formal, machine-checked vocabulary for stating and reasoning about these equations in a discrete setting.

/-- Quasi-static Maxwell equations on the mesh (no time derivative terms).
    Faraday and Gauss-M are stated cleanly. Constitutive relations (const_D, const_B)
    and source equations (ampere_qs, gauss_e) require dimension n=3 for form-degree
    alignment, so they are parameterized by the dimension hypothesis `hn`. -/
structure Equations (α : Type) [HasCoboundary α] [inst : HasHodge α] (M : Medium α) where
  E : DForm α 1
  H : DForm α 1
  B : DForm α 2
  D : DForm α 2
  src : Sources α
  /-- Faraday QS: curl E = 0 (no time-varying B in quasistatic limit) -/
  faraday_qs : HasCoboundary.d E = fun _ => 0
  /-- Ampere QS: d H = star J (requires n-1=2 for form-degree alignment) -/
  ampere_qs  : ∀ (hn : inst.n - 1 = 2),
    HasCoboundary.d H = cast (congrArg (DForm α) hn) (HasHodge.star src.J)
  /-- Gauss E: d D = star rho (requires n-0=3 for form-degree alignment) -/
  gauss_e    : ∀ (hn : inst.n - 0 = 3),
    HasCoboundary.d D = cast (congrArg (DForm α) hn) (HasHodge.star src.ρ)
  /-- Gauss M: div B = 0 (no magnetic monopoles) -/
  gauss_m    : HasCoboundary.d B = fun _ => 0
  /-- Constitutive: D = ε⋆E (requires n-1=2 for form-degree alignment) -/
  const_D    : ∀ (hn : inst.n - 1 = 2), D = hn ▸ (fun s => M.eps * HasHodge.star E s)
  /-- Constitutive: B = μ⋆H (requires n-1=2 for form-degree alignment) -/
  const_B    : ∀ (hn : inst.n - 1 = 2), B = hn ▸ (fun s => M.mu * HasHodge.star H s)

/-- Positivity of the Hodge energy density for admissible media, provided the
    instance supplies `star2_psd`. This is signature-agnostic and delegates the
    sign choice to the instance via `star2_psd`. -/
theorem energy2_nonneg_pointwise
  [inst : HasHodge α] (h : inst.n - 2 = 2) (M : Medium α) (hadm : Admissible (α:=α) M) (ω : DForm α 2)
  : ∀ s, 0 ≤ energy2 (α:=α) ω h s := by
  intro s
  have hpsd := HasHodge.star2_psd (α:=α) h ω s
  simp [energy2]
  exact hpsd

/-- Quasi-static Maxwell equations on the mesh (no time derivative terms).
    Faraday and Gauss-M are stated cleanly. Constitutive relations (const_D, const_B)
    and source equations (ampere_qs, gauss_e) require dimension n=3 for form-degree
    alignment, so they are parameterized by the dimension hypothesis `hn`. -/
structure Equations (α : Type) [HasCoboundary α] [inst : HasHodge α] (M : Medium α) where
  E : DForm α 1
  H : DForm α 1
  B : DForm α 2
  D : DForm α 2
  src : Sources α
  /-- Faraday QS: curl E = 0 (no time-varying B in quasistatic limit) -/
  faraday_qs : HasCoboundary.d E = fun _ => 0
  /-- Ampere QS: d H = star J (requires n-1=2 for form-degree alignment) -/
  ampere_qs  : ∀ (hn : inst.n - 1 = 2),
    HasCoboundary.d H = cast (congrArg (DForm α) hn) (HasHodge.star src.J)
  /-- Gauss E: d D = star rho (requires n-0=3 for form-degree alignment) -/
  gauss_e    : ∀ (hn : inst.n - 0 = 3),
    HasCoboundary.d D = cast (congrArg (DForm α) hn) (HasHodge.star src.ρ)
  /-- Gauss M: div B = 0 (no magnetic monopoles) -/
  gauss_m    : HasCoboundary.d B = fun _ => 0
  /-- Constitutive: D = ε⋆E (requires n-1=2 for form-degree alignment) -/
  const_D    : ∀ (hn : inst.n - 1 = 2), D = hn ▸ (fun s => M.eps * HasHodge.star E s)
  /-- Constitutive: B = μ⋆H (requires n-1=2 for form-degree alignment) -/
  const_B    : ∀ (hn : inst.n - 1 = 2), B = hn ▸ (fun s => M.mu * HasHodge.star H s)

What this page does not claim

This declaration does not prove that Maxwell's equations are the only possible set of electromagnetic laws. The declaration does not derive the numerical values of the speed of light or the fine-structure constant. The discrete equations are quasistatic and do not include time-derivative terms for wave propagation.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/MaxwellDEC.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: