solitonClass_count
plain-language theorem explainer
Exactly five soliton classes arise as topologically distinct localized solutions in the Recognition Science framework. Modelers of stable field configurations cite this enumeration when classifying defects such as kinks and Skyrmions. The proof reduces to a decision procedure that counts the constructors of the finite inductive type.
Claim. The set of soliton classes has cardinality five: $|$kink in $phi^4$, breather in sine-Gordon, KdV soliton, NLS soliton, Skyrmion$| = 5$.
background
The module introduces five canonical soliton classes (= configDim D = 5) as topologically distinct stable localized solutions on the recognition field: kink ($phi^4$), breather (sine-Gordon), KdV soliton, NLS soliton, and Skyrmion. SolitonClass is the inductive type whose constructors are kinkPhi4, breatherSineGordon, kdvSoliton, nlsSoliton, and skyrmion, deriving Fintype to support direct cardinality computation. This enumeration occurs inside the Recognition Science derivation of physics from one functional equation, where the classes label distinct topological defects.
proof idea
The proof invokes the decide tactic, which exhausts the Fintype instance derived from the inductive definition of SolitonClass and returns the cardinality five.
why it matters
This theorem supplies the five_classes field inside the solitonClassCert definition, confirming the enumeration of soliton types. It fills the listing step in the physics depth module and aligns with the forcing chain landmarks that fix D = 3 spatial dimensions and the eight-tick octave. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.