StringMode
plain-language theorem explainer
The inductive definition enumerates five string modes in the Recognition Science model: tachyon-suppressed, massless, massive, winding, and momentum. Researchers modeling tachyon-free spectra would cite it to fix the mode space at cardinality five. It is a direct enumeration that automatically derives decidable equality and finite type structure from the constructors.
Claim. The string modes form the finite set consisting of the five elements tachyon-suppressed, massless, massive, winding, and momentum.
background
In the Recognition Science framework the tachyon-free condition is the absence of modes with negative J-cost, where the cost function satisfies J(x) ≥ 0 for all x > 0. The module therefore states that the RS recognition field excludes tachyons at the Lagrangian level. Five canonical modes are introduced to realize a configuration dimension of five.
proof idea
The declaration is a direct inductive definition of the five modes. It derives DecidableEq, Repr, BEq, and Fintype automatically. The winding constructor references the upstream net-winding definition on the eight-tick clock, which sums +1 or -1 according to direction.
why it matters
This definition supplies the mode space whose cardinality is certified as five by the downstream stringModeCount theorem. That theorem in turn populates the TachyonFreeCert structure, which asserts five modes together with non-negative J-cost and zero cost for the massless state. It fills the S7 string-theory depth of the module and supports the claim that J ≥ 0 yields a tachyon-free spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.