unique17ScanUpTo64_true
plain-language theorem explainer
A closed Boolean scan certifies that 17 is the unique admissible wallpaper-count value among candidates through 64. Bridge and verification authors cite it as the machine-checked certificate that the scan succeeds. The proof is a one-line native decision of that Boolean expression.
Claim. The Boolean scan that searches candidate wallpaper counts through $64$ and tests uniqueness of the value $17$ evaluates to $\mathrm{true}$.
background
This module builds an endogenous RS candidate for the crystallographic constant $W=17$, without re-proving Fedorov's classical wallpaper classification. The candidate is
$$W_{\mathrm{endogenous}}(D):=E_{\mathrm{passive}}(D)+F(D).$$
At the forced spatial dimension $D=3$ (T8), one has $E_{\mathrm{passive}}=11$ and $F=6$, so $W_{\mathrm{endogenous}}=17$, matching the imported classical count of wallpaper groups. The identity $11+6=17$ is therefore an explicit, machine-checked counting-layer fact at $D=3$.
The Boolean unique17ScanUpTo64 is the finite scan that checks uniqueness of this $17$ among candidates up to bound $64$. Spatial dimension $D=3$ is the same constant forced elsewhere in the forcing chain (T8/T9 linking).
proof idea
One-line computational certificate: native_decide evaluates the closed Boolean expression unique17ScanUpTo64 in the kernel and confirms it is true. No algebraic lemmas are unfolded; the proof is pure decidable arithmetic/combinatorial evaluation of the scan definition.
why it matters
The declaration closes the computational side of the Pass-2 wallpaper endogenous bridge: once the scan is true, the counting identity $W_{\mathrm{endogenous}}(3)=17$ is not only equal to the classical wallpaper count but uniquely so inside the scanned range. That supports sibling facts such as $W$ from the cube equaling $17$, matching wallpaper groups, and uniqueness of the wallpaper slot from the endogenous formula.
In the broader RS chain this sits under T8 ($D=3$) and the program of replacing imported classical constants by endogenous RS counts. The module itself states this is only a bridge step toward full endogeneity of $W$; the classical classification is still imported, not re-derived. No downstream theorems currently depend on this certificate (used-by is empty), so it is a leaf verification fact for the bridge module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.