IndisputableMonolith.Foundation.DeltaSpine.GoldenIntReal
Evaluation homomorphism from the golden integer ring Z[phi] into the reals: pair (a,b) maps to a + b·phi. Supplies ring operations, injectivity, and positivity transport so sigma0 certificates on Z[phi] can be read as real numbers. Downstream mass-ratio display cites this map. Proofs are direct expansions of the embedding and the minimal polynomial of phi.
claimThe evaluation map $\mathrm{toReal}:\mathbb{Z}[\varphi]\to\mathbb{R}$ sends $\langle a,b\rangle\mapsto a+b\varphi$ with $\varphi=(1+\sqrt{5})/2$. It is an injective ring homomorphism, fixes $0$ and $1$, sends the golden basis elements to $\varphi$ and $\psi=1-\varphi$, and identifies the positive cone of $\mathbb{Z}[\varphi]$ with strictly positive reals.
background
Recognition Science forces the golden ratio as the self-similar fixed point of the discrete ledger (T6). The sigma0 module GoldenInt rebuilds that carrier as the ring $\mathbb{Z}[\varphi]$ of pairs $\langle a,b\rangle$ with integer coordinates, avoiding classical choice and real square roots on the kernel path. CostUniqueness and LadderRatioBounds then run T5 and dimensionless rung ratios on that discrete carrier.
This module is the bridge back to $\mathbb{R}$. It defines the interpretation $\langle a,b\rangle\mapsto a+b\varphi$ and records that the map is a unital ring homomorphism. Companion lemmas identify images of $0$, $1$, $\varphi$, and the conjugate $\psi$, and transport the positivity predicate on pairs to ordinary positivity in $\mathbb{R}$.
PhiForcing already forces $\varphi$ over the reals with a choice-taxed carrier; GoldenIntReal is the matching display map for the choice-free ring, not a second forcing argument.
proof idea
Definition module plus elementary algebraic lemmas, not a deep existence proof. The core object is the linear evaluation $\mathrm{toReal},\langle a,b\rangle=a+b\varphi$. Homomorphism laws for addition, negation, and multiplication expand both sides and cancel with the relation $\varphi^2=\varphi+1$. Images of zero, one, $\varphi$, and $\psi$ are one-line unfoldings. Injectivity and the zero criterion follow from linear independence of ${1,\varphi}$ over $\mathbb{Q}$ (equivalently, the minimal polynomial). Positivity lemmas compare the pair-level positive cone to the sign of the real image.
why it matters in Recognition Science
MassRatioBindingReal imports this module as its real display layer: sigma0 kernel facts about mass ratios live on $\mathbb{Z}[\varphi]$ and are decided by decide; the only new content on the real side is this interpretation map (noncomputable, sigma1). Without toReal, rung certificates cannot be stated as ordinary real inequalities for muon/electron and related ladder comparisons.
In the forcing chain the module sits after T6 (phi forced) and the delta-spine GoldenInt rebuild, and before real-facing mass-law bindings. It does not re-prove T5/T6; it only exports the embedding those later display theorems need. Framework landmarks: T6 phi fixed point, the phi-ladder mass formula, and the sigma0/sigma1 split between kernel certificates and real readout.
scope and limits
- Does not re-prove T6 phi forcing or uniqueness of the golden fixed point.
- Does not derive mass ratios or rung gaps; only supplies the real embedding.
- Does not eliminate classical choice from Real.sqrt or noncomputable Real arithmetic.
- Does not address complex embeddings or Galois conjugates beyond psi image lemmas.
- Does not certify decimal bounds; LadderRatioBounds and MassRatioBinding handle brackets.
used by (1)
depends on (5)
declarations in this module (26)
-
def
toReal -
theorem
toReal_zero -
theorem
toReal_one -
theorem
toReal_phi -
theorem
toReal_psi -
theorem
toReal_add -
theorem
toReal_neg -
theorem
toReal_mul -
theorem
toReal_eq_zero_iff -
theorem
toReal_injective -
theorem
posPair_real_pos -
theorem
isPos_iff_toReal_pos -
theorem
t6_bridge -
theorem
toReal_sub -
theorem
toReal_two -
theorem
toReal_phiInv -
theorem
toReal_phiZpow -
theorem
toReal_traceZ -
theorem
traceZ_cosh -
theorem
jdouble_eq_jcost -
theorem
t5_bridge -
theorem
toReal_ratWitness -
theorem
ratLt_toReal -
theorem
ratGt_toReal -
theorem
toReal_phiPow -
theorem
ladder_ratio_real_brackets