Maxwell Dec Simplex

The discrete cell

In geometry, a simplex is the simplest possible shape in a given number of dimensions: a point in zero dimensions, a line segment in one, a triangle in two, a tetrahedron in three. A mesh, the kind used in computer graphics or numerical physics, is built by gluing many such shapes together. The declaration Simplex in the framework's machine-checked library of formal theorems defines what a simplex is for its own calculations: an abstract identifier plus a single orientation flag, a boolean that records which way the shape is considered to face. This is a definitional choice, not a mathematical discovery; it sets up the vocabulary for everything that follows.

The point of fixing an orientation is that it lets the framework talk about discrete versions of calculus. A discrete k-form, defined in the same file, is simply a rule that assigns a real number to every oriented k-simplex. The declaration also sets up two interfaces that act like the two sides of a coin. The first, HasCoboundary, provides an operator that takes a form on k-simplices and produces a form on (k+1)-simplices, the discrete analogue of taking a derivative. The second, HasHodge, provides the Hodge star, which in this setting is a linear map that acts as a stand-in for the metric and the material properties of a medium. The framework keeps these interfaces abstract, so that a concrete mesh can choose its own geometric or physical interpretation.

These definitions are the scaffolding for a discrete version of Maxwell's equations, the classical laws of electromagnetism. The file goes on to define a medium by its permittivity and permeability, sources of charge and current, and a structure that holds the equations themselves. The equations are stated in a quasi-static limit, meaning they omit time-derivative terms, and they require the dimension of the mesh to be three for the form degrees to line up correctly. The framework also proves one substantive theorem here: for a medium with strictly positive material parameters, the pointwise Hodge energy density of a 2-form is always non-negative. This is a small but meaningful result, a guarantee that the discrete energy behaves as physical intuition expects.

In Recognition Science, this declaration is a foundational brick, not a grand conclusion. It establishes the language of discrete geometry that the framework's larger claims about physics build upon, but it does not itself derive any physical law or constant. It is a definitional starting point, a way of saying: here is how we will name the cells of our mesh, here is how we will orient them, and here is the machinery we will use to do calculus on them.

/-- Oriented k-simplex (abstract id). -/
structure Simplex (α : Type) (k : Nat) where
  id     : α
  orient : Bool

/-- Discrete k-form: value per oriented k-simplex. -/
@[simp] def DForm (α : Type) (k : Nat) := Simplex α k → ℝ

/-- 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

What this page does not claim

This declaration does not derive Maxwell's equations from more basic principles. It does not specify a particular metric or physical interpretation for the Hodge star. It does not establish the three-dimensionality of physical space.

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: