lt
plain-language theorem explainer
Defines strict less-than on LogicNat by existence of a positive difference expressed via successor. Cited in antisymmetry proofs for the induced order and in establishing explicit phi-power numerical bounds. The definition is a direct existential wrapper over the addition operation and the successor constructor.
Claim. For $n, m$ in the logic naturals, $n < m$ holds precisely when there exists $k$ in the logic naturals such that $n +$ successor of $k$ equals $m$.
background
LogicNat is the inductive type whose constructors are identity (the zero-cost multiplicative identity) and step (one further iteration of the generator), realizing the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by γ. The module ArithmeticFromLogic constructs addition, order, and induction theorems directly from the functional equation without external axioms. The companion definition le states that $n ≤ m$ when there exists any $k$ with $n + k = m$; succ is the one-line wrapper .step n.
proof idea
One-line definition that applies the existential quantifier to the sum of n with the successor of k.
why it matters
Supplies the strict order required by le_antisymm (same module) and by the concrete bounds phi^(-58) < 7.57e-13 and rung_gap_is_seven_halves in the neutrino sector. It completes the arithmetic layer that feeds the phi-ladder mass formula and the eight-tick octave structure derived from the Recognition functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.