passiveAtLevel_matches_passiveCoupling
plain-language theorem explainer
Passive cell counts at CW levels 0–2 on the D-cube equal the passive coupling counts for vertices, edges, and faces from the excitation ordering. Anyone wiring the 8-tick Q₃ cycle into generation torsion cites this dictionary. The proof is definitional on the vertex case and closed by native decision on the edge and face cases.
Claim. For spatial dimension $D=3$, the passive count at CW level $0$ equals the passive vertex coupling, the passive count at level $1$ equals the passive edge coupling, and the passive count at level $2$ equals the passive face coupling.
background
The module derives generation torsion values ${0,11,17}$ as the unique numbers compatible with the 8-tick Hamiltonian cycle on the 3-cube $Q_3$, projected onto the $\varphi$-ladder through the Recognition Composition Law. At each tick one edge is active and the remaining skeleton is passive; those passive cells are grouped by CW dimension (vertices, edges, faces).
passiveAtLevel counts passive cells at a fixed CW level for dimension $D$. passiveCoupling (from ExcitationOrdering) assigns the corresponding coupling multiplicity to each CW cell type (vertex, edge, face). Spatial dimension is fixed at $D=3$ by the forcing chain (T8/T9). The CW attachment rule (faces attach along edges) later restricts admissible coupling profiles to lower sets in the CW poset; this lemma only equates the two counting schemes.
RCL enters the broader story as the reason independent couplings add in the $\varphi$-exponent ($J=\cosh-1$ from the d'Alembert form), but is not used in this equality.
proof idea
Term-mode proof. Split the three-way conjunction with refine ⟨rfl, ?_, ?_⟩. The level-0/vertex equality is definitional (rfl). The remaining two goals (level 1 vs edge, level 2 vs face) are closed by native_decide, which evaluates the concrete natural-number expressions at $D=3$. No external lemmas are invoked.
why it matters
This is the dictionary step between the geometric passive partition of the 8-tick cycle on $Q_3$ and the CW-level coupling language of ExcitationOrdering. Without it, the passive skeleton counts cannot be fed into the additive torsion-channel arithmetic that produces ${0,11,17}$.
It sits in part (B)–(C) of the module chain: Hamiltonian cycle partitions by CW level, then CW boundary structure forces level ordering. Downstream torsion theorems (RCL-additive channels, ground-state zero cost, face-pair generation bound) rely on these matched counts even though no used_by edges are recorded yet. Framework landmarks: T7 eight-tick octave, T8 $D=3$, and RCL-forced additive $\varphi$-ladder exponents. No open scaffold remains here; the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.