ExclusivityCert
plain-language theorem explainer
Empty marker certificate whose verification predicate bundles five uniqueness and positivity claims: φ as sole positive root of x²=x+1, D=3 matching the wallpaper count 17, J vanishing only at 1, strictly positive mass predictions, and exact φ-scaling under rung increment. Cited as the top-level exclusivity bundle for the RS framework. Companion theorem discharges all five conjuncts from golden-ratio uniqueness, W_endo at D=3, J normalization/strictness, and mass-law lemmas.
Claim. An exclusivity certificate is a unit marker whose verification asserts five conjuncts: (1) every positive real root of $x^2=x+1$ equals $\varphi$; (2) the endomorphism count at spatial dimension $D=3$ equals the wallpaper-group constant $17$; (3) the cost satisfies $J(1)=0$ and $J(x)>0$ whenever $x>0$ and $x\neq 1$; (4) predicted mass is positive for every sector, rung, and charge; (5) raising the rung by one multiplies predicted mass by $\varphi$.
background
The module frames exclusivity as stronger than mere derivation: not only do the RS premises yield the observed structure, but no inequivalent choice of base, dimension, cost, or mass decomposition is claimed to reproduce the same structural integers and scalings. The five conjuncts here are a concrete slice of that claim (φ-root, D=3 wallpaper match, J normalization and strict positivity, mass positivity, φ-rung scaling).
Upstream constants fix $D:=3$ (spatial dimension forced by the linking/T9 step) and wallpaper_groups$:=17$ (classical Fedorov count of 2D wallpaper groups). The cost $J$ is the RS J-cost from the cost algebra: normalized so $J(1)=0$, nonnegative on $\mathbb{R}_+$, with defect form $(x-1)^2/(2x)$. Mass predictions come from the φ-ladder mass law $m=A_s\cdot\varphi^{r-8+\mathrm{gap}(Z)}$ in RS-native units.
Module doc also lists fuller exclusivity targets (full RCL uniqueness of $J$, unique gap in the affine-log family) that sit beside this certificate rather than inside the five conjuncts.
proof idea
The structure itself is an empty Repr marker; the content is the verified predicate (five-way conjunction) and the discharge theorem verified_any.
verified_any is a single refine assembling five existing facts: golden-ratio uniqueness for the positive root of $x^2=x+1$; W_endo_at_D3 for the wallpaper match at $D=3$; J_at_one for $J(1)=0$; predict_mass_pos for mass positivity; mass_rung_scaling for exact φ-multiplication under rung$+1$.
The remaining strict-positivity goal for $J$ is proved by contradiction: nonnegativity (J_nonneg) plus $\neg(J x>0)$ forces $J x=0$, hence $x=1$ by the zero-locus lemma, contradicting $x\neq 1$.
why it matters
This is the verification-layer packaging of RS exclusivity: a single Prop that a checker can ask of any certificate value. It sits at the end of the forcing narrative (T5 J-shape, T6 φ as self-similar fixed point, T8 $D=3$) and the mass-law stack (baseline, rung scaling, positivity).
Module doc states the intended reading: change any structural ingredient (base, dimension, cost) and predictions degrade; the certificate records the uniqueness/positivity facts that make that ablation claim checkable in Lean. The companion theorem closes the certificate for every inhabitant, so downstream verifiers need only invoke verified_any.
No used_by edges are recorded yet; the declaration is a top-level export of the Verification domain rather than an intermediate lemma. Fuller exclusivity items named in the module (unique RCL solution for $J$, unique three-point gap) are not all folded into these five conjuncts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.