IndisputableMonolith.Foundation.DeltaSpine.GoldenInt
The golden ring Z[φ] is coded as integer pairs (a,b) for a+bφ, with multiplication reduced by φ²=φ+1. Recognition Science uses this discrete carrier so T6 (φ forced as the unique positive golden root) can close inside sigma0 before any real embedding. Cost uniqueness on the φ-ladder, the real display bridge, and certified ladder-ratio brackets all import it. The module is definitional infrastructure for the DeltaSpine discrete layer.
claimThe golden integer ring $\mathbb{Z}[\varphi]$ consists of pairs $(a,b)\in\mathbb{Z}\times\mathbb{Z}$ standing for $a+b\varphi$, with componentwise addition and multiplication folded through the relation $\varphi^2=\varphi+1$. The conjugate root $\psi=1-\varphi$ is carried in the same arithmetic, together with the units $0$ and $1$ as named pairs.
background
Recognition Science isolates $\varphi$ as the self-similar fixed point (T6) after J-cost uniqueness (T5). The DeltaSpine program re-derives those nodes on a discrete carrier so continuum structure is paid only at a display boundary.
This module introduces $\mathbb{Z}[\varphi]$ as pairs $(a,b)$ for $a+b\cdot\varphi$. The identity $\varphi^2=\varphi+1$ collapses higher powers, keeping ring operations inside $\mathbb{Z}\times\mathbb{Z}$. Named constants package $0$, $1$, $\varphi$, and the conjugate $\psi$; component projections expose the integer coordinates later decide tactics consume.
The setting is pure algebra: Mathlib is the sole import. No real analysis appears here; evaluation into $\mathbb{R}$ is deferred.
proof idea
This is a definition module, not a theorem package. It declares the golden-integer type (pairs with the $\varphi^2=\varphi+1$ multiplication law), the ring operations, and the standard generators $0$, $1$, $\varphi$, $\psi$ together with their integer components. Arithmetic identities are definitional or inherited from integer arithmetic; there is no substantial proof body to walk.
why it matters in Recognition Science
CostUniqueness imports the carrier to re-derive T5 (any reciprocal-symmetric, normalized, calibrated continuous $F$ obeying the Recognition Composition Law is the J-cost) on the forced discrete $\varphi$-ladder at sigma0. GoldenIntReal is the sigma1 display bridge: it evaluates $\mathbb{Z}[\varphi]$ into $\mathbb{R}$ and matches the classical PhiForcing presentation, paying the continuum tax once. LadderRatioBounds uses the same arithmetic to certify dimensionless $\varphi^k$ mass-ladder ratios with rational brackets that both the kernel and runtime accept. The module therefore underwrites the discrete half of the T5–T6 spine before any real embedding.
scope and limits
- Does not embed Z[φ] into R; that is the GoldenIntReal display bridge.
- Does not prove T5 or T6 uniqueness; those live in CostUniqueness and related spine nodes.
- Does not state the Recognition Composition Law or any continuity hypothesis.
- Does not certify numerical mass-ladder brackets; LadderRatioBounds owns that.
- Does not introduce analysis, topology, or measure structure.
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