below
plain-language theorem explainer
Census-span obstruction for recognition cost J built from vertex ledger imbalance on the Freudenthal carrier. In 4D no rational kind-rate triple, with or without additive constant, matches J's moment vector; certificate u=(0,1,-2,2,0) kills the census and returns 192 on J. In 3D the triple alone fails, but adjoining a constant makes the 4×4 map onto (det −108), so the published inversion always returns rates and discriminates nothing; the free check j0=c_V fails (2≠−4). Closes the Gap-2 route that would fix posting rates from J.
Claim. Let $J$ be the recognition cost of a letter read from net ledger imbalance on the Freudenthal carrier. Write $m_V,m_E,m_T$ for the moment vectors of vertex/edge/top-cell counts on cube dilates, and $m_J$ for $J$'s moments. In 4D there are no $a,b,c\in\mathbb{Q}$ (nor $a,b,c,d$ with a constant column) such that $a m_V+b m_E+c m_T(+d\,1)=m_J$; the integer functional $u=(0,1,-2,2,0)$ annihilates all census columns and gives $\langle u,m_J\rangle=192$. In 3D the same holds without a constant (certificate $(0,1,-3,6)$). With a constant the $4\times 4$ census matrix has $\det=-108$, hence is onto, so every moment vector including $m_J$ lies in the span; the inverted rates satisfy $j_0=2\neq -4=c_V$.
background
Gap 2 asks whether the three free kind rates left by posting-plus-gluing can be fixed by reading recognition cost $J$ off the ledger imbalance the carrier already carries, then matching $J$'s census moments by aggregate-linear kind totals.
Ground truth is the kernel identity: recognition cost equals (net ledger imbalance)$^2$ over twice the Casimir. On the ordered-edge carrier every edge is one directed posting (debit head, credit tail). The ledger state of a vertex letter is therefore its indegree/outdegree pair; edge and top-cell letters are balanced or non-targets, so they cost zero. Bulk cancels on balanced vertices, so $J$ on a region accrues only at the boundary. Gauge equivariance ensures none of this is a labelling artifact.
Upstream, Gap2PostingCostDerivation reduces the measure to FixedKindTotals (total charge of each kind is a fixed multiple of that kind's count), and the fugacity-gluing layer leaves the three rates free. This module tests the remaining route: fix those rates from $J$'s census representation on Freudenthal cube dilates in 3D and 4D.
proof idea
The headline non-memberships are elementary linear algebra over $\mathbb{Q}$. Assume a rational combination of the kind-count moment columns equals $J$'s measured moments; project onto the middle coordinates; simp unfolds the explicit dilate tables; linarith derives a contradiction. The same pattern covers the 4D case with an extra constant column: the obstruction functional is blind to the constant.
Onto-ness in 3D with constant is the determinant computation $\det=-108\neq 0$ on the $4\times 4$ census matrix, so the map from rates-plus-constant to moments is bijective. The exhibited inverse is the published triple $c_E=(j_2-j_1)/6$, $c_V=(3j_1-j_2)/6$, $c_T=(j_3-j_2+(2/3)j_1)/6$. Evaluating on measured moments then gives the numerical mismatch $j_0=2$ versus $c_V=-4$, killing the free prediction that was supposed to carry content.
why it matters
Inside the Seven Gaps gravity program this is the negative verdict on Gap 2 / C2: $J$ induced from vertex-level ledger imbalance does not yield an aggregate-linear letter cost that could pin the three posting rates. The module doc is explicit that the bulk-boundary structure and dual-entry reading force edge and top-cell costs to zero, so the failure is structural, not a bad fit of constants.
The flag gap2_measure_derived is deliberately left untouched; only this imbalance-referent route is closed. Downstream cost algebra still uses the genuine $J$ (and the d'Alembert/RCL form $H(xy)+H(x/y)=2H(x)H(y)$ whose continuous solution is cosh), so the framework keeps T5's $J$-uniqueness while discarding a false census reading. The result also clarifies why a square invertible 3D system cannot be evidence: invertibility returns a triple for every input and therefore discriminates nothing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.