le_succ
plain-language theorem explainer
The ordering fact n ≤ succ n holds for every element n of LogicNat, the naturals induced by the Law of Logic. Researchers deriving arithmetic and reachability properties in Recognition Science cite this when establishing basic inequalities on the generator orbit. The term proof supplies the witness succ zero and reduces the equality via the successor addition rule followed by the zero addition identity.
Claim. For every element $n$ of the inductive type of naturals forced by the Law of Logic, $n$ is less than or equal to its successor, where the order is witnessed by addition.
background
LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity) and step (one iteration of the generator), forming the smallest subset of positive reals closed under multiplication by γ and containing 1. The successor operation is the step constructor. This module extracts arithmetic operations and ordering relations as theorems from the inductive structure rather than positing them as axioms. The result depends on the addition lemmas stating that addition distributes over successor and that zero is the additive identity.
proof idea
The proof is a term-mode construction supplying succ zero as the witness for the inequality and verifying the equality n + succ zero = succ n. It applies the rewriting rule from the successor addition lemma followed by the zero addition lemma.
why it matters
This inequality supports transitivity arguments and reachability inclusions, appearing in proofs of lt_trans and in ballP_subset_inBall lemmas within causality and complexity modules. It contributes to the foundation that derives Peano-style arithmetic from the functional equation instead of assuming it. The result underpins later cost-covering and possibility-space constructions without external number axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.