Physics Soliton Classes From Rs

Soliton classes

A soliton is a localized wave that keeps its shape while it travels. In classical physics, the best-known examples are the kink, the breather, the Korteweg-de Vries (KdV) soliton, the nonlinear Schrödinger (NLS) soliton, and the Skyrmion. Each arises in a different equation: the kink in φ⁴ field theory, the breather in sine-Gordon theory, the KdV soliton in shallow water waves, the NLS soliton in optical fibers, and the Skyrmion in nuclear physics as a model of the nucleon. These five are not a random list; each is a topologically distinct stable solution of its governing equation, meaning small perturbations do not destroy it.

The history runs deep. John Scott Russell first observed a solitary wave on a canal in 1834, chasing it on horseback. Diederik Korteweg and his student Gustav de Vries wrote the equation that bears their names in 1895. The term soliton was coined in 1965 by Norman Zabusky and Martin Kruskal. The sine-Gordon equation and its breather solutions came from field theory in the 1960s and 1970s, and Tony Skyrmion's proposal of the Skyrmion as a model of the nucleon dates to 1961. Each of these discoveries was independent, and each produced a stable, localized solution to a different nonlinear equation.

In Recognition Science, the framework packages these five classical soliton classes as a single family. The framework's library, a machine-checked collection of formal theorems, defines an inductive type with exactly these five members: kink, breather, KdV soliton, NLS soliton, and Skyrmion. A theorem in the library proves that the number of these classes is exactly five. This is a combinatorial fact about the framework's own classification, not a claim that no other soliton exists in physics. The framework models the five as topologically distinct stable localized solutions on its recognition field, which is a discrete record of events. The library's proof is axiom-clean, meaning it relies only on the standard logical postulates of the ambient type theory, with no special axioms added.

The payoff is a single organizing statement: the five canonical soliton classes that physics discovered separately, over more than a century, are exactly the five members of one finite family in the framework. This does not explain why each equation has its soliton, nor does it prove that the list is complete for all of physics. What it does is give a compact, machine-checked certificate that the classical five form a closed set under the framework's classification. A reader who knows the classical solitons can now see them as one family, and a reader who meets the framework first can find the classical examples waiting inside it.

inductive SolitonClass where
  | kinkPhi4
  | breatherSineGordon
  | kdvSoliton
  | nlsSoliton
  | skyrmion
  deriving DecidableEq, Repr, BEq, Fintype

theorem solitonClass_count : Fintype.card SolitonClass = 5 := by decide

inductive SolitonClass where
  | kinkPhi4
  | breatherSineGordon
  | kdvSoliton
  | nlsSoliton
  | skyrmion
  deriving DecidableEq, Repr, BEq, Fintype

What this page does not claim

The framework does not prove that these five are the only solitons in all of physics. The framework does not derive the equations (φ⁴, sine-Gordon, KdV, NLS, Skyrme) from first principles. The framework does not claim that the classical solitons are physically identical to its recognition field objects.

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/Physics/SolitonClassesFromRS.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: