DivisorExponentBoxLogic
DivisorExponentBoxLogic packages a pair of positive LogicNat elements d and e whose product equals N squared, serving as the native representation of a divisor-exponent box point for the Erdős-Straus square-budget phase. Number theorists adapting classical box-phase arguments to the logic setting cite it when defining intermediate structures before transport to ℕ. The declaration is a direct structure with no proof obligations beyond the listed fields.
claimLet $N$ be a logic-natural number. A divisor-exponent box point consists of logic-natural numbers $d$ and $e$ satisfying $d > 0$, $e > 0$, and $d e = N^2$.
background
LogicNat is the inductive type whose constructors identity and step generate the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by the generator and containing the multiplicative identity, as forced by the Law of Logic. The module supplies a logic-native adapter for the Erdős-Straus square-budget box phase: combinatorial structures are expressed over LogicNat, the final theorem transports to the existing ℕ box-phase result, and the outcome is returned as a LogicRat representation via the RCL adapter. The upstream result e_pos merely records that exp(1) is positive and is not invoked by this structure.
proof idea
The declaration is a structure definition that directly introduces the fields d and e together with the three required properties (positivity of each and the square-budget equation). No tactics or lemmas are applied; the structure itself encodes the recovered box point.
why it matters in Recognition Science
The structure supplies the core data type for the logic-native Erdős-Straus box phase and is immediately consumed by boxDivisorLogic, boxComplementLogic, and the transport theorem box_logic_toNat_square_budget that recovers the classical square-budget relation toNat(d) · toNat(e) = toNat(N)². It therefore occupies the position of the recovered divisor-exponent point inside the adapter module that bridges the logic setting to the classical Erdős-Straus box-phase theorem.
scope and limits
- Does not assert existence of d and e for a given N.
- Does not supply an algorithm to locate such a pair.
- Does not address the full Erdős-Straus conjecture.
- Does not define arithmetic operations on the structure itself.
formal statement (Lean)
29structure DivisorExponentBoxLogic (N : LogicNat) where
30 d : LogicNat
31 e : LogicNat
32 d_pos : 0 < d
33 e_pos : 0 < e
34 square_budget : d * e = N * N
35