HitsBalancedPhaseLogic
This definition equips logic naturals with a balanced phase hit predicate by transporting the classical Erdős-Straus box condition through the iteration count map. Researchers bridging logic-native structures to classical arithmetic in Recognition Science would cite it to keep the finite phase proof surface unchanged. It is a direct one-line wrapper that applies toNat to the classical HitsBalancedPhase predicate.
claimFor logic naturals $n$ and $c$, the predicate HitsBalancedPhaseLogic$(n,c)$ holds when the classical balanced residual phase condition is satisfied by the natural numbers obtained as iteration counts from the identity element under the step generator.
background
The module supplies a logic-native adapter for the Erdős-Straus square-budget box phase. LogicNat is the inductive type whose constructors identity (the zero-cost multiplicative identity) and step generate the orbit closed under multiplication by the generator. The map toNat extracts the iteration count, sending identity to 0 and each step to its successor. HitsBalancedPhase asserts that a square-budget box for parameters $n$ and $c$ meets the balanced residual phase when $c$ divides both $N +$ boxDivisor and $N +$ boxComplement, with $N = n x$ and $c = 4x - n$. The local setting records that native combinatorial structures live over LogicNat while the final transport returns results as LogicRat representations.
proof idea
The definition is a one-line wrapper that applies the toNat map to the arguments of the classical HitsBalancedPhase predicate from the ErdosStrausBoxPhase module.
why it matters in Recognition Science
This supplies the logic-native balanced phase hit used by box_phase_hit_gives_repr_logic to obtain HasRationalErdosStrausReprLogic and by hitsBalancedPhaseLogic_iff_classical to record the equivalence with the classical predicate. It forms part of the adapter that transports the classical Erdős-Straus box-phase theorem back to LogicRat via LogicErdosStrausRCL while preserving the Law of Logic carrier. The construction supports the program of deriving arithmetic structures from the forced orbit without reopening the classical proof surface.
scope and limits
- Does not establish existence of any balanced phase hit for given $n$ and $c$.
- Does not extend the predicate beyond the square-budget box construction.
- Does not supply size bounds on the auxiliary parameters $x$ or $N$.
- Does not connect to J-cost, defect distance, or the phi-ladder.
formal statement (Lean)
51def HitsBalancedPhaseLogic (n c : LogicNat) : Prop :=
proof body
Definition body.
52 ErdosStrausBoxPhase.HitsBalancedPhase (toNat n) (toNat c)
53