SolitonClass
plain-language theorem explainer
Recognition Science admits exactly five topologically distinct soliton classes on the recognition field when the configuration dimension equals five. A physicist classifying stable localized solutions would cite this enumeration to fix the complete set before proving cardinality or certification. The declaration is a direct inductive type with five constructors and automatic derivation of decidable equality together with finiteness.
Claim. Let $S$ be the set of soliton classes consisting of the kink solution of the $phi^4$ theory, the breather solution of the sine-Gordon equation, the soliton solution of the Korteweg-de Vries equation, the soliton solution of the nonlinear Schrödinger equation, and the Skyrmion.
background
The module Soliton Classes from RS asserts that the recognition field supports five canonical soliton classes when the configuration dimension equals five. Each class is described as a topologically distinct stable localized solution. The module states: 'Five canonical soliton classes (= configDim D = 5): kink (φ⁴), breather (sine-Gordon), KdV soliton, NLS soliton, Skyrmion.' No upstream lemmas are required because the declaration introduces the enumeration directly.
proof idea
The declaration is an inductive definition that introduces five constructors corresponding to the listed soliton classes and derives the instances DecidableEq, Repr, BEq, and Fintype automatically.
why it matters
This definition supplies the finite set whose cardinality is certified by the downstream structure SolitonClassCert and proved equal to five by the theorem solitonClass_count. It fills the enumeration step required for soliton classification inside the Recognition Science framework at the point where configDim D = 5 is asserted. The five classes provide concrete realizations of stable solutions that later connect to the forcing chain and the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.