IndisputableMonolith.Foundation.DeltaSpine.GoldenIntReal
Defines the evaluation map from the golden integer ring ℤ[φ] into ℝ by ⟨a,b⟩ ↦ a + b·φ. Supplies ring-homomorphism laws, injectivity, and positivity transfer so discrete φ-ladder certificates can be read as real numbers. Downstream mass-ratio display modules use this map as the sole σ1 bridge from the choice-free kernel. Content is the standard embedding plus elementary algebraic identities.
claimConstructs the evaluation homomorphism $\iota:\mathbb{Z}[\varphi]\to\mathbb{R}$ by $\iota(\langle a,b\rangle)=a+b\varphi$, proves it is an injective ring homomorphism (preserves $0,1,\varphi,\psi$, addition, negation, multiplication), and equates positivity of a golden integer with positivity of its real image.
background
Recognition Science forces φ as the unique self-similar fixed point of the discrete ledger (T6). The DeltaSpine rebuilds that node choice-free on the golden ring ℤ[φ]: pairs ⟨a,b⟩ of integers with the multiplication rule induced by φ² = φ + 1. GoldenInt carries the ring structure and positivity predicate at σ0 (no Classical.choice).
Real physics display still needs ordinary real numbers. This module supplies the canonical embedding into ℝ, using the classical real φ from PhiForcing. Upstream CostUniqueness and LadderRatioBounds already certify J-cost uniqueness and rational brackets for φ-ladder ratios on the discrete carrier; the embedding is the bridge that turns those certificates into real mass ratios.
Sibling lemmas cover the basic arithmetic of the map (zero, one, φ, the conjugate ψ, add, neg, mul), injectivity, the zero kernel, and the equivalence between the discrete positivity predicate and positivity of the real image.
proof idea
Definition-and-lemmas module, not a single deep theorem. The core object is the noncomputable map toReal sending ⟨a,b⟩ to a + b·φ in ℝ. Homomorphism identities are unfolded from the ring operations on GoldenInt and the minimal polynomial of φ. Injectivity and the zero-kernel criterion follow from linear independence of {1,φ} over ℚ (equivalently over ℤ). Positivity transfer compares the discrete posPair predicate with the sign of the real image. No heavy analysis; pure algebraic bookkeeping once φ is fixed in ℝ.
why it matters in Recognition Science
Closes the σ0-to-σ1 handoff on the DeltaSpine. MassRatioBindingReal imports this module as its display layer: kernel-decided facts on ℤ[φ] (mass-ratio certificates, rung gaps) are re-read in ℝ solely through toReal. Downstream doc states the only new mathematical content is this interpretation map. Without it, T6 ladder ratios and the mass formula yardstick·φ^(rung−8+gap(Z)) stay formal; with it they become ordinary real comparisons (e.g. muon/electron ↔ rung 11). Sits between GoldenInt (discrete carrier) and the real mass-ratio binding that experimentalists actually quote.
scope and limits
- Does not re-prove T6 or uniqueness of φ; imports PhiForcing and GoldenInt.
- Does not certify mass ratios; only supplies the ℝ reading of discrete certificates.
- Does not avoid Classical.choice: toReal is noncomputable (σ1 display).
- Does not treat other embeddings or Galois conjugates beyond the listed ψ lemmas.
- Does not address continuity, topology, or analytic properties of the ladder.
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