lt_iff_le_and_ne
plain-language theorem explainer
The equivalence between strict inequality and the conjunction of weak inequality with distinctness holds for the natural numbers induced by the logic functional equation. Researchers deriving Peano structure inside Recognition Science cite this when verifying order axioms from the orbit construction. The proof splits the biconditional via constructor, derives a contradiction in one direction by applying the iteration-count embedding, and performs case analysis on the difference in the other.
Claim. For elements $a, b$ in the logic natural numbers, $a < b$ if and only if $a ≤ b$ and $a ≠ b$.
background
LogicNat is the inductive type whose constructors identity and step encode the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by the self-similar fixed point γ. The successor operation is the single application of the step constructor. The map toNat sends identity to 0 and step n to the successor of toNat n; it is additive and commutes with successor. The upstream results toNat_add and toNat_succ supply the embedding properties used to transport contradictions between the two number systems.
proof idea
Constructor splits the biconditional. Forward direction assumes a difference expressed with succ, builds the weak inequality, then applies congrArg toNat together with toNat_add and toNat_succ to reach succ k = 0, contradicting the inductive structure. Reverse direction assumes a difference k and distinctness, cases on k: the identity case yields immediate equality contradicting distinctness, while the step case extracts the required predecessor.
why it matters
The result is invoked directly by le_antisymm to conclude equality from mutual inequalities, completing the order axioms on the logic naturals. This arithmetic layer supplies the counting structure required by the Recognition Composition Law and the phi-ladder mass assignments that appear later in the forcing chain (T5–T8). No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.