hitsBalancedPhaseLogic_iff_classical
plain-language theorem explainer
The equivalence establishes that the logic-native balanced-phase hit predicate on LogicNat is identical to the classical Erdős-Straus box-phase predicate once the iteration-count map is applied. Researchers transporting combinatorial results between logic-forced arithmetic and standard natural-number arithmetic would cite this transport lemma. The proof is a one-line reflexivity that follows directly from the definitional unfolding of HitsBalancedPhaseLogic.
Claim. Let $n,c$ belong to the logic-natural numbers. The logic-native balanced phase hit condition holds for $n$ and $c$ if and only if the classical Erdős-Straus box-phase balanced hit condition holds for the underlying natural numbers obtained by reading off the iteration counts of $n$ and $c$.
background
LogicNat is the inductive type whose constructors identity and step generate the orbit {1, γ, γ², …} forced by the Law of Logic; toNat extracts the corresponding Peano natural by counting steps. HitsBalancedPhaseLogic is the in-module definition that simply applies the classical HitsBalancedPhase predicate after this embedding. The module supplies a logic-native adapter for the Erdős-Straus square-budget box phase so that combinatorial structures remain inside the logic-forced carrier while the final representation is recovered as a LogicRat via the RCL transport.
proof idea
The proof is a term-mode reflexivity (Iff.rfl). Because HitsBalancedPhaseLogic is literally defined to be ErdosStrausBoxPhase.HitsBalancedPhase (toNat n) (toNat c), the two sides of the biconditional are definitionally equal and the reflexivity tactic closes the goal immediately.
why it matters
The declaration closes the transport between the logic-native arithmetic (ArithmeticFromLogic) and the existing classical box-phase theorem (ErdosStrausBoxPhase), enabling the module’s final step that returns a LogicRat representation. It sits inside the eight-tick phase machinery (T7) and the square-budget formulation of the Erdős-Straus conjecture, keeping the finite-phase proof surface stable while the carrier is recovered from the Law of Logic. No downstream uses are recorded yet; the lemma is scaffolding for the RCL recovery step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.