t6_delta_forced
plain-language theorem explainer
In the golden ring ℤ[φ], the self-similarity equation x² = x + 1 has unique positive root φ, with conjugate ψ = 1 − φ as the only other root. Researchers citing the choice-free T6 forcing node of the Delta Spine use this package. The proof is a four-conjunct term refine: kernel facts for the equation and positivity, factorization for the root list, and a positivity contradiction that eliminates ψ.
Claim. In the golden integer ring $\mathbb{Z}[\varphi]$ of pairs $(a,b)$ representing $a+b\varphi$, one has $\varphi\cdot\varphi=\varphi+1$, $\varphi$ is constructively positive, every $x$ with $x\cdot x=x+1$ equals either $\varphi$ or $\psi=1-\varphi$, and every positive solution of that equation equals $\varphi$.
background
This module is the sigma0 (choice-free) re-derivation of the T6 golden-ratio forcing node. The older continuum spine proves the same claim over $\mathbb{R}$ with $\sqrt{5}$ and pays Classical.choice; here the carrier is the ring $\mathbb{Z}[\varphi]=\mathbb{Z}\times\mathbb{Z}$ with multiplication folded through $\varphi^2=\varphi+1$, and the target axiom closure is ${propext, Quot.sound}$.
GoldenInt is the structure of pairs $(a,b)$ for $a+b\varphi$. Constructive positivity IsPos is the decidable integer predicate PosPair(2a+b,b), the exact sign data of $(s+b\sqrt{5})/2$. The conjugate root is $\psi=\langle 1,-1\rangle$.
Upstream facts used here: $\varphi$ satisfies the golden equation and is positive by kernel decide; the classification theorem factors $(x-\varphi)(x-\psi)=0$ and invokes the integral-domain property (multiplicative norm $N(a+b\varphi)=a^2+ab-b^2$, with irrationality of $\sqrt{5}$ by strong induction on $\mathbb{N}$).
proof idea
Term-mode refine builds the four-way conjunction directly.
- First conjunct: apply the kernel theorem that $\varphi\cdot\varphi=\varphi+1$.
- Second: apply the kernel theorem that $\varphi$ is positive (
decideon the integer sign pair). - Third: pointwise apply the root-classification theorem, which rewrites the golden equation as $(x-\varphi)(x-\psi)=0$ and splits via the integral-domain zero-product law.
- Fourth: from that classification, case-split on $x=\varphi$ versus $x=\psi$. The $\varphi$ branch is reflexivity; the $\psi$ branch is
absurdagainst the positivity hypothesis, using the kernel fact that $\psi$ is not positive.
why it matters
This is the named DELTA_FORCED closure of T6 in the forcing chain (T0–T8): $\varphi$ is forced as the unique positive self-similar fixed point of $x^2=x+1$. The continuum PhiForcing proof of the same content is sigma1 (choice via Real.sqrt); the present theorem strips that carrier tax so the derivation itself sits in ${propext, Quot.sound}$. The display bridge toReal (with toReal φ = PhiForcing.φ and positivity agreement) is deferred to GoldenIntReal, which honestly remains sigma1: continuum tax is paid once at the boundary, not inside the forcing argument.
No downstream graph edges are recorded yet; the declaration is the module's audit target (#print axioms t6_delta_forced, Delta Forcing Spectrum program). Framework landmark: T6 phi-forcing, now available without choice inside the golden ring.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.