entropyArrowCert
plain-language theorem explainer
The definition assembles a certificate for the thermodynamic arrow of time by populating the EntropyArrowCert structure with the fact that five thermodynamic arrows exist, together with the non-negativity, equilibrium, and time-reversal properties of the J-cost function. Researchers modeling pre-Big Bang physics or the origin of entropy increase would cite this to ground the forward time direction in J-cost minimization toward r=1. The construction is a direct record literal that invokes four sibling results for the four fields.
Claim. The entropy arrow certificate is the structure whose fields are: the cardinality of the set of thermodynamic arrows equals 5; the recognition cost satisfies $J(r)≥0$ for every $r>0$; $J(1)=0$; and $J(r)=J(r^{-1})$ for every $r>0$.
background
The module establishes the thermodynamic arrow of time from the recognition cost J(r), which is minimized at equilibrium r=1 where J=0; evolution drives r toward 1 and thereby defines the forward time direction. J-cost is the function imported from the Cost module whose non-negativity, vanishing at unity, and symmetry J(r)=J(r^{-1}) are proved in the sibling theorems jcost_nonneg, equilibrium_zero, and time_reversal_symmetric. The structure EntropyArrowCert packages these four properties, with the cardinality claim supplied by arrowCount. Upstream, jcost_nonneg is obtained from Cost.Jcost_nonneg and the local jcost_nonneg wrapper that handles the r=1 case via Jcost_unit0.
proof idea
The definition is a one-line record construction that directly assigns the four fields of EntropyArrowCert: five_arrows is taken from arrowCount, nonneg from jcost_nonneg, equilibrium from equilibrium_zero, and time_reversal from time_reversal_symmetric.
why it matters
This definition supplies the single packaged certificate that realizes the four key claims of the module (J-cost non-negative, zero at equilibrium, time-reversal symmetric, and five arrows) and thereby grounds the thermodynamic arrow in Recognition Science. It implements the pre-Big Bang physics setting in which J-cost minimization defines the future direction and equates the number of thermodynamic arrows to configDim D=5. The construction rests on the J-cost theorems from PhysicsComplexityStructure and the Cost module; no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.