passiveCoupling_face_pos
plain-language theorem explainer
Face-type passive coupling on the D=3 cube is strictly positive. Cited when building the CW-cumulative torsion schedule that places face support after edge support in fermion generation. The proof is a one-line native_decide on the concrete numeric value of that coupling.
Claim. With spatial dimension $D=3$, the passive coupling attached to face-type subcells of the cube is strictly positive: $0 < C_{\mathrm{pass}}(D,\mathrm{face})$.
background
The module derives fermion generation torsion from the CW-filtration of the 3-cube $Q_3$. Subcells are stratified by CW dimension: 8 vertices (dim 0), 12 edges of which 11 are passive (dim 1), and 6 faces (dim 2). Passive coupling assigns to each cell type the numeric weight that generation excitations pick up when they first touch that skeleton.
Spatial dimension is the forced constant $D=3$ (T8/T9). The face cell is the CW-dim-2 class in the local CubeCell enumeration. Sibling facts already record the edge coupling and its positivity; this declaration is the matching face statement.
Under the filtration principle, generation 3 is the first mode that couples to 2-cells, adding the face weight to the cumulative torsion (canonical schedule ${0,11,17}$).
proof idea
Term-level tactic proof: native_decide. After unfolding passiveCoupling, D, and the face constructor, both sides are closed numeric expressions in \mathbb{N} (or a decidable ordered type), so the kernel decides $0 < C_{\mathrm{pass}}(3,\mathrm{face})$ by evaluation. No lemmas are invoked beyond decidable arithmetic.
why it matters
Closes the positivity half of the face rung in the CW-cumulative torsion story. Together with the edge positivity sibling and the dim-ordering facts (edge_dim_lt_face_dim), it underwrites the strict J-cost chain $J(\varphi^0)=0 < J(\varphi^{11}) < J(\varphi^{17})$ that the module advertises for generation excitations.
That chain is the structural reason edges precede faces in CubeAdmissibleTorsion, replacing ad-hoc mode labels by cube geometry plus J-monotonicity on $\varphi$-powers. No downstream consumers are wired yet in the graph; the declaration is local scaffolding for the Part-3 torsion schedule. It does not discharge the remaining filtration premise (that excitations couple in CW-dimension order).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.