passiveAtLevel_1
plain-language theorem explainer
At spatial dimension three, the passive edge count on the 3-cube under the eight-tick Hamiltonian cycle is exactly eleven. Mass and generation-torsion arguments cite this as the level-1 entry of the passive CW inventory that feeds the torsion triple {0, 11, 17}. The proof is a one-line native decision of the closed arithmetic definition.
Claim. With spatial dimension $D = 3$, the passive subcell count at CW level $1$ equals $11$: one edge of the $3$-cube is active on the eight-tick cycle and the remaining eleven edges form the passive field dressing.
background
The module derives generation torsion values ${0, 11, 17}$ as the unique inventory compatible with the eight-tick Hamiltonian cycle on the $3$-cube $Q_3$, projected onto the $\varphi$-ladder through the Recognition Composition Law. RCL makes independent couplings additive in the ladder exponent; the Gray cycle visits all eight vertices so that, at each tick, exactly one edge is active.
passiveAtLevel packages the passive subcell counts by CW dimension: level $0$ (vertices) is $0$ because the cycle sees every vertex; level $1$ (edges) is the passive-field-edge count; level $2$ (faces) is the six cube faces on the passive skeleton; higher levels vanish. Spatial dimension $D$ is fixed at $3$ by the forcing chain (T8/T9).
For $D=3$ the cube has $12$ edges, so with one active edge the passive count is $11$. That integer is the level-$1$ torsion channel used downstream in the generation ladder.
proof idea
One-line computational proof. Unfolding passiveAtLevel D 1 reduces to passive_field_edges 3, an explicit natural-number expression in $D=3$. native_decide evaluates the closed arithmetic and discharges equality to $11$. No lemmas beyond the definition and the constant $D=3$ are required.
why it matters
This simp fact locks the middle entry of the passive CW inventory that the torsion-forcing narrative identifies with generation charges. Module goal: show ${0, 11, 17}$ are the unique values compatible with the eight-tick cycle on $Q_3$, RCL additivity on the $\varphi$-ladder, and CW lower-set constraints. Level $1$ contributes the $11$; siblings cover levels $0$, $2$, $3$ and the match to passive coupling.
Framework landmarks: T7 eight-tick octave (period $2^3$), T8 forcing $D=3$, and RCL-driven additive torsion channels. No used_by edges are recorded yet; the declaration is local scaffolding for the uniqueness argument rather than a cited parent theorem. It closes the arithmetic side of the level-$1$ count so later uniqueness proofs can treat $11$ as a decided constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.