SolitonClassCert
plain-language theorem explainer
SolitonClassCert is a structure that certifies the inductive type of soliton classes has exactly five elements. Physicists classifying stable localized solutions in recognition science cite it to record the complete enumeration of kink, breather, KdV, NLS, and Skyrmion types. The definition is a bare structure whose single field is populated downstream by a cardinality count.
Claim. A structure $SolitonClassCert$ whose field asserts that the finite set of soliton classes satisfies $|SolitonClass| = 5$, where $SolitonClass$ is the inductive type whose constructors are the kink-phi4, sine-Gordon breather, KdV soliton, NLS soliton, and Skyrmion.
background
The module enumerates five canonical soliton classes as topologically distinct stable localized solutions on the recognition field. The upstream inductive definition lists the constructors kinkPhi4, breatherSineGordon, kdvSoliton, nlsSoliton, and skyrmion, and derives Fintype so that cardinality statements become available. This supplies the concrete list that the certificate structure merely records.
proof idea
Structure definition whose single field requires the cardinality of the SolitonClass inductive type to equal five. The field value is supplied by the downstream construction solitonClassCert that invokes the count lemma solitonClass_count.
why it matters
SolitonClassCert supplies the certified count of five classes that is consumed by the definition solitonClassCert in the same module. It closes the enumeration step that aligns with the recognition science claim of five canonical classes arising from the recognition field, supporting any later argument that treats these five topologically distinct solutions as exhaustive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.