time_reversal_symmetric
plain-language theorem explainer
The declaration establishes that recognition cost is invariant under inversion of its positive real argument. Physicists constructing the entropy arrow certificate in pre-Big Bang models cite this result to confirm time-reversal symmetry among the five arrows. The proof is a direct one-line application of the core J-cost symmetry lemma.
Claim. For every positive real number $r > 0$, the recognition cost satisfies $J(r) = J(r^{-1})$.
background
Recognition cost $J(r)$ quantifies recognition effort and attains its global minimum of zero at equilibrium ($r = 1$). The module shows that evolution drives $r$ toward 1, thereby defining the forward time direction, and lists five thermodynamic arrows (thermodynamic, cosmological, causal, psychological, quantum) that equal configDim $D = 5$. The local setting requires four properties: non-negativity, equilibrium zero, inversion symmetry, and the arrow count.
proof idea
The proof is a one-line wrapper that applies the Jcost_symm lemma to the positivity hypothesis.
why it matters
This supplies the time-reversal field required by entropyArrowCert, which bundles the five arrows with non-negativity and equilibrium. It completes the symmetry claim stated in the module documentation and supports the Recognition Science construction of the thermodynamic arrow from J-cost. The result sits inside the forcing chain that derives $D = 3$ and the five-arrow count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.