passiveCoupling_edge_pos

The module derives fermion generation torsion ordering from the CW filtration of the 3-cube $Q_3$. Skeletons are ordered by cell dimension: 8 vertices (dim 0), 12 edges (dim 1), 6 faces (dim 2). Generation excitations that couple in that order produce the cumulative torsion schedule ${0, 11, 17}$.

Passive coupling counts how many subcells at a given CW level can host passive field content. Vertices contribute 0 (ground state). Edges contribute $\mathrm{cube_edges}-1$ (one edge is the active transition), written passive_field_edges. Faces contribute all six faces. Spatial dimension $D$ is the forced value 3 from the T8/T9 chain.

The sibling definition passiveCoupling packages those three cases. This theorem only asserts positivity on the edge case, which is the first nontrivial excitation level.

One-line native_decide. After unfolding passiveCoupling D .edge to the concrete natural passive_field_edges 3 (equal to 11), Lean decides $0 < 11$ by computation. No intermediate lemmas are invoked.

In the excitation-ordering argument, Gen 2 is the first nontrivial mode and must add a positive edge torsion increment before faces appear. Positivity of the edge passive count is the arithmetic content of that claim: without it the schedule collapses and J-cost monotonicity $J(\varphi^0)=0 < J(\varphi^{11}) < J(\varphi^{17})$ cannot start.

The module frames this as the geometric reason edges precede faces in CubeAdmissibleTorsion, replacing ad hoc mode labels by CW dimension. No downstream theorems currently depend on this lemma in the graph, but it is the local positivity gate for the edge rung of that filtration story. The remaining open premise is still the filtration principle itself (excitations couple in CW order), not this arithmetic fact.