EntropyArrowCert
plain-language theorem explainer
The EntropyArrowCert structure collects the four defining properties of the recognition cost function that establish a thermodynamic arrow of time in Recognition Science. Researchers modeling pre-Big-Bang physics or the emergence of irreversibility cite it when linking J-cost minimization to the five distinct arrows. The declaration is a structure definition that directly assembles the cardinality of the arrow type with non-negativity, zero at equilibrium, and time-reversal symmetry of J.
Claim. Let $J$ denote the recognition cost function. The structure EntropyArrowCert asserts that the inductive type of thermodynamic arrows has cardinality five, that $J(r)geq 0$ for all $r>0$, that $J(1)=0$, and that $J(r)=J(r^{-1})$ for all $r>0$.
background
In the module on the arrow of time from J-cost, recognition cost $J(r)$ is minimized at equilibrium $r=1$ where $J=0$. Evolution toward this minimum defines the forward time direction. The type ThermodynamicArrow is the inductive enumeration with constructors thermodynamic, cosmological, causal, psychological, and quantum, whose Fintype.card equals five. The upstream equilibrium theorem states that Jcost 1 = 0, supplying one field directly. The module imports the Cost library for the Jcost definition and Mathlib for Fintype and real-number operations.
proof idea
The declaration is a structure definition with an empty proof body. It simply declares the four fields that any instance must satisfy. The five_arrows field relies on the Fintype instance derived from the inductive ThermodynamicArrow; the equilibrium field imports the upstream theorem Jcost 1 = 0; the remaining two fields are stated as quantified propositions over the reals.
why it matters
This structure bundles the four key claims listed in the module documentation and is instantiated downstream by entropyArrowCert using arrowCount, jcost_nonneg, equilibrium_zero, and time_reversal_symmetric. It realizes the Recognition Science claim that J-cost non-negativity and symmetry produce the thermodynamic arrow of time, with the five arrows corresponding to configuration dimension five. The declaration closes the pre-BB physics scaffolding by supplying a single object that encodes the arrow-of-time properties without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.