NonIdentityReciprocal
plain-language theorem explainer
NonIdentityReciprocal defines a positive integer n not equal to one that admits an integer witness N such that n divides N squared. Researchers applying bounded visibility engines or minimal phase-budget engines cite this property to restrict the class of integer ledgers under consideration. The declaration is a three-field structure that introduces the positivity, non-identity, and reciprocal-budget conditions directly.
Claim. A natural number $n$ satisfies the non-identity reciprocal property when $n>0$, $n≠1$, and there exists $N∈ℕ$ with $N>0$ such that $n$ divides $N^2$.
background
The BoundedPhaseVisibility module shows that finite phase invisibility cannot persist beyond a supplied bound once recovered integer ledgers carry stable unresolved-phase budgets and failed gates respect a uniform KTheta floor. NonIdentityReciprocal encodes the ledger-side precondition: positivity, exclusion of the unit, and existence of a square-divisor budget witness. Upstream, KTheta is the RS phase-failure floor given by Jcost phi / 45, while scale(k) = phi^k supplies the cosmological scaling used in the surrounding number-theoretic arguments.
proof idea
This is a structure definition that introduces the three required properties as named fields. No lemmas or tactics are invoked; the declaration functions as a typed interface for downstream visibility theorems.
why it matters
NonIdentityReciprocal supplies the ledger hypothesis required by BoundedVisibilityEngine, MinimalEngine, and the theorems bounded_phase_visibility and hits_admissible_gate. It thereby connects the phase-budget arithmetic to the KThetaFailureFloorHypothesis and the Recognition Science forcing chain (T5 J-uniqueness through T7 eight-tick octave). The property closes the interface between stable budget assumptions and subset-product phase hits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.