arrowCount
plain-language theorem explainer
The theorem establishes that the inductive type of thermodynamic arrows contains exactly five elements. Researchers modeling the arrow of time via J-cost minimization cite this enumeration when connecting entropy increase to the five listed directions. The proof is a one-line decision procedure that exhausts the finite constructors of the inductive definition.
Claim. The finite cardinality of the set of thermodynamic arrows is five: $|$ {thermodynamic, cosmological, causal, psychological, quantum} $| = 5$.
background
The module develops the thermodynamic arrow of time from recognition cost J(r), which is minimized at equilibrium r = 1 where J = 0. Evolution that decreases J defines the forward direction, with J symmetric under r to r inverse. The upstream inductive definition lists exactly five cases and automatically derives Fintype, Repr, and DecidableEq.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute the cardinality by enumerating the five constructors of the inductive type.
why it matters
This count supplies the five_arrows field inside the entropyArrowCert definition that assembles the full certification of J-cost properties. It implements the module claim that five arrows equal configDim D = 5 and links J-cost non-negativity and equilibrium to the arrow of time. The result sits downstream of the forcing chain landmarks but does not yet derive the count from T5 J-uniqueness or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.