passiveAtLevel_3
plain-language theorem explainer
At spatial dimension D = 3, the passive subcell count on the 3-cube at CW level 3 is definitionally zero. Anyone tracing the torsion-forcing chain that produces generation torsions {0, 11, 17} from the 8-tick Hamiltonian cycle will hit this simp fact when assembling passive coupling profiles by CW degree. The proof is pure reflexivity against the definition of the level-wise passive count.
Claim. For spatial dimension $D = 3$, the number of passive cells of the $3$-cube at CW level $3$ equals $0$.
background
The module derives generation torsion values ${0, 11, 17}$ as the unique profile compatible with the 8-tick Hamiltonian cycle on the 3-cube $Q_3$, the Recognition Composition Law, and the $\varphi$-ladder. Spatial dimension is fixed at $D = 3$ (T8 / linking).
The Gray cycle on $Q_3$ visits all eight vertices along eight edges. At each tick one edge is active and the remaining skeleton is passive; cells are then grouped by CW degree (vertices, edges, faces, volume). The function passiveAtLevel records how many cells of a given CW level sit in that passive partition.
Level 3 is the top cell of $Q_3$ (the single 3-volume). Sibling facts fix the counts at levels 0–2; this declaration closes the top degree. Downstream in the same file those counts are matched to the CW-level coupling tallies from ExcitationOrdering.
proof idea
Term-mode one-liner: rfl. Once $D$ is the constant $3$, the clause of passiveAtLevel at level $3$ reduces definitionally to $0$, so no lemma application is required. Marked @[simp] for automatic discharge in later equalities.
why it matters
Fills the top rung of the level-wise passive census used in the torsion-forcing derivation chain (module goal: unique compatibility of ${0, 11, 17}$ with 8-tick cycle $\times$ RCL $\times$ $\varphi$-ladder). Together with passiveAtLevel_0/1/2 it supplies the full passive profile that passiveAtLevel_matches_passiveCoupling equates to the ExcitationOrdering coupling counts.
That census feeds the CW-boundary lower-set constraint (faces require edges) and the additive torsion channels forced by RCL in log-coordinates. No external used_by edges are recorded yet; the immediate consumers are the sibling matching and torsion-assembly lemmas in this module. Framework landmarks: T8 ($D = 3$), the eight-tick octave on $Q_3$, and RCL additivity of ladder exponents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.