Mathematics Partial Differential Equations From Rs Partial Differential Equation

The five-type certificate

Partial differential equations (PDEs) are equations that relate a function to its own rates of change. They are the language of field physics: Laplace's equation describes equilibrium, the heat equation describes diffusion, and the wave equation describes propagation. A standard classification groups these into five families: elliptic, parabolic, hyperbolic, mixed, and integro-differential. The elliptic family includes Laplace's equation, where the sum of second derivatives is zero. Parabolic equations, like the heat equation, smooth out irregularities over time. Hyperbolic equations, like the wave equation, carry signals at finite speed. Mixed types combine features of several families, and integro-differential equations also involve integrals of the unknown function.

The classification is classical, but counting the families is a discrete fact: there are exactly five. The Recognition Science framework encodes this count in a machine-checked library of formal theorems. Its declaration PartialDifferentialEquationsCert is a certificate that the number five is correct. The certificate is a structure whose only field is a proof that the type PDEType, which lists the five families, has cardinality five. The proof is checked by the kernel, with no unproved assumptions and no axioms beyond the ambient type theory. This is a theorem in the sense that the count is formally verified, not a claim about the physical origin of the equations.

The framework's own vocabulary connects the five families to its core concept of recognition, a discrete record of events. In this account, physical laws are PDEs on the recognition field: the Laplace equation is the cost potential at equilibrium, the heat equation is cost diffusion, and the wave equation is cost propagation. These identifications are definitional choices, not consequences of the certificate. The certificate itself only counts the types; it does not prove that any particular equation is a recognition field equation, nor that the five families exhaust all possible PDEs.

What the certificate does not claim is as important as what it proves. It does not derive the classification from first principles; it assumes the five families as a definition. It does not show that the five types correspond to physical phenomena; that is a modeling decision. It does not prove that any PDE solves a recognition problem; the certificate is silent on solutions. The count is a small, exact fact: five families, verified by computation. It is a building block, not a theory of PDEs.

structure PartialDifferentialEquationsCert where
  five_types : Fintype.card PDEType = 5

theorem pdeTypeCount : Fintype.card PDEType = 5 := by decide

What this page does not claim

The certificate does not derive the five PDE families from physics or from the forcing chain. It does not prove that any specific equation is a recognition field equation. It does not claim that the five families exhaust all possible partial differential equations.

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/Mathematics/PartialDifferentialEquationsFromRS.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: