srEffectCount
plain-language theorem explainer
The theorem establishes that the Recognition Science cost function generates exactly five canonical special-relativistic effects. Researchers deriving Lorentz invariance from the single J-functional equation would cite this enumeration when listing the effects that follow from J(1) = 0 and divergence at c. The proof is a one-line decision procedure that counts the constructors of the finite inductive type SREffect.
Claim. The finite set of special-relativistic effects generated by the recognition cost function has cardinality five: $ |SREffect| = 5 $, where the elements are time dilation, length contraction, mass-energy equivalence, relative simultaneity, and velocity addition.
background
The module derives special relativity from the Recognition Science cost function J. The upstream equilibrium theorem states that Jcost 1 = 0, confirming the rest frame as recognition equilibrium. Module documentation lists the five canonical effects that arise once J(v/c) diverges at the speed of light and J is symmetric under sign flip of velocity.
proof idea
The proof is a term-mode application of the decide tactic. SREffect carries DecidableEq, Repr, BEq, and Fintype instances, so decide computes the cardinality directly by enumerating its five constructors.
why it matters
The result populates the five_effects field of the downstream specialRelativityCert definition. It realizes the module claim that five effects correspond to configDim D = 5, linking the enumeration to the Recognition Science forcing chain (T0-T8) and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.