boxDivisorLogic
plain-language theorem explainer
boxDivisorLogic extracts the divisor component from a recovered divisor-exponent box point over LogicNat. Number theorists adapting the Erdős-Straus square-budget phase cite it when moving between logic-native and classical arithmetic. The definition is realized as a direct field projection on the input structure.
Claim. Let $N$ be a logic-natural and let box be a structure holding positive logic-naturals $d$ and $e$ with $d$ times $e$ equal to $N$ squared. The function returns the divisor component $d$.
background
LogicNat encodes the natural numbers as forced by the Law of Logic. The inductive type uses identity for the zero-cost multiplicative identity and step for one further iteration of the generator, forming the orbit closed under multiplication by the generator and containing 1. DivisorExponentBoxLogic recovers a divisor-exponent box point for a given LogicNat $N$. The structure packages two positive logic-naturals $d$ and $e$ together with the square-budget equality $d$ times $e$ equals $N$ squared. This module supplies the logic-native adapter for the Erdős-Straus square-budget box phase, preparing structures over LogicNat for transport to the classical natural-number theorem.
proof idea
The definition is a one-line wrapper that applies field projection to extract the $d$ component of the supplied DivisorExponentBoxLogic structure.
why it matters
This definition supplies the divisor recovery step inside the logic-native formulation of the Erdős-Straus box phase. It supports the module's transport to the existing natural-number box-phase theorem via the RCL adapter. Within the Recognition framework it contributes to the number-theoretic layer without invoking the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.