zero_a
plain-language theorem explainer
The integer part of the zero element of ℤ[φ] is the integer 0. Anyone rewriting componentwise in the golden ring cites this as a simp lemma. The proof is pure reflexivity from the structure and zero instance.
Claim. If $0$ denotes the additive identity of the golden ring $\mathbb{Z}[\varphi]=\{(a,b):a,b\in\mathbb{Z}\}$ with $a+b\varphi$, then the integer-part projection of $0$ equals $0\in\mathbb{Z}$.
background
The module rebuilds the T6 golden-ratio forcing node over the ring $\mathbb{Z}[\varphi]$ rather than $\mathbb{R}$. Elements are pairs $(a,b)$ standing for $a+b\varphi$, with multiplication folded through the relation $\varphi^2=\varphi+1$. The goal is a choice-free (sigma0) derivation: only elementary integer arithmetic, with axiom closure inside ${\mathrm{propext},\mathrm{Quot.sound}}$.
GoldenInt is the structure carrying those two integer fields. Additive zero is the pair with both components zero; this lemma names the first-component fact so later componentwise rewrites can stay inside a restricted simp only set. Full simp is banned in the module because Mathlib's default simp set pulls choice-tainted lemmas.
proof idea
One-line reflexivity. The zero instance on GoldenInt is definitionally the pair $(0,0)$, so projecting the integer part and comparing to $0\in\mathbb{Z}$ is rfl. No lemmas are applied.
why it matters
Feeds the component-lemma simp set used throughout the golden-ring development; the immediate downstream consumer is mul_b, which expands the $\varphi$-coefficient of a product by rfl and relies on the same disciplined simp surface. Without these projection lemmas, every ring identity would have to unfold structure fields by hand, cluttering the sigma0 T6 re-derivation.
In the Recognition forcing chain, T6 forces $\varphi$ as the self-similar fixed point. This module's point is that the same content lives over $\mathbb{Z}[\varphi]$ with no continuum and no Classical.choice. Tiny rfl facts like this one keep the rewrite hygiene that the Delta Forcing Spectrum program demands before the display bridge in GoldenIntReal pays the continuum tax once.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.