lt_irrefl
plain-language theorem explainer
Irreflexivity of the strict order on the natural numbers derived from the law of logic: no such number is less than itself. Cited in mutual-exclusion arguments for horizons in climate models, cross-section bands in cosmology, and regimes in economics. The proof assumes an equality via successor addition, maps it to ordinary naturals via the iteration count, and obtains a contradiction with the omega tactic.
Claim. For every natural number $n$ derived from the law of logic, it is not the case that $n < n$, where these numbers are generated inductively by an identity element and a step constructor mirroring the multiplicative orbit, and $<$ denotes the strict order induced by addition of a positive step.
background
The logic-derived natural numbers are defined inductively with an identity constructor representing the zero-cost element and a step constructor representing one iteration of the generator, corresponding to the orbit {1, γ, γ², …} in the positive reals. The successor function applies one step. The iteration-count map sends the identity to zero and each step to the successor in ordinary naturals, with the addition-preservation theorem showing that addition on these numbers corresponds to addition of their counts. This theorem belongs to the module deriving arithmetic from the logic functional equation.
proof idea
The proof assumes for contradiction that n is less than itself, yielding some k such that n plus the successor of k equals n. It applies the iteration-count map to this equality. Rewriting using the addition-preservation and successor-count theorems produces an equation in ordinary naturals where a number plus one equals itself. The omega tactic derives the contradiction.
why it matters
This irreflexivity is invoked to establish that the before relation is irreflexive in the arrow-of-time module and to prove mutual exclusions such as within-horizon and past-horizon states being incompatible, predicted bands excluding falsifiers in dark-matter bounds, and high-mobility and high-inequality regimes being disjoint. It provides a foundational order property for the J-cost gradient and the phi-ladder constructions in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.