zero_le
plain-language theorem explainer
zero_le states that the zero element is minimal in the ordering on LogicNat. Researchers deriving arithmetic from the functional equation cite it when establishing nonnegativity for costs and complexity measures. The proof is a one-line term that pairs n with the equality from zero_add to witness the order relation.
Claim. For every element $n$ of the logic-forced naturals, the zero element satisfies $0 ≤ n$.
background
LogicNat is the inductive type with identity (the zero-cost base element) and step (the successor), constructed as the smallest subset of positive reals closed under multiplication by the generator and containing 1. The ArithmeticFromLogic module builds Peano-style arithmetic directly from the Law of Logic. zero_add states that zero + n = n for any LogicNat n and is the key upstream fact used to construct the order witness.
proof idea
The proof is a direct term-mode construction that applies the zero_add lemma: it supplies the pair consisting of n together with the equality zero + n = n, which satisfies the existential definition of the ≤ relation on LogicNat.
why it matters
zero_le supplies the basic nonnegativity fact required by downstream results such as satJCost_nonneg, clay_bridge_theorem, and main_resolution. It occupies an early position in the chain that derives arithmetic from the Recognition functional equation before moving to complexity and decision applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.