IndisputableMonolith.Foundation.DeltaSpine.GoldenInt
Defines the golden ring ℤ[φ] as integer pairs (a,b) for a + b·φ, with ring operations reduced by φ² = φ + 1. Supplies the discrete carrier on which T6 (φ forced) and ladder ratios live without continuum axioms. Downstream CostUniqueness, GoldenIntReal, and LadderRatioBounds import it as the sigma0 base. Structure is a pure definition module: constructors, basis elements, and componentwise arithmetic.
claimThe golden integer ring $\mathbb{Z}[\varphi] = \{ a + b\varphi : a,b \in \mathbb{Z} \}$ with multiplication reduced by the minimal relation $\varphi^2 = \varphi + 1$. Basis elements include $0$, $1$, $\varphi$, and the conjugate $\psi$; addition and multiplication act componentwise on the pair coordinates after folding higher powers of $\varphi$.
background
Recognition Science forces the cost $J$ (T5) and then the self-similar fixed point $\varphi$ (T6) as the unique positive root of $x^2 = x + 1$. Working entirely inside $\mathbb{Z}[\varphi]$ keeps the argument at sigma0: only propositional extensionality and quotient soundness, no real analysis.
Elements are pairs $(a,b)$ standing for $a + b\varphi$. Because $\varphi^2 = \varphi + 1$, every higher power reduces to a linear combination with integer coefficients, so the set is closed under multiplication. The conjugate root $\psi = 1 - \varphi$ (equivalently $-1/\varphi$) appears as a second basis element used in norm and ratio arguments later on the spine.
The module sits in Foundation.DeltaSpine: the discrete ladder carrier before any display map into $\mathbb{R}$. Component projections (zero, one, $\varphi$, $\psi$ coordinates) and the addition law on the first coordinate are the primitive API exposed to importers.
proof idea
This is a definition module, no theorems. It introduces the pair type for golden integers, named constants for $0$, $1$, $\varphi$, $\psi$ in coordinates, and the ring operations (addition begins with the first-component rule) with multiplication folded through $\varphi^2 = \varphi + 1$. Downstream modules prove uniqueness and bounds on top of these constructors.
why it matters in Recognition Science
CostUniqueness re-derives T5 on this forced discrete carrier: any reciprocal-symmetric normalized calibrated continuous $F$ obeying the Recognition Composition Law is pinned to $J$ once the ladder is $\mathbb{Z}[\varphi]$. GoldenIntReal is the sigma1 display bridge: it evaluates $\mathbb{Z}[\varphi]$ into $\mathbb{R}$ once and matches the classical PhiForcing presentation, paying the continuum tax only at the boundary. LadderRatioBounds carries dimensionless ratios $\varphi^k$ end-to-end at sigma0 with rational brackets certified by both decide and runtime eval, using the mass-law placement of spectrum rungs on the $\varphi$-ladder.
Without this ring, T6 and the ladder would sit on $\mathbb{R}$ from the start and lose the DELTA_FORCED (sigma0) closure. The module is the algebraic substrate for the forcing chain steps T5–T6 and for every later dimensionless $\varphi$-power identity in the spine.
scope and limits
- Does not prove uniqueness of φ or T6; only defines the carrier ring.
- Does not embed ℤ[φ] into ℝ; that is GoldenIntReal.
- Does not derive the Recognition Composition Law or J-cost uniqueness.
- Does not certify ladder ratio bounds or mass-law exponents.
- Does not introduce analysis, continuity, or completeness axioms.
used by (3)
declarations in this module (43)
-
structure
GoldenInt -
def
phi -
def
psi -
theorem
zero_a -
theorem
zero_b -
theorem
one_a -
theorem
one_b -
theorem
phi_a -
theorem
phi_b -
theorem
psi_a -
theorem
psi_b -
theorem
add_a -
theorem
add_b -
theorem
neg_a -
theorem
neg_b -
theorem
mul_a -
theorem
mul_b -
theorem
sub_a -
theorem
sub_b -
def
norm -
theorem
norm_zero -
theorem
norm_mul -
theorem
five_dvd_of_five_dvd_sq -
theorem
sq_ne_five_sq -
theorem
int_sq_eq_five_sq -
theorem
norm_eq_zero_iff -
theorem
mul_eq_zero_iff -
theorem
phi_sq -
theorem
psi_sq -
theorem
phi_ne_psi -
theorem
golden_factorization -
theorem
golden_roots -
def
PosPair -
def
IsPos -
theorem
phi_isPos -
theorem
psi_not_isPos -
theorem
zero_not_isPos -
theorem
posPair_trichotomy -
theorem
posPair_not_neg -
theorem
isPos_trichotomy -
theorem
isPos_not_neg -
theorem
isPos_ne_zero -
theorem
t6_delta_forced