passiveAtLevel_0

The module derives the generation torsion values ${0, 11, 17}$ as the unique numbers compatible with the $8$-tick Hamiltonian cycle on $Q_3$, projected onto the $\varphi$-ladder through the Recognition Composition Law. RCL forces independent couplings to add in the ladder exponent; the Gray cycle on $Q_3$ partitions cells into one active edge and a passive skeleton; CW attachment forces admissible couplings to be downward-closed.

passiveAtLevel records the passive subcell count by CW dimension: level $0$ (vertices) is $0$ because the cycle visits all $2^D$ vertices; level $1$ is the passive field-edge count $11$; level $2$ is the face count $6$; higher levels are $0$. Spatial dimension $D$ is the constant $3$ forced by the T8/T9 chain (linking and configuration dimension).

One-line definitional proof. Unfolding passiveAtLevel D 0 hits the first match arm, which is the literal constant $0$, so rfl closes the equality. The @[simp] attribute makes the reduction available to the simplifier in later level-matching lemmas.

This is the level-$0$ base case in the torsion-forcing table that feeds the structural claim that generation torsions are exactly ${0, 11, 17}$. The module narrative ties that triple to the $8$-tick octave (T7), $D = 3$ (T8), and additive RCL channels on the $\varphi$-ladder. Sibling facts cover levels $1$–$3$ and the match to passive coupling; together they pin the passive skeleton used by the generation-torsion bridge and the variational ground-state-at-zero argument. No downstream users are recorded yet; the lemma is infrastructure for the closed derivation chain in this file.