lspCandidates
plain-language theorem explainer
This definition enumerates the candidate particles for the lightest superpartner under supersymmetry in the Recognition Science setting. A physicist examining dark matter candidates in the odd-phase sector would cite the list when discussing stable particles compatible with the J-cost asymmetry. The declaration is a direct enumeration of three standard phenomenological candidates with no computation or lemmas involved.
Claim. The lightest superpartner candidates are the neutralino (mix of photino, zino, higgsino), the gravitino (superpartner of the graviton), and the axino (superpartner of the axion).
background
Recognition Science derives supersymmetry breaking from differences in J-cost between bosons and fermions that arise from the eight-tick phase structure. The module shows that exact supersymmetry would force equal masses for partners such as the electron and selectron, contradicting observation, so the breaking scale lies above 1 TeV. The lightest superpartner remains stable under R-parity and occupies the dark (odd-phase) sector, making it a dark matter candidate via ledger shadows.
proof idea
This is a direct definition that enumerates three strings naming the candidate particles. No lemmas or tactics are applied; the body is a literal list.
why it matters
The declaration supplies the concrete particle names for the stable lightest superpartner when supersymmetry is assumed inside the Recognition Science framework. It supports the module's claim that supersymmetry is compatible but not required, with the hierarchy problem instead solved by the phi-ladder structure. The list connects to the J-cost asymmetry mechanism and the eight-tick octave (T7) while noting that SUSY is not necessary for gauge unification or dark matter explanations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.