DvdL
plain-language theorem explainer
DvdL defines divisibility on the logic-forced naturals that underpin the Erdős-Straus square-budget adapter. Number theorists adapting classical divisor arguments to the logic-native setting would cite this predicate when transporting box-phase results. The definition is supplied directly as an existential statement over the multiplicative structure of LogicNat.
Claim. Let $a$ and $b$ be elements of the logic naturals. Then $a$ divides $b$ if there exists an element $k$ of the logic naturals such that $b = a k$.
background
LogicNat is the inductive type whose constructors are the zero-cost identity element (multiplicative identity) and the step constructor (one further iteration of the generator). The two-constructor structure mirrors the smallest subset of positive reals closed under multiplication by the generator and containing 1, as recovered from the Law of Logic in the arithmetic-from-logic foundation.
proof idea
The declaration is a direct definition that encodes divisibility by an existential quantifier over multiplication in the logic naturals.
why it matters
The predicate supplies the divisor relation required by sibling constructions such as divisor-exponent box logic and phase-hit representations inside the Erdős-Straus adapter. It participates in the module-level transport that moves classical box-phase theorems to LogicNat and returns LogicRat representations via the RCL module, thereby closing the logic-native path for the square-budget phase.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.