passiveAtLevel
plain-language theorem explainer
Maps each CW dimension of the 3-cube to its passive subcell count under the 8-tick Hamiltonian cycle: vertices 0, edges 11, faces 6, higher 0. Mass and generation-torsion arguments cite it as the level-wise inventory of passive dressing. The body is a four-branch pattern match on the level index, wiring in the standard cube face and passive-edge counts.
Claim. For spatial dimension $d$, the passive subcell count at CW level $\ell$ is $0$ if $\ell=0$ (vertices), $\mathrm{passive\_field\_edges}(d)$ if $\ell=1$ (edges), $\mathrm{cube\_faces}(d)=2d$ if $\ell=2$ (faces), and $0$ otherwise (including the 3-cell interior).
background
The module derives generation torsion values ${0,11,17}$ as the unique schedule compatible with the 8-tick Hamiltonian cycle on the 3-cube $Q_3$, the Recognition Composition Law, and the $\varphi$-ladder. RCL in log-coordinates makes independent couplings add in the ladder exponent, so torsion is assembled from integer passive counts by CW level.
The cycle visits all 8 vertices along 8 edges. At each tick one edge is active and the rest of the 1-skeleton is passive field dressing; all 2-faces sit on that passive skeleton. Upstream, $\mathrm{passive_field_edges}(d)$ is total cube edges minus one active edge per tick (11 when $d=3$), and $\mathrm{cube_faces}(d)=2d$ (6 when $d=3$). Level 0 contributes nothing because the cycle already covers every vertex; the single 3-cell is interior and does not enter surface-mode coupling.
proof idea
Definition by cases on the level index: branch 0 returns 0; branch 1 returns the imported passive-field-edge count; branch 2 returns the imported cube-face count $2d$; the catch-all returns 0. No lemmas or tactics; the simp theorems passiveAtLevel_0 through _3 are immediate rfl or native_decide unfoldings at $D=3$.
why it matters
This inventory is the numeric backbone of torsion forcing. Downstream, profileTorsion sums selected level counts into candidate torsions; passiveAtLevel_matches_passiveCoupling ties it to the excitation-ordering coupling table; and the simp facts at levels 0–3 feed the RCL-forcing witness generationTorsion_is_rcl_forced, which realizes the three generations as the admissible lower-set profiles on the CW poset.
The CW prerequisite theorem uses it to exclude the face-only profile (torsion 6), which would otherwise spoil uniqueness of ${0,11,17}$. In the primer chain this sits after T7 (eight-tick octave) and T8 ($D=3$): the 8-tick Gray cycle on $Q_3$ partitions cells, and only downward-closed face/edge combinations survive, yielding the three generation slots bounded by face-pairs $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.