lt_irrefl
plain-language theorem explainer
LogicNat numbers satisfy irreflexivity of the strict order. Cosmology and climate models cite this to establish mutual exclusion of contradictory states such as a quantity being both within and past a horizon. The proof reduces the assumption to a numerical contradiction on the underlying Nat via the toNat embedding and the omega tactic.
Claim. For every $n$ in the orbit of natural numbers generated by the logic law, it is not the case that $n < n$.
background
LogicNat is the inductive type with constructors identity (zero-cost element) and step (one iteration of the generator), mirroring the orbit {1, γ, γ², ...} as the smallest subset of positive reals closed under multiplication by γ and containing 1. The map toNat sends identity to 0 and step n to Nat.succ (toNat n). Addition on LogicNat is defined so that toNat respects it: toNat (a + b) = toNat a + toNat b. The strict order < on LogicNat is witnessed by existence of k such that n + succ k = n.
proof idea
Assume n < n, so there exists k with n + succ k = n. Apply toNat to obtain toNat n + Nat.succ (toNat k) = toNat n after rewriting with toNat_add and toNat_succ. This equation is impossible on Nat, hence contradiction by omega.
why it matters
This irreflexivity is invoked by before_irrefl to show the before relation is irreflexive, and by horizon_states_exclusive, regimes_exclusive, and band_excludes_falsifier to derive contradictions from overlapping states. It supplies the order axiom needed for the arithmetic layer derived from the functional equation before the forcing chain reaches T5 J-uniqueness and T8 D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.