face_has_edge_boundary
plain-language theorem explainer
For dimension d ≥ 1, a positive face count on the d-cube forces a positive edge count. Torsion-forcing and mass arguments that treat faces as coupling channels cite this to enforce the CW lower-set rule: faces attach only along edges. The proof is a short natural-number inequality after unfolding the edge formula d·2^(d−1).
Claim. For every natural number $d$ with $d \ge 1$, if the $d$-cube has positively many faces ($2d > 0$), then it has positively many edges ($d \cdot 2^{d-1} > 0$).
background
Hypercube counts used across the monolith set the number of faces of the $d$-cube to $2d$ and the number of edges to $d \cdot 2^{d-1}$. At $d=3$ this is $Q_3$: six faces and twelve edges, the 1-skeleton supporting the eight-tick Gray cycle.
The TorsionForcing module derives generation torsion values ${0,11,17}$ from that 8-tick Hamiltonian cycle, the Recognition Composition Law, and the $\varphi$-ladder. Module section (C) records the CW fact that 2-cells (faces) attach along 1-cells (edges), so any coupling profile that activates faces must already activate edges. That lower-set restriction on the CW poset is the local setting for this lemma.
proof idea
Introduce $d$, the bound $d \ge 1$, and the face-positivity hypothesis. Unfold the edge count to $d \cdot 2^{d-1}$. Compare it to $1 \cdot 2^0$ by Nat.mul_le_mul on $d \ge 1$ and $2^{d-1} \ge 2^0$ (the power step via Nat.pow_le_pow_right with norm_num/omega), then reduce the right-hand side to 1. Face positivity is not used in the arithmetic; it only shapes the implication to match the CW narrative.
why it matters
This is the combinatorial half of the CW boundary prerequisite in the torsion-forcing chain: admissible coupling profiles on $Q_3$ must be downward-closed in the CW filtration. Without a nonempty edge skeleton whenever faces are present, face-level passive couplings could appear without edge support and break the partition into passive subcell groups by CW level that selects the unique torsion set ${0,11,17}$.
The module links that partition to the eight-tick octave (T7) and spatial dimension $D=3$ (T8). The dependency graph currently lists no downstream users, so the lemma is local infrastructure for the lower-set argument rather than a widely cited bridge. It discharges the count-level "faces imply edges" direction stated in the module doc; it does not by itself enumerate the four edges of a square face.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.