ThermodynamicArrow
plain-language theorem explainer
ThermodynamicArrow enumerates five distinct arrows of time arising from J-cost minimization in pre-Big Bang physics. Researchers modeling entropy increase or time asymmetry in Recognition Science cite it when establishing the count of arrows or bundling their shared properties. The declaration is a direct inductive construction that derives decidable equality and finite cardinality instances automatically.
Claim. An inductive type enumerating the five arrows of time with constructors for the thermodynamic, cosmological, causal, psychological, and quantum cases.
background
The module derives the thermodynamic arrow from recognition cost J(r), which satisfies J(r) ≥ 0 for all r > 0 and reaches its global minimum J(1) = 0 at equilibrium. Forward time is defined by the drive toward this minimum, while the symmetry J(r) = J(r^{-1}) encodes time-reversal invariance. The module states that these considerations produce exactly five arrows, matching a configuration dimension of 5.
proof idea
This declaration is an inductive definition introducing five named constructors and a deriving clause that installs DecidableEq, Repr, BEq, and Fintype instances without further tactics or lemmas.
why it matters
The definition supplies the finite set required by the downstream theorem arrowCount, which establishes cardinality exactly 5, and by the structure EntropyArrowCert, which packages the count together with non-negativity of J-cost, vanishing at equilibrium, and time-reversal symmetry. It realizes the module claim that five arrows correspond to configDim D = 5 and connects to J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.