pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Physics.EntropyArrowFromJCost

show as:
view Lean formalization →

The module derives the thermodynamic arrow of time directly from non-negativity of J-cost in Recognition Science. Foundational physicists would cite it when tracing entropy increase to the underlying cost function. The module organizes this via sibling definitions of arrowCount and EntropyArrowCert that build on the imported Cost module.

claimThermodynamicArrow is the direction in which arrowCount increases, certified by EntropyArrowCert when J-cost is nonnegative: $J(x) = (x + x^{-1})/2 - 1$ forces the arrow via jcost_nonneg and equilibrium_zero.

background

Recognition Science defines J-cost in the Cost module as the function J(x) = (x + x^{-1})/2 - 1, which satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). This module imports that definition and introduces the thermodynamic arrow as the cumulative direction of positive J-cost accumulation along the phi-ladder. The local setting uses the eight-tick octave and D = 3 spatial dimensions from the upstream forcing chain.

proof idea

This is a definition module, no proofs. It groups the sibling declarations ThermodynamicArrow, arrowCount, jcost_nonneg, equilibrium_zero, time_reversal_symmetric, and EntropyArrowCert to structure the entropy arrow argument from the Cost import.

why it matters in Recognition Science

The module supplies the explicit link from J-cost non-negativity to the entropy arrow, feeding parent results in the broader physics derivations that close the T0-T8 forcing chain. It fills the step that converts the cost function into time asymmetry, consistent with the alpha band and Berry creation threshold.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)