IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpan

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCostDerivation
   2
   3/-!
   4# Gap 2 / C2: the recognition cost of a letter in context, and the census span test
   5
   6`Gap2PostingCostDerivation` reduces the measure to **aggregate linearity by kind**
   7(`FixedKindTotals`): the total charge of each kind is a fixed multiple of that kind's
   8count.  `Gap2FugacityPostingGluing` then showed the posting layer plus the gluing law
   9leaves the three rates entirely free.  The route this module tests is the one that
  10would fix them: define the recognition cost `J` of a letter from the **imbalance**
  11structure the ledger layer already carries, and read the three rates off its
  12census representation.
  13
  14## §1-§2.  What `J` is, and that it is derived rather than stipulated
  15
  16Ground truth is the kernel identity
  17`ChartFromLedgerMomentum.Jlog_eq_imbalance_sq_div_two_casimir`:
  18
  19    recognition cost  =  (net ledger imbalance) ^ 2 / (2 * Casimir).
  20
  21The complex-level ledger state of a letter is supplied by the carrier and not
  22invented here.  `BoundedComplex.edgeVerts` is an **ordered** pair, so every edge is
  23one directed recognition posting: it debits its head and credits its tail.  The
  24ledger state of a vertex letter `v` inside a complex `K` is therefore
  25`(indeg K v, outdeg K v)`, its net imbalance is `vertexImbalance K v`, and its
  26recognition cost is that imbalance squared over twice the Casimir (`jCost`).  An
  27edge letter is itself one balanced posting, one debit and one credit, so its
  28imbalance is zero; a top-cell letter is not a posting target, so its imbalance is
  29zero.  Both are charged nothing, which is a consequence of the dual-entry reading
  30and not a modelling choice made to be convenient.
  31
  32Three properties are recorded because the route needs all three.  `jCost` is a
  33legitimate `LetterCost`, since the kernel's `LetterCost` already sees the whole
  34complex as well as the letter, so context dependence is the general case
  35(`jCost` needs no amendment to state).  It is gauge equivariant
  36(`jCost_equivariant`), so nothing below is an artifact of a labelling.  And the
  37bulk cancels: a vertex whose incident postings pair up is charged nothing
  38(`jCost_vanishes_on_balanced_vertex`), which is why `J` on a region of the
  39Freudenthal carrier accrues only at the boundary.
  40
  41## §3.  The verdict: `J` induces no aggregate-linear letter cost
  42
  43`jCost` is **not** `FixedKindTotals`, and the failing configuration is two
  44complexes with two cells between them.  A single vertex has no incident postings,
  45so its imbalance is zero, so the vertex block sums to zero, so `cV = 0`.  A single
  46edge has two vertices of imbalance one, so its vertex block sums to `1 / kappa`,
  47which must be `cV * 2 = 0`.  For any nonzero Casimir that is a contradiction
  48(`jCost_not_fixedKindTotals`).
  49
  50The same quadratic is why `J` is not a valuation.  A two-edge path is two edges
  51glued along one vertex; the interface **imbalances** cancel exactly, so the middle
  52vertex is charged nothing, but the two edge **costs** do not cancel, and the path
  53costs `1 / kappa` against the `2 / kappa` a valuation would give
  54(`jCost_not_a_valuation`).  Bulk cancellation inside the square and additivity of
  55the square are different properties, and only the first one holds.
  56
  57## §4-§5.  The census span test, and the 3D test's vacuity
  58
  59§4 carries the moment vectors measured by exact enumeration of the Freudenthal
  60(Kuhn) carrier on dilates of a cube region, in the basis `(N^d, ..., N, 1)`.
  61Those numbers are MEASURED (`scripts/qg/qg_j_ehrhart_span_20260730.py`, exact
  62integer arithmetic, quasi-polynomial fits verified on held-out dilates); every
  63theorem below is a THEOREM about them.
  64
  65* In four dimensions no rational triple of kind rates, and no triple plus an
  66  additive constant, reproduces `J`'s moment vector
  67  (`J4_not_in_census_span`, `J4_not_in_census_span_with_const`).  The obstruction
  68  is a single integer functional of the moments,
  69  `u = (0, 1, -2, 2, 0)`, which annihilates all three counts and the constant and
  70  returns `192` on `J` (`cert4_annihilates_census`, `cert4_sees_J4`).
  71* In three dimensions the same holds for the three counts alone
  72  (`J3_not_in_census_span`, certificate `(0, 1, -3, 6)`).
  73* **But the three-dimensional test with a constant column cannot fail.**  Its
  74  4-by-4 matrix has determinant `-108`, so the map from rates to moments is onto:
  75  *every* moment vector is in the span, `J`'s included
  76  (`census3_with_const_is_onto`, `census3_det`).  The inversion that theorem
  77  exhibits is exactly the published one,
  78  `c_E = (j2 - j1)/6`, `c_V = (3 j1 - j2)/6`, `c_T = (j3 - j2 + (2/3) j1)/6`, whose
  79  arithmetic is correct; what fails is the reading, because a square invertible
  80  system returns a triple for any input whatever and so discriminates nothing.
  81  The free prediction that was supposed to carry the content, `j0 = c_V`, is false
  82  on the measured moments: `j0 = 2` while `c_V = -4` (`j0_ne_cV_3D`).
  83
  84## Scope
  85
  86The verdict is exactly as strong as the object it is about: the recognition cost
  87built from vertex-level ledger imbalance on the Freudenthal carrier, over the
  88region families enumerated.  It closes that route and says nothing about a cost
  89built from some other imbalance referent.  It does not flip any flag; flag
  90`gap2_measure_derived` stays as it was, with its premise unchanged.
  91
  92Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
  93-/
  94
  95namespace IndisputableMonolith
  96namespace Gravity
  97namespace SevenGaps
  98namespace Gap2JEhrhartSpan
  99
 100open PathSumMeasure GaugeHistoryMeasure Gap2PostingCostDerivation
 101
 102variable {B : ℕ}
 103
 104/-! ## §1. The ledger state of a vertex letter, from the carrier's own incidence -/
 105
 106/-- Out-postings at a vertex: edges whose ordered first endpoint is `v`.  These are
 107the credits of the dual-entry reading. -/
 108def outdeg (K : BoundedComplex B) (v : Fin K.nV) : ℕ :=
 109  (Finset.univ.filter fun e : Fin K.nE => (K.edgeVerts e).1 = v).card
 110
 111/-- In-postings at a vertex: edges whose ordered second endpoint is `v`.  These are
 112the debits. -/
 113def indeg (K : BoundedComplex B) (v : Fin K.nV) : ℕ :=
 114  (Finset.univ.filter fun e : Fin K.nE => (K.edgeVerts e).2 = v).card
 115
 116/-- **The net recognition imbalance of a vertex letter in context**: debits minus
 117credits, read off the carrier's ordered edge incidence.  Nothing is stipulated: the
 118ordering is already in `BoundedComplex.edgeVerts`. -/
 119def vertexImbalance (K : BoundedComplex B) (v : Fin K.nV) : ℤ :=
 120  (indeg K v : ℤ) - (outdeg K v : ℤ)
 121
 122/-- The squared-imbalance total of a complex, the integer part of `J`. -/
 123def imbalanceSq (K : BoundedComplex B) : ℤ :=
 124  ∑ v : Fin K.nV, (vertexImbalance K v) ^ 2
 125
 126theorem indeg_eq_sum (K : BoundedComplex B) (v : Fin K.nV) :
 127    indeg K v = ∑ e : Fin K.nE, if (K.edgeVerts e).2 = v then 1 else 0 := by
 128  classical
 129  simp only [indeg, Finset.card_filter]
 130
 131theorem outdeg_eq_sum (K : BoundedComplex B) (v : Fin K.nV) :
 132    outdeg K v = ∑ e : Fin K.nE, if (K.edgeVerts e).1 = v then 1 else 0 := by
 133  classical
 134  simp only [outdeg, Finset.card_filter]
 135
 136/-! ## §2. `jCost`: the derived letter cost, and its three needed properties -/
 137
 138noncomputable section
 139
 140/-- **The recognition cost of a letter in context.**  A vertex letter is charged its
 141net ledger imbalance squared over twice the Casimir, which is the kernel identity
 142`Jlog_eq_imbalance_sq_div_two_casimir` evaluated at the letter's own ledger state.
 143An edge letter is one balanced posting and a top-cell letter is not a posting
 144target, so both carry zero imbalance and zero charge. -/
 145def jCost (kappa : ℝ) : LetterCost := fun _ K a =>
 146  match a with
 147  | Sum.inl v => ((vertexImbalance K v : ℝ)) ^ 2 / (2 * kappa)
 148  | Sum.inr _ => 0
 149
 150@[simp] theorem jCost_inl (kappa : ℝ) (B : ℕ) (K : BoundedComplex B) (v : Fin K.nV) :
 151    jCost kappa B K (Sum.inl v) = ((vertexImbalance K v : ℝ)) ^ 2 / (2 * kappa) := rfl
 152
 153@[simp] theorem jCost_edge (kappa : ℝ) (B : ℕ) (K : BoundedComplex B) (e : Fin K.nE) :
 154    jCost kappa B K (Sum.inr (Sum.inl e)) = 0 := rfl
 155
 156@[simp] theorem jCost_tet (kappa : ℝ) (B : ℕ) (K : BoundedComplex B) (t : Fin K.nT) :
 157    jCost kappa B K (Sum.inr (Sum.inr t)) = 0 := rfl
 158
 159/-- **`J` is the sum over its letters.**  The weak form of local additivity holds by
 160construction: the history cost of `jCost` is the vertex block sum, because the other
 161two blocks are silent. -/
 162theorem historyCost_jCost (kappa : ℝ) (B : ℕ) (K : BoundedComplex B) :
 163    historyCost (jCost kappa) B K
 164      = ∑ v : Fin K.nV, jCost kappa B K (Sum.inl v) := by
 165  classical
 166  unfold historyCost
 167  rw [Fintype.sum_sum_type, Fintype.sum_sum_type]
 168  simp
 169
 170/-- **Bulk cancellation, at the letter.**  A vertex whose incident postings pair up
 171carries zero imbalance and is charged nothing.  This is why `J` on a region of the
 172Freudenthal carrier accrues only on the boundary: an interior vertex has one
 173in-posting and one out-posting per displacement class. -/
 174theorem jCost_vanishes_on_balanced_vertex (kappa : ℝ) (B : ℕ) (K : BoundedComplex B)
 175    (v : Fin K.nV) (h : indeg K v = outdeg K v) :
 176    jCost kappa B K (Sum.inl v) = 0 := by
 177  have : vertexImbalance K v = 0 := by
 178    simp [vertexImbalance, h]
 179  simp [jCost_inl, this]
 180
 181end
 182
 183/-! ### Equivariance: the failure below is not a labelling artifact -/
 184
 185theorem indeg_relabel {K K' : BoundedComplex B} (r : Relabel K K') (v : Fin K.nV) :
 186    indeg K v = indeg K' (r.vEquiv v) := by
 187  classical
 188  rw [indeg_eq_sum, indeg_eq_sum]
 189  refine Fintype.sum_equiv r.eEquiv _ _ ?_
 190  intro e
 191  rw [r.edge_comm e]
 192  by_cases h : (K.edgeVerts e).2 = v
 193  · simp [Prod.map, h]
 194  · have h' : ¬ (r.vEquiv ((K.edgeVerts e).2) = r.vEquiv v) := by
 195      intro hh; exact h (r.vEquiv.injective hh)
 196    simp [Prod.map, h, h']
 197
 198theorem outdeg_relabel {K K' : BoundedComplex B} (r : Relabel K K') (v : Fin K.nV) :
 199    outdeg K v = outdeg K' (r.vEquiv v) := by
 200  classical
 201  rw [outdeg_eq_sum, outdeg_eq_sum]
 202  refine Fintype.sum_equiv r.eEquiv _ _ ?_
 203  intro e
 204  rw [r.edge_comm e]
 205  by_cases h : (K.edgeVerts e).1 = v
 206  · simp [Prod.map, h]
 207  · have h' : ¬ (r.vEquiv ((K.edgeVerts e).1) = r.vEquiv v) := by
 208      intro hh; exact h (r.vEquiv.injective hh)
 209    simp [Prod.map, h, h']
 210
 211theorem vertexImbalance_relabel {K K' : BoundedComplex B} (r : Relabel K K')
 212    (v : Fin K.nV) : vertexImbalance K v = vertexImbalance K' (r.vEquiv v) := by
 213  simp [vertexImbalance, indeg_relabel r v, outdeg_relabel r v]
 214
 215/-- **`jCost` is gauge equivariant.**  Labels are gauge for it, so every negative
 216result below is about the cost and not about a choice of names. -/
 217theorem jCost_equivariant (kappa : ℝ) : Equivariant (jCost kappa) := by
 218  intro B K K' r a
 219  cases a with
 220  | inl v =>
 221      simp only [postingAlphEquiv, Equiv.sumCongr_apply, Sum.map_inl, jCost_inl]
 222      rw [vertexImbalance_relabel r v]
 223  | inr b =>
 224      cases b with
 225      | inl e => simp [postingAlphEquiv]
 226      | inr t => simp [postingAlphEquiv]
 227
 228/-! ## §3. The verdict: no aggregate-linear letter cost, and no valuation
 229
 230Four explicit complexes at cap `4`.  `pointComplex` is one vertex; `edgeComplex` is
 231one edge; `pathComplex` is two edges glued along a vertex; `twoEdgeComplex` is two
 232disjoint edges. -/
 233
 234/-- One vertex, no edges, no top cells. -/
 235def pointComplex : BoundedComplex 4 where
 236  nV := 1
 237  nE := 0
 238  nT := 0
 239  hV := by decide
 240  hE := by decide
 241  hT := by decide
 242  edgeVerts := fun e => e.elim0
 243  tetVerts := fun t => t.elim0
 244
 245/-- One directed edge `0 -> 1`. -/
 246def edgeComplex : BoundedComplex 4 where
 247  nV := 2
 248  nE := 1
 249  nT := 0
 250  hV := by decide
 251  hE := by decide
 252  hT := by decide
 253  edgeVerts := fun _ => (0, 1)
 254  tetVerts := fun t => t.elim0
 255
 256/-- Two edges glued along one vertex: `0 -> 1 -> 2`. -/
 257def pathComplex : BoundedComplex 4 where
 258  nV := 3
 259  nE := 2
 260  nT := 0
 261  hV := by decide
 262  hE := by decide
 263  hT := by decide
 264  edgeVerts := fun e => if e = 0 then (0, 1) else (1, 2)
 265  tetVerts := fun t => t.elim0
 266
 267/-- Two disjoint edges: `0 -> 1` and `2 -> 3`. -/
 268def twoEdgeComplex : BoundedComplex 4 where
 269  nV := 4
 270  nE := 2
 271  nT := 0
 272  hV := by decide
 273  hE := by decide
 274  hT := by decide
 275  edgeVerts := fun e => if e = 0 then (0, 1) else (2, 3)
 276  tetVerts := fun t => t.elim0
 277
 278theorem imbalance_point : ∀ v : Fin pointComplex.nV, vertexImbalance pointComplex v = 0 := by
 279  decide
 280
 281theorem imbalance_edge_zero : vertexImbalance edgeComplex (0 : Fin 2) = -1 := by decide
 282
 283theorem imbalance_edge_one : vertexImbalance edgeComplex (1 : Fin 2) = 1 := by decide
 284
 285theorem imbalance_path_zero : vertexImbalance pathComplex (0 : Fin 3) = -1 := by decide
 286
 287theorem imbalance_path_one : vertexImbalance pathComplex (1 : Fin 3) = 0 := by decide
 288
 289theorem imbalance_path_two : vertexImbalance pathComplex (2 : Fin 3) = 1 := by decide
 290
 291/-- **Non-vacuity of the bulk-cancellation clause.**  On the two-edge path the
 292middle vertex really is balanced and the two ends really are not, so
 293`jCost_vanishes_on_balanced_vertex` has an instance and a non-instance on the same
 294complex. -/
 295theorem path_middle_balanced_ends_not :
 296    indeg pathComplex (1 : Fin 3) = outdeg pathComplex (1 : Fin 3)
 297      ∧ indeg pathComplex (0 : Fin 3) ≠ outdeg pathComplex (0 : Fin 3)
 298      ∧ indeg pathComplex (2 : Fin 3) ≠ outdeg pathComplex (2 : Fin 3) := by
 299  decide
 300
 301noncomputable section
 302
 303theorem blockSum_point (kappa : ℝ) :
 304    (∑ v : Fin pointComplex.nV, jCost kappa 4 pointComplex (Sum.inl v)) = 0 := by
 305  simp [jCost_inl, imbalance_point]
 306
 307theorem blockSum_edge (kappa : ℝ) (hk : kappa ≠ 0) :
 308    (∑ v : Fin edgeComplex.nV, jCost kappa 4 edgeComplex (Sum.inl v)) = 1 / kappa := by
 309  show (∑ v : Fin 2, jCost kappa 4 edgeComplex (Sum.inl v)) = 1 / kappa
 310  rw [Fin.sum_univ_two]
 311  simp only [jCost_inl, imbalance_edge_zero, imbalance_edge_one]
 312  push_cast
 313  field_simp <;> norm_num
 314
 315theorem blockSum_path (kappa : ℝ) (hk : kappa ≠ 0) :
 316    (∑ v : Fin pathComplex.nV, jCost kappa 4 pathComplex (Sum.inl v)) = 1 / kappa := by
 317  show (∑ v : Fin 3, jCost kappa 4 pathComplex (Sum.inl v)) = 1 / kappa
 318  rw [Fin.sum_univ_three]
 319  simp only [jCost_inl, imbalance_path_zero, imbalance_path_one, imbalance_path_two]
 320  push_cast
 321  field_simp <;> norm_num
 322
 323/-- **HEADLINE (the route fails at the letter).**  For every nonzero Casimir the
 324derived cost has no fixed kind totals, so it induces no additive letter cost by kind
 325and `measure_from_fixedKindTotals` cannot be applied to it.  The witness is two
 326complexes: a single vertex forces `cV = 0`, and a single edge then demands
 327`1 / kappa = 0`. -/
 328theorem jCost_not_fixedKindTotals (kappa : ℝ) (hk : kappa ≠ 0) :
 329    ¬ FixedKindTotals (jCost kappa) := by
 330  rintro ⟨cV, cE, cT, h⟩
 331  have hp := (h 4 pointComplex).1
 332  have he := (h 4 edgeComplex).1
 333  rw [blockSum_point kappa] at hp
 334  rw [blockSum_edge kappa hk] at he
 335  have h1 : ((pointComplex.nV : ℕ) : ℝ) = 1 := by
 336    show ((1 : ℕ) : ℝ) = 1
 337    norm_num
 338  have h2 : ((edgeComplex.nV : ℕ) : ℝ) = 2 := by
 339    show ((2 : ℕ) : ℝ) = 2
 340    norm_num
 341  rw [h1, mul_one] at hp
 342  rw [h2] at he
 343  have hcV : cV = 0 := hp.symm
 344  rw [hcV] at he
 345  have hz : (1 : ℝ) / kappa = 0 := by linarith
 346  exact (one_div_ne_zero hk) hz
 347
 348/-- **The gluing failure, stated as arithmetic on three explicit complexes.**  The
 349two-edge path is two edges glued along one vertex, whose intersection is a single
 350vertex.  A valuation would give `1/kappa + 1/kappa - 0`; the path gives `1/kappa`.
 351The interface imbalances cancel exactly, and the interface costs do not. -/
 352theorem jCost_not_a_valuation (kappa : ℝ) (hk : kappa ≠ 0) :
 353    historyCost (jCost kappa) 4 pathComplex
 354      ≠ historyCost (jCost kappa) 4 edgeComplex
 355        + historyCost (jCost kappa) 4 edgeComplex
 356        - historyCost (jCost kappa) 4 pointComplex := by
 357  rw [historyCost_jCost, historyCost_jCost, historyCost_jCost,
 358    blockSum_path kappa hk, blockSum_edge kappa hk, blockSum_point kappa]
 359  intro h
 360  have : (1 : ℝ) / kappa = 0 := by linarith
 361  exact (one_div_ne_zero hk) this
 362
 363end
 364
 365/-! ## §4. The census span test on the measured moment vectors
 366
 367Moment vectors of the Freudenthal (Kuhn) carrier on cube dilates `R_N`, in the
 368basis `(N^d, ..., N, 1)`.  MEASURED by exact enumeration
 369(`scripts/qg/qg_j_ehrhart_span_20260730.py`); the fits reproduce held-out dilates
 370exactly, and both parity constituents of the period-doubled cell agree, so the
 371period-2 quasi-polynomial is a polynomial on this family.
 372
 373`mJ4` is the moment vector of `2 * kappa * J`, whose leading coefficient is exactly
 374zero: `J` is a boundary functional of degree three in four dimensions. -/
 375
 376/-- Vertex census of the 4D cube dilate: `(N+1)^4`. -/
 377def mV4 : Fin 5 → ℚ := ![1, 4, 6, 4, 1]
 378
 379/-- Edge census of the 4D cube dilate over the fifteen displacement classes:
 380`(2N+1)^4 - (N+1)^4`. -/
 381def mE4 : Fin 5 → ℚ := ![15, 28, 18, 4, 0]
 382
 383/-- Kuhn 4-simplex census of the 4D cube dilate: `24 N^4`. -/
 384def mT4 : Fin 5 → ℚ := ![24, 0, 0, 0, 0]
 385
 386/-- The constant column. -/
 387def mC4 : Fin 5 → ℚ := ![0, 0, 0, 0, 1]
 388
 389/-- MEASURED moment vector of `2 * kappa * J` on the 4D cube dilate. -/
 390def mJ4 : Fin 5 → ℚ := ![0, 512, 192, 32, 2]
 391
 392/-- The obstruction functional: the integer combination of boundary strata that
 393every census column is blind to. -/
 394def cert4 : Fin 5 → ℚ := ![0, 1, -2, 2, 0]
 395
 396def dot4 (u w : Fin 5 → ℚ) : ℚ := ∑ i, u i * w i
 397
 398theorem cert4_annihilates_census :
 399    dot4 cert4 mV4 = 0 ∧ dot4 cert4 mE4 = 0 ∧ dot4 cert4 mT4 = 0
 400      ∧ dot4 cert4 mC4 = 0 := by
 401  refine ⟨?_, ?_, ?_, ?_⟩ <;>
 402    simp [dot4, cert4, mV4, mE4, mT4, mC4, Fin.sum_univ_five] <;> norm_num
 403
 404theorem cert4_sees_J4 : dot4 cert4 mJ4 = 192 := by
 405  simp [dot4, cert4, mJ4, Fin.sum_univ_five]
 406  norm_num
 407
 408/-- **HEADLINE (outside the census span, four dimensions).**  No rational triple of
 409kind rates reproduces `J`'s measured moment vector on the 4D Freudenthal cube
 410dilate. -/
 411theorem J4_not_in_census_span :
 412    ¬ ∃ a b c : ℚ, ∀ i : Fin 5, a * mV4 i + b * mE4 i + c * mT4 i = mJ4 i := by
 413  rintro ⟨a, b, c, h⟩
 414  have h1 := h 1
 415  have h2 := h 2
 416  have h3 := h 3
 417  simp [mV4, mE4, mT4, mJ4] at h1 h2 h3
 418  linarith
 419
 420/-- **The same with an additive constant allowed.**  Adding a constant column does
 421not rescue it: the obstruction functional is blind to the constant too. -/
 422theorem J4_not_in_census_span_with_const :
 423    ¬ ∃ a b c d : ℚ,
 424      ∀ i : Fin 5, a * mV4 i + b * mE4 i + c * mT4 i + d * mC4 i = mJ4 i := by
 425  rintro ⟨a, b, c, d, h⟩
 426  have h1 := h 1
 427  have h2 := h 2
 428  have h3 := h 3
 429  simp [mV4, mE4, mT4, mC4, mJ4] at h1 h2 h3
 430  linarith
 431
 432/-! ### The three-dimensional carrier, and why its published test cannot fail -/
 433
 434def mV3 : Fin 4 → ℚ := ![1, 3, 3, 1]
 435def mE3 : Fin 4 → ℚ := ![7, 9, 3, 0]
 436def mT3 : Fin 4 → ℚ := ![6, 0, 0, 0]
 437def mC3 : Fin 4 → ℚ := ![0, 0, 0, 1]
 438
 439/-- MEASURED moment vector of `2 * kappa * J` on the 3D cube dilate. -/
 440def mJ3 : Fin 4 → ℚ := ![0, 96, 24, 2]
 441
 442def cert3 : Fin 4 → ℚ := ![0, 1, -3, 6]
 443
 444def dot3 (u w : Fin 4 → ℚ) : ℚ := ∑ i, u i * w i
 445
 446theorem cert3_annihilates_counts :
 447    dot3 cert3 mV3 = 0 ∧ dot3 cert3 mE3 = 0 ∧ dot3 cert3 mT3 = 0 := by
 448  refine ⟨?_, ?_, ?_⟩ <;>
 449    simp [dot3, cert3, mV3, mE3, mT3, Fin.sum_univ_four] <;> norm_num
 450
 451theorem cert3_sees_J3 : dot3 cert3 mJ3 = 36 := by
 452  simp [dot3, cert3, mJ3, Fin.sum_univ_four]
 453  norm_num
 454
 455/-- No rational triple of kind rates reproduces `J`'s measured moment vector on the
 4563D Freudenthal cube dilate either. -/
 457theorem J3_not_in_census_span :
 458    ¬ ∃ a b c : ℚ, ∀ i : Fin 4, a * mV3 i + b * mE3 i + c * mT3 i = mJ3 i := by
 459  rintro ⟨a, b, c, h⟩
 460  have h1 := h 1
 461  have h2 := h 2
 462  have h3 := h 3
 463  simp [mV3, mE3, mT3, mJ3] at h1 h2 h3
 464  linarith
 465
 466/-- The published 3D census determinant, recomputed: `-108`, with the rows the four
 467boundary strata `(N^3, N^2, N, 1)` and the columns `(n_V, n_E, n_T, 1)`. -/
 468theorem census3_det :
 469    Matrix.det !![mV3 0, mE3 0, mT3 0, mC3 0;
 470                  mV3 1, mE3 1, mT3 1, mC3 1;
 471                  mV3 2, mE3 2, mT3 2, mC3 2;
 472                  mV3 3, mE3 3, mT3 3, mC3 3] = -108 := by
 473  simp [mV3, mE3, mT3, mC3, Matrix.det_succ_row_zero, Fin.sum_univ_succ,
 474    Matrix.det_fin_three, Fin.succAbove] <;> norm_num
 475
 476/-- **The three-dimensional test with a constant column is vacuous.**  The 4-by-4
 477census matrix is invertible, so the map from rates to moments is onto: for *every*
 478target moment vector a triple plus a constant exists, so no target can ever be
 479found outside the span and the test discriminates nothing.  The exhibited inversion
 480is exactly the published one, `c_E = (j2 - j1)/6`, `c_V = (3 j1 - j2)/6`,
 481`c_T = (j3 - j2 + (2/3) j1)/6`, `c_0 = j0 - c_V`, whose arithmetic is correct. -/
 482theorem census3_with_const_is_onto (t : Fin 4 → ℚ) :
 483    ∃ a b c d : ℚ,
 484      ∀ i : Fin 4, a * mV3 i + b * mE3 i + c * mT3 i + d * mC3 i = t i := by
 485  refine ⟨(3 * t 2 - t 1) / 6, (t 1 - t 2) / 6,
 486    (t 0 - t 1 + (2 / 3) * t 2) / 6, t 3 - (3 * t 2 - t 1) / 6, ?_⟩
 487  intro i
 488  fin_cases i <;> simp [mV3, mE3, mT3, mC3] <;> ring
 489
 490/-- **The free prediction fails.**  `j0 = c_V` was the one independent consequence
 491the 3D inversion had left, and on the measured moments it is false: `j0 = 2` while
 492`c_V = -4`. -/
 493theorem j0_ne_cV_3D :
 494    mJ3 3 ≠ (3 * mJ3 2 - mJ3 1) / 6 := by
 495  simp [mJ3]
 496  norm_num
 497
 498/-! ## §5. Certificate -/
 499
 500/-- **The C2 span-test verdict.**  The derived cost is a gauge-equivariant letter
 501cost whose bulk cancels and which is the sum over its letters; it has no fixed kind
 502totals, it is not a valuation, and its measured moment vector lies outside the
 503census span in four dimensions with or without a constant column.  The published
 504three-dimensional inversion is arithmetically correct and vacuous, and its one free
 505prediction is false. -/
 506structure JEhrhartSpanVerdict : Prop where
 507  equivariant : ∀ kappa : ℝ, Equivariant (jCost kappa)
 508  bulk_cancels : ∀ (kappa : ℝ) (B : ℕ) (K : BoundedComplex B) (v : Fin K.nV),
 509    indeg K v = outdeg K v → jCost kappa B K (Sum.inl v) = 0
 510  sum_over_letters : ∀ (kappa : ℝ) (B : ℕ) (K : BoundedComplex B),
 511    historyCost (jCost kappa) B K = ∑ v : Fin K.nV, jCost kappa B K (Sum.inl v)
 512  no_kind_totals : ∀ kappa : ℝ, kappa ≠ 0 → ¬ FixedKindTotals (jCost kappa)
 513  not_a_valuation : ∀ kappa : ℝ, kappa ≠ 0 →
 514    historyCost (jCost kappa) 4 pathComplex
 515      ≠ historyCost (jCost kappa) 4 edgeComplex
 516        + historyCost (jCost kappa) 4 edgeComplex
 517        - historyCost (jCost kappa) 4 pointComplex
 518  outside_span_4d :
 519    ¬ ∃ a b c : ℚ, ∀ i : Fin 5, a * mV4 i + b * mE4 i + c * mT4 i = mJ4 i
 520  outside_span_4d_with_const :
 521    ¬ ∃ a b c d : ℚ,
 522      ∀ i : Fin 5, a * mV4 i + b * mE4 i + c * mT4 i + d * mC4 i = mJ4 i
 523  outside_span_3d :
 524    ¬ ∃ a b c : ℚ, ∀ i : Fin 4, a * mV3 i + b * mE3 i + c * mT3 i = mJ3 i
 525  three_d_test_vacuous : ∀ t : Fin 4 → ℚ, ∃ a b c d : ℚ,
 526    ∀ i : Fin 4, a * mV3 i + b * mE3 i + c * mT3 i + d * mC3 i = t i
 527  three_d_determinant :
 528    Matrix.det !![mV3 0, mE3 0, mT3 0, mC3 0;
 529                  mV3 1, mE3 1, mT3 1, mC3 1;
 530                  mV3 2, mE3 2, mT3 2, mC3 2;
 531                  mV3 3, mE3 3, mT3 3, mC3 3] = -108
 532  free_prediction_fails : mJ3 3 ≠ (3 * mJ3 2 - mJ3 1) / 6
 533
 534theorem jEhrhartSpanVerdict : JEhrhartSpanVerdict where
 535  equivariant := jCost_equivariant
 536  bulk_cancels := jCost_vanishes_on_balanced_vertex
 537  sum_over_letters := historyCost_jCost
 538  no_kind_totals := jCost_not_fixedKindTotals
 539  not_a_valuation := jCost_not_a_valuation
 540  outside_span_4d := J4_not_in_census_span
 541  outside_span_4d_with_const := J4_not_in_census_span_with_const
 542  outside_span_3d := J3_not_in_census_span
 543  three_d_test_vacuous := census3_with_const_is_onto
 544  three_d_determinant := census3_det
 545  free_prediction_fails := j0_ne_cV_3D
 546
 547/-! ## Axiom audit -/
 548
 549#print axioms historyCost_jCost
 550#print axioms jCost_vanishes_on_balanced_vertex
 551#print axioms jCost_equivariant
 552#print axioms path_middle_balanced_ends_not
 553#print axioms blockSum_point
 554#print axioms blockSum_edge
 555#print axioms blockSum_path
 556#print axioms jCost_not_fixedKindTotals
 557#print axioms jCost_not_a_valuation
 558#print axioms cert4_annihilates_census
 559#print axioms cert4_sees_J4
 560#print axioms J4_not_in_census_span
 561#print axioms J4_not_in_census_span_with_const
 562#print axioms cert3_annihilates_counts
 563#print axioms cert3_sees_J3
 564#print axioms J3_not_in_census_span
 565#print axioms census3_det
 566#print axioms census3_with_const_is_onto
 567#print axioms j0_ne_cV_3D
 568#print axioms jEhrhartSpanVerdict
 569
 570end Gap2JEhrhartSpan
 571end SevenGaps
 572end Gravity
 573end IndisputableMonolith
 574