DefectMonotone
plain-language theorem explainer
DefectMonotone encodes the non-increasing defect condition on sequences of ledger snapshots. It requires non-decreasing tick indices together with defect reduction on every unit tick advance. Researchers deriving the arrow of time from ledger updates cite this structure to formalize irreversibility within an epoch. The definition directly packages the two properties without invoking lemmas or reductions.
Claim. A sequence of ledger snapshots $(s_n)_{n∈ℕ}$ is defect-monotone when the tick index of $s_n$ is at most the tick index of $s_{n+1}$ for every $n$, and whenever the tick index increases by exactly one, the defect value of $s_{n+1}$ is at most the defect value of $s_n$.
background
The TimeEmergence module identifies time with the discrete ledger tick counter rather than a continuous background parameter. Each LedgerSnapshot pairs a Tick (whose index supplies the ordering) with a nonnegative defect value; the defect functional is taken from the Law of Existence as the J-cost on positive reals. The module states that the minimal complete update period is the eight-tick octave arising from D=3 spatial dimensions.
proof idea
As a structure definition, DefectMonotone directly records the two field predicates: tick_ordered asserts non-decreasing indices, while defect_decreasing asserts the conditional reduction on unit steps. No upstream lemmas are applied; the declaration is the formal statement of the non-increasing defect principle.
why it matters
DefectMonotone supplies the hypothesis for the downstream theorem arrow_well_defined, which establishes that the arrow of time is well-defined once defect decreases along the sequence. It realizes the F-006 claim that recognition is irreversible because defect can only decrease toward the cost minimum. In the Recognition framework this anchors the thermodynamic arrow to the eight-tick octave and the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.