succ_le_succ
plain-language theorem explainer
The successor on the naturals forced by the law of logic preserves the order relation. Researchers deriving arithmetic and reachability from the Recognition functional equation cite this when establishing monotonicity for induction or ball constructions. The term proof destructures the order witness k and rewrites the equality via the successor-addition identity.
Claim. Let $N_L$ be the naturals forced by the law of logic, generated by the orbit under the generator with successor $S$. If $a, b$ satisfy $a + k = b$ for some $k$ in $N_L$, then $S(a) + k = S(b)$.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost multiplicative identity in the orbit) and step (one iteration of the generator), forming the smallest subset of positive reals closed under multiplication by the generator and containing 1. Successor is defined as one further application of the step constructor. The order $a ≤ b$ is witnessed by existence of an additive element $k$ such that $a + k = b$ (as used in the destructuring step of the proof).
proof idea
The proof obtains the witness $k$ from the hypothesis $a ≤ b$. It then supplies the same $k$ for the conclusion and reduces the required equality $S(a) + k = S(b)$ by applying the successor-addition lemma, which rewrites the left side to $S(a + k)$ and matches the original witness.
why it matters
This result supplies the monotonicity step needed by ballP_subset_inBall in the causality modules and by clay_bridge_theorem together with main_resolution in the complexity bridge. It belongs to the arithmetic-from-logic chain that derives Peano properties as theorems rather than axioms, feeding later order and induction arguments before the framework reaches J-uniqueness and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.