nonIdentityReciprocal_of_residualTrap
plain-language theorem explainer
Residual traps on natural numbers are converted into non-identity reciprocal ledgers by this definition. It supplies the bound witness for the phase-budget engine in the Erdős-Straus residual proof chain. Researchers working on the Erdős-Straus conjecture within the Recognition Science framework would cite it to bridge the rotation hierarchy to visibility engines. The construction extracts positivity directly from the trap hypothesis and verifies the non-identity and budget properties via basic arithmetic.
Claim. Let $n$ be a natural number satisfying the residual trap condition ($1 < n$, $n ≡ 1 mod 24$, and all prime factors of $n$ and $(n+3)/4$ congruent to 1 mod 3). Then $n$ admits a positive non-identity reciprocal ledger: $0 < n$, $n ≠ 1$, and there exists $N$ with $0 < N$ such that $n$ divides $N^2$.
background
ResidualTrap n asserts $1 < n$, $n % 24 = 1$, and all prime factors of both $n$ and $(n+3)/4$ are congruent to 1 mod 3. NonIdentityReciprocal n is the structure with fields pos ($0 < n$), nonidentity ($n ≠ 1$), and reciprocal_budget (existence of $N$ with $0 < N$ and $n | N*N$).
proof idea
The definition constructs the NonIdentityReciprocal structure field by field. Positivity follows from the first component of the residual trap hypothesis via Nat.zero_lt_of_lt. Non-identity is shown by contradiction: assuming equality to 1 produces 1 < 1, discharged by omega. The reciprocal budget is witnessed explicitly by N = n using dvd_mul_right.
why it matters
This definition bridges the Erdős-Straus rotation hierarchy to the phase budget engine. It is invoked in phaseBudgetEngine_of_boundedVisibilityEngine to supply the bound field of PhaseBudgetEngine and likewise in MinimalVisibilityEngine.phaseBudgetEngine. It fills the recovered-ledger step required by the Erdős-Straus chain, sitting inside the eight-tick octave and phi-ladder structure of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.