passiveAtLevel_2
plain-language theorem explainer
At spatial dimension 3, the passive subcell count on CW level 2 (faces) is exactly 6. Mass and generation-torsion arguments that partition the 8-tick Hamiltonian cycle on the 3-cube cite this as the face contribution to passive field dressing. The proof is a one-line native decision of the level-2 clause of the passive-count definition against D = 3.
Claim. With spatial dimension $D = 3$, the passive subcell count at CW level 2 equals 6: $\mathrm{passive}(D,2) = 6$. Equivalently, the number of cube faces is $2D = 6$, and every face sits on the passive skeleton of the 8-tick cycle.
background
The module derives generation torsion values ${0,11,17}$ as the unique profile compatible with the 8-tick Hamiltonian cycle on $Q_3$, the Recognition Composition Law, and the $\varphi$-ladder. Under RCL, independent couplings add in the ladder exponent; the cycle partitions $Q_3$ into active and passive subcells by CW dimension.
passiveAtLevel records that partition: level 0 (vertices) contributes 0 because the cycle visits every vertex; level 1 contributes the 11 passive edges; level 2 contributes all cube faces; higher levels contribute 0. The spatial dimension $D$ is fixed at 3 by the forcing chain (T8/T9).
Level 2 is therefore just the face count of the 3-cube. In the CW picture those six faces form the passive skeleton available for higher-dimensional coupling, subject to the downward-closed attachment rule that faces require their bounding edges.
proof idea
Unfold passiveAtLevel at argument 2: the clause is cube_faces d. Instantiate at the global $D = 3$ and evaluate cube_faces 3 = 6 by native_decide. No lemmas beyond the definition and the numeral $D = 3$ are required; the @[simp] attribute exposes the equality to the simplifier.
why it matters
This numeral is one of the four level-wise anchors (passiveAtLevel_0 through _3) that feed the torsion-forcing story: the 8-tick cycle on $Q_3$ leaves six faces passive, matching the geometric face count $2D$ at $D = 3$. Together with the eleven passive edges and the zero vertex/interior counts, it supplies the CW-level inventory used to restrict admissible coupling profiles to lower sets and ultimately to force generation torsions ${0,11,17}$.
Framework landmarks in play are T7 (eight-tick octave, period $2^3$), T8 ($D = 3$), and the RCL-driven additive torsion channels on the $\varphi$-ladder. No downstream theorems currently list this declaration as a direct dependency in the graph, but sibling matching lemmas (e.g. agreement with passiveCoupling) and the module-level uniqueness claim for ${0,11,17}$ are the intended consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.