oT4
plain-language theorem explainer
Literal five-component rational vector (6, −6, 0, 0, 0) recording measured top-cell census moments on the 4D oblique region. Downstream census-span certificates and the C12 oriented-face verdict cite it as the T-column of the census matrix. The body is a pure array literal; no proof work.
Claim. Define the top-cell census moment vector on the four-dimensional oblique region by the rational 5-tuple $oT_4 = (6,-6,0,0,0)$, indexed by $i \in \{0,1,2,3,4\}$.
background
Gap 2 / C12 asks whether a recognition cost built from an oriented-face imbalance can lie in the linear span of the combinatorial census. The prior lane (vertex referent, Gap2JEhrhartSpan) already killed the vertex reading: its measured moment vector sits outside the census span in four dimensions. This module switches the referent one chain degree up, reading ordered top-cell incidence at faces via alternating facet signs and orientation comparison of ordered triples.
The census basis used in the span test is four rational 5-vectors: vertex moments, edge moments, top-cell moments, and a constant channel. The present definition supplies the top-cell column. Spatial dimension $D=3$ is the T8/T9 landmark in the forcing chain, but the span arithmetic here is run in four combinatorial dimensions on the oblique region (even and odd dilates share this same T-vector).
Upstream face maps (simplicial face inclusions, singular 2-simplex faces) justify why a top cell posts to codimension-one facets with signs $(-1)^i$; they are not invoked in the body of this literal.
proof idea
Definitional array literal. The map Fin 5 → ℚ is the concrete vector ![6, −6, 0, 0, 0] with no lemmas, no tactics, and no computation beyond the notation for a five-entry rational vector.
why it matters
Feeds the four-dimensional oriented-face census kill. The certificates ocert4e_annihilates_census and ocert4o_annihilates_census both require the T-dot to vanish, and the non-membership theorems oFor4e_not_in_census_span_with_const and oFor4o_not_in_census_span_with_const treat this vector as the c-coefficient column in the linear combination a·V + b·E + c·T + e·const. Those facts assemble into OrientedFaceSpanVerdict: the oriented-face cost is gauge equivariant, sums over letters, bulk-cancels, and its measured moments lie outside the exact census span on both region families and both parities. That closes pure surface terms for C12 after the vertex route was already killed. Landmark contact is local to Gap 2 gravity scaffolding rather than T5–T8 forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.