arrowCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove physical existence or observability of any listed arrow.
- Does not derive the five arrows from the J-uniqueness formula or phi fixed point.
- Does not connect the count to the Recognition Composition Law or the eight-tick octave.
- Does not address the separate spatial dimension D = 3 from the forcing chain.
Lean usage
have h : Fintype.card ThermodynamicArrow = 5 := arrowCountformal statement (Lean)
30theorem arrowCount : Fintype.card ThermodynamicArrow = 5 := by decide
proof body
31