Pith. sign in
module module moderate

IndisputableMonolith.Foundation.DeltaSpine.CostUniqueness

show as:
view Lean formalization →

Exact inverse and integer powers of φ inside the golden ring ℤ[φ], with φ⁻¹ = φ − 1 as the pair ⟨−1, 1⟩ and no field division. Supplies the multiplicative skeleton used by the real display bridge and by certified φ-ladder ratio bounds. Argument is definitional plus short ring identities on the GoldenInt carrier.

claimIn the golden ring $\mathbb{Z}[\varphi]$, the multiplicative inverse is exact: $\varphi^{-1}=\varphi-1=\langle -1,1\rangle$. The module defines the corresponding unit powers $\varphi^{n}$ for $n\in\mathbb{Z}$ and records the product and addition laws $\varphi^{m+n}=\varphi^{m}\varphi^{n}$, together with the elementary identities $\varphi\cdot\varphi^{-1}=1$ and $\varphi^{-1}=\varphi-1$.

background

DeltaSpine rebuilds the T6 golden-ratio node on a choice-free carrier. Upstream GoldenInt introduces the ring $\mathbb{Z}[\varphi]$ of pairs $\langle a,b\rangle$ standing for $a+b\varphi$ with $\varphi^2=\varphi+1$, and proves the forcing facts at sigma0 (axiom closure ${propext, Quot.sound}$), avoiding the classical Real.sqrt 5 path of PhiForcing.

Once $\varphi$ lives in that ring, the cost and ladder calculus need its inverse and integer powers without leaving the discrete carrier. This module records $\varphi^{-1}$ as the ring element $\varphi-1=\langle -1,1\rangle$ (exact, no division) and packages $\varphi^{n}$ (phiZpow) with the usual cocycle laws. Related constants such as $\sqrt{5}$ appear only as ring-level companions where needed for later display.

The local setting is therefore pure algebraic bookkeeping on $\mathbb{Z}[\varphi]$, preparatory to any continuum evaluation.

proof idea

Definition module with short algebraic lemmas, not a deep existence proof. phiInv is introduced as the concrete pair $\langle -1,1\rangle$; phiInv_eq_phi_sub_one identifies it with $\varphi-1$. The two product lemmas phi_mul_phiInv and phiInv_mul_phi discharge the unit equations by expanding the GoldenInt multiplication rule and reducing via $\varphi^2=\varphi+1$.

phiZpow is the integer power map on that unit; phiZpow_add, phiZpow_zero, phiZpow_one, phiZpow_neg_one, and phiZpow_neg_mul are the standard inductive or case-split identities for group homomorphisms $\mathbb{Z}\to\mathbb{Z}[\varphi]^{\times}$. No analytic estimates and no real embedding appear here.

why it matters in Recognition Science

Feeds the two immediate consumers of the discrete golden skeleton. GoldenIntReal is the sigma1 display bridge: it evaluates $\mathbb{Z}[\varphi]$ into $\mathbb{R}$ once and shows the sigma0 structure maps onto classical PhiForcing. That bridge needs a well-defined inverse and powers already present on the ring side.

LadderRatioBounds carries dimensionless forced ratios $\varphi^{k}$ end-to-end at sigma0 with rational brackets certified by both decide and runtime evaluation. Those ratios are exactly the phiZpow objects defined here; the mass-law ladder (yardstick times $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) depends on them.

In the forcing chain this sits under T6 (φ forced as self-similar fixed point) and supports the cost side of T5 (J-uniqueness), where $J(x)=(x+x^{-1})/2-1$ needs a clean $x^{-1}$ on the golden carrier. Keeps the delta-spine cost story choice-free until the single continuum tax at the display boundary.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (32)