unique17ScanUpTo64
plain-language theorem explainer
Boolean certificate that, among dimensions 0 through 64, the endogenous wallpaper count equals 17 exactly when the dimension is 3. Anyone checking that the RS cube formula singles out spatial dimension three for the classical W=17 slot will cite it. The body is a pure finite scan: range, pointwise decide of the biconditional, and List.all.
Claim. Define the boolean that holds if and only if, for every natural number $d$ with $0 \le d \le 64$, one has $W_{\mathrm{endogenous}}(d) = 17 \Leftrightarrow d = 3$, where $W_{\mathrm{endogenous}}(d) = d \cdot 2^{d-1} - 1 + 2d$.
background
The module builds an endogenous RS candidate for the crystallographic constant $W = 17$ without re-proving Fedorov's classification. It sets $W_{\mathrm{endogenous}}(d) := E_{\mathrm{passive}}(d) + F(d)$, with closed form $d \cdot 2^{d-1} - 1 + 2d$. At $d = 3$ this splits as $11 + 6 = 17$, matching the imported wallpaper-group count.
$W_{\mathrm{endogenous}}$ is the local counting layer: passive field edges plus cube faces. The scan asks whether that count hits 17 only at the forced spatial dimension $D = 3$ (T8 in the forcing chain), at least on a finite initial segment large enough for machine checking.
Upstream, all is the universal quantifier over a family of stable trace predicates; here the same List.all pattern is used computationally on a concrete range rather than as a TracePredicate.
proof idea
Not a proof: a definitional boolean. List.range 65 yields $0,\ldots,64$. For each $d$, decide evaluates the Prop $W_{\mathrm{endogenous}}(d) = 17 \leftrightarrow d = 3$ to a Bool. List.all returns true only if every entry is true. Downstream, unique17ScanUpTo64_true discharges the equality to true by native_decide.
why it matters
Closes the finite uniqueness half of the wallpaper endogenous bridge: the counting identity $11+6=17$ is not accidental at $D=3$ among the first 65 dimensions. Parent theorem unique17ScanUpTo64_true asserts the scan succeeds, so later lemmas (W_from_cube_eq_17, wallpaper_slot_unique_from_endogenous_formula) can treat uniqueness up to 64 as machine-checked fact.
In the RS forcing chain this supports T8 ($D=3$ spatial dimensions): the same dimension that the chain forces is the unique small-$d$ root of $W_{\mathrm{endogenous}}(d)=17$. The module still imports classical $W=17$; full endogeneity remains open beyond this bridge and finite scan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.