NonIdentityReciprocal
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assert existence of any such n for a given budget or floor.
- Does not compute or bound the witness N.
- Does not embed J-cost, phi-ladder, or phase-visibility bounds directly.
- Does not address the KTheta floor hypothesis itself.
Lean usage
theorem use_non_identity (engine : BoundedVisibilityEngine) {n : ℕ} (hn : NonIdentityReciprocal n) : BoundedFiniteQuotientPhaseVisibility n engine.bound := bounded_phase_visibility engine hnformal statement (Lean)
27structure NonIdentityReciprocal (n : ℕ) : Prop where
28 pos : 0 < n
29 nonidentity : n ≠ 1
30 reciprocal_budget : ∃ N : ℕ, 0 < N ∧ n ∣ N * N
31
32/-- KTheta floor hypothesis assumption at the RS scale `KTheta`. -/