le
plain-language theorem explainer
The definition introduces non-strict order on LogicNat by requiring an additive increment k such that n + k equals m. Arithmetic foundations in Recognition Science cite this when proving inequalities for J-cost minima and phi-ladder comparisons. It is realized as a direct existential definition over the addition operation already built from the inductive LogicNat type.
Claim. For $n, m$ in the inductive type LogicNat, $n$ is less than or equal to $m$ when there exists $k$ in LogicNat satisfying $n + k = m$.
background
LogicNat is the inductive type with constructors identity (zero-cost multiplicative identity) and step (one generator iteration), mirroring the orbit {1, γ, γ², ...} as the smallest subset of positive reals closed under multiplication by γ and containing 1. The module ArithmeticFromLogic derives addition and other arithmetic from this structure via the Law of Logic. The upstream LogicNat result supplies the two-constructor inductive foundation on which the order is defined.
proof idea
The definition is a direct one-line existential quantification over the addition already constructed on LogicNat, with no lemmas or tactics applied.
why it matters
This order definition feeds 40 downstream results, including path interpolation in Action.PathSpace, heat factor bounds in ContinuumLimit2D, the kappa_einstein_eq relation, Hubble resolution theorem, phi_power_matches_eta for baryon asymmetry, and jcost_energy_min_at_ground. It completes the arithmetic layer required for the Recognition Science forcing chain, enabling comparisons that support the eight-tick octave and phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.