Mathematics Partial Differential Equations From Rs Pdetype

The fivefold classification

A partial differential equation (PDE) relates a function to its own rates of change in more than one variable. The classical taxonomy sorts these equations into five families: elliptic, parabolic, hyperbolic, mixed, and integro-differential. The Laplace equation, which describes steady states like the shape of a stretched membrane, is the model elliptic case. The heat equation, governing diffusion of temperature, is parabolic. The wave equation, which carries vibrations through a medium, is hyperbolic. Mixed types combine features of the others, and integro-differential equations include an integral alongside the derivatives.

This fivefold division is not arbitrary. Each family has its own characteristic behavior, its own boundary conditions that make a problem well-posed, and its own typical solution methods. Elliptic problems tend to be smooth and determined by their boundary; parabolic problems smooth out over time; hyperbolic problems propagate sharp signals. A century of analysis has built distinct toolkits around each class, and the names appear throughout physics and engineering.

In Recognition Science, the framework models physical laws as PDEs on its recognition field, a field that records the cost of recognizing events. The framework's machine-checked library of formal theorems declares an inductive type called PDEType with exactly those five constructors: elliptic, parabolic, hyperbolic, mixed, and integroDifferential. A companion theorem proves that the number of constructors is five. That is the entire content of the declaration: it fixes the classification as a finite set of five named types.

The declaration does not say which PDE describes any particular physical situation. It does not derive the Laplace, heat, or wave equations from the framework's cost function. It does not assert that the five types exhaust all possible PDEs in some deeper sense. It only records that the framework's classification contains five members, mirroring the classical taxonomy.

What the declaration changes is vocabulary. Within the framework, a statement about elliptic or hyperbolic behavior can refer back to this formal list, and the count of five is available as a proved fact rather than a convention. The physical content, which equation applies where, remains a separate question.

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

What this page does not claim

The declaration does not derive the Laplace, heat, or wave equations from the framework's cost function. The declaration does not assert that the five types exhaust all possible PDEs in a deeper mathematical sense. The declaration does not assign any PDE type to a specific physical situation.

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: