zero_le
plain-language theorem explainer
zero_le asserts that the zero element of LogicNat is less than or equal to every element of the type. Researchers establishing non-negativity of costs or ledger properties cite it in complexity and decision-theory arguments. The proof is a direct term construction that supplies the additive witness from zero_add.
Claim. For every element $n$ of the natural numbers induced by the law of logic, the zero element satisfies $0 ≤ n$, where $≤$ is witnessed by an additive complement satisfying $0 + m = n$.
background
ArithmeticFromLogic builds the natural numbers and their arithmetic directly from the Law of Logic. LogicNat is the inductive type whose identity constructor represents the zero-cost multiplicative identity and whose step constructor iterates the generator; this mirrors the orbit of positive reals closed under multiplication by the generator and containing 1. The relation $≤$ on LogicNat is the standard order induced by addition: $a ≤ b$ means there exists $m$ such that $a + m = b$. zero_add states that left-addition by zero is the identity map on any LogicNat element and is proved by induction on the second argument.
proof idea
One-line wrapper that applies zero_add to furnish the witness pair for the ≤ relation.
why it matters
zero_le supplies the base non-negativity fact used by satJCost_nonneg (J-cost ≥ 0), logUtilityPartial_succ, and the main_resolution and clay_bridge_theorem in ComputationBridge. It completes the arithmetic layer required before the Recognition Composition Law and the ledger arguments that resolve P vs NP. The result sits inside the forcing chain that derives arithmetic from the single functional equation before any appeal to T5–T8 or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.