arrow_well_defined
plain-language theorem explainer
The declaration proves that the arrow of time holds between consecutive ledger snapshots on any sequence satisfying DefectMonotone when ticks advance by exactly one. A physicist constructing discrete models of emergent time from recognition events would cite it to equate tick ordering with irreversible defect reduction. The proof is a direct constructor that splits the arrow relation into an index inequality discharged by omega and a defect inequality taken from the hypothesis.
Claim. Let $s : ℕ →$ LedgerSnapshot be a sequence of ledger states. If $h$ is a DefectMonotone structure on $s$ (ticks non-decreasing and defect non-increasing on unit steps) and $n ∈ ℕ$ satisfies the step condition that the tick index of $s_{n+1}$ equals the tick index of $s_n$ plus one, then the arrow-of-time relation holds from $s_n$ to $s_{n+1}$.
background
The TimeEmergence module identifies time with the discrete tick counter on ledger states rather than a continuous background parameter. A LedgerSnapshot packages a Tick (carrying an index) together with a nonnegative real defect that quantifies distance from the cost minimum. The DefectMonotone structure encodes the principle that, inside one epoch, each recognition step advances the tick by one while weakly decreasing defect, thereby supplying the direction of time.
proof idea
The term proof applies the constructor of arrow_of_time. The first conjunct (strict increase of tick index) is discharged by the omega tactic applied to the supplied step hypothesis. The second conjunct (defect non-increase) is obtained exactly by projecting the defect_decreasing field of the DefectMonotone hypothesis h onto n and the step condition.
why it matters
The result discharges F-006 in the time-emergence chain, confirming that temporal order coincides with thermodynamic irreversibility through defect reduction. It rests on the module's identification of time as ledger tick count and on the eight-tick octave (T7) for D=3. No downstream uses appear yet, but the theorem directly supports the irreversibility claim recognition_irreversible listed among the module siblings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.