passiveCoupling_edge
plain-language theorem explainer
For spatial dimension D=3, the passive coupling count on edge cells equals 11. Mass and generation-torsion arguments cite this as the first nontrivial rung of the CW filtration schedule {0, 11, 17}. The proof is a one-line native decision of the closed arithmetic definition.
Claim. With spatial dimension $D=3$, the passive coupling attached to an edge cell of the $3$-cube equals $11$: one less than the twelve edges of $Q_3$, the active transition edge being excluded.
background
The module builds excitation ordering from the CW-filtration of the $D=3$ cube $Q_3$. The $0$-skeleton has $8$ vertices, the $1$-skeleton has $12$ edges, and the $2$-skeleton has $6$ faces. Generation excitations are assumed to couple to subcells in increasing CW dimension, producing the cumulative torsion schedule ${0, 11, 17}$.
Passive coupling counts how many subcells at a given CW level can absorb torsion without being the active transition. Vertices contribute $0$ (ground state). Edges contribute $\mathrm{cube_edges}(D)-1$; faces contribute all $\mathrm{cube_faces}(D)$. Spatial dimension $D$ is fixed at $3$ by the forcing chain (T8/T9).
The sibling definition passiveCoupling packages those three cases. The edge case is exactly the quantity evaluated here.
proof idea
One-line wrapper: native_decide evaluates the closed definition of passive coupling on the edge constructor at $D=3$. Unfolding gives $\mathrm{passive_field_edges},3 = 12-1 = 11$, which the kernel decides by computation. No intermediate lemmas are invoked.
why it matters
This pins the middle entry of the torsion schedule that the module derives from CW dimension: Gen 2 (first excitation) couples to the $1$-skeleton and accumulates torsion $11$. Together with the vertex value $0$ and the face value $6$ (total $17$), it supplies the geometric origin of the edge-before-face ordering that otherwise appears as an unexplained label in cube-admissible torsion.
J-cost monotonicity on $\varphi$-power ratios then yields the strict cost chain $J(\varphi^0)=0 < J(\varphi^{11}) < J(\varphi^{17})$. The result sits inside the masses domain and supports the filtration principle that replaces mode labels by a single geometric premise about coupling order. No downstream theorems currently depend on it in the graph; it is a local simp fact for the schedule arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.