SREffect
plain-language theorem explainer
The inductive enumeration of special relativity effects lists the five canonical phenomena that arise from the Recognition Science J-cost function. Researchers working on the derivation of special relativity within the Recognition Science framework cite this enumeration when establishing that the effects satisfy the rest-frame equilibrium and motion-cost conditions. The definition proceeds by introducing five constructors and deriving a Fintype instance to support cardinality statements.
Claim. The inductive type enumerating the canonical special-relativistic effects consists of five constructors corresponding to time dilation, length contraction, mass-energy equivalence, relativity of simultaneity, and velocity addition.
background
The module establishes special relativity from Recognition Science by requiring that the J-cost function obeys J(1) = 0 at the rest frame (recognition equilibrium) and J(r) > 0 for any r ≠ 1 that represents motion. J-cost measures the recognition cost of a velocity ratio r = v/c. The module documentation states that the five canonical effects correspond to a configuration dimension of five.
proof idea
The declaration is an inductive definition that introduces five named constructors and derives the Fintype instance. No lemmas or tactics are invoked; the structure itself directly enables the cardinality computation used downstream.
why it matters
This supplies the effect enumeration required by the special relativity certification structure to assert that exactly five effects satisfy Jcost 1 = 0, positive cost for motion, and symmetry under inversion. It realizes the module claim that five canonical SR effects equal configDim D = 5. In the Recognition Science framework the enumeration links J-cost properties to standard relativistic phenomena.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.