IndisputableMonolith.Gravity.SevenGaps.Gap2OrientedFaceSpan

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpan
   2
   3/-!
   4# Gap 2 / C12: the oriented-face imbalance referent, and the census span test
   5
   6`Gap2JEhrhartSpan` (lane A1.5) read the net ledger imbalance off **vertices** and
   7killed that route: the resulting recognition cost is gauge equivariant, is the sum
   8over its letters, and has bulk cancellation, but its measured moment vector lies
   9outside the span of the census in four dimensions.  That verdict was scoped to the
  10vertex referent and said nothing about a cost built from a different one.
  11
  12This module builds the different one.
  13
  14## §1.  The referent, and why it is not a relabelling of the old one
  15
  16The vertex reading used a single structural fact: `BoundedComplex.edgeVerts` is an
  17**ordered** pair, so an edge is one directed posting, debiting its head and
  18crediting its tail, and a vertex's ledger state is its pair of degrees.
  19
  20`BoundedComplex.tetVerts` is an **ordered** tuple too, `Fin K.nT → Fin 4 → Fin K.nV`.
  21The same reading one chain degree up says a top cell is one directed posting over
  22its own codimension-one facets, debiting the even-indexed ones and crediting the
  23odd-indexed ones.  That is the simplicial boundary with its alternating signs, and
  24the incidence sign of the `i`-th facet is `(-1)^i` (`facetSign`).  A facet is a
  25triangle, carried here as an ordered triple of vertices, and `orientSign` compares
  26two ordered triples: it returns `1` when they agree up to an even permutation, `-1`
  27up to an odd one, and `0` otherwise.  The net imbalance of an oriented face is then
  28
  29    faceImbalance K f  =  sum over top cells tau and facet slots i of
  30                            (-1)^i * orientSign (facetTriple K tau i) f
  31
  32and its recognition cost is that imbalance squared over twice the Casimir, which is
  33`ChartFromLedgerMomentum.Jlog_eq_imbalance_sq_div_two_casimir` evaluated at the face's
  34own ledger state.
  35
  36**Genuinely different, not a relabelling.**  The vertex referent is the boundary of
  37the complex's *edge* data read at vertices; this is the boundary of its *top-cell*
  38data read at faces.  Different block of the incidence structure, different chain
  39degree, different arithmetic: the vertex imbalance of a Freudenthal region ranges over
  40the whole interval from `-15` to `15` in four dimensions (MEASURED), while the face
  41imbalance takes only the values `-2, -1, 0, 1, 2` under the raw chain ordering and only
  42`-1, 0, 1` under the oriented convention used here (both MEASURED).  The consequence matters.  A1.5's kill turned
  43on the fact that a squared imbalance is not a linear function of counts; a face
  44imbalance that is `0` or one of `1, -1` has an idempotent square, so the face-read `J` is a
  45plain *count* of unbalanced faces and does **not** inherit that obstruction.  It fails
  46for a different reason, given in §3.
  47
  48**Orientation signed** (`faceImbalance_reverse`): reversing a face negates its
  49imbalance, unconditionally, because `revFace` is an involution that exchanges the
  50three even comparisons of `orientSign` with the three odd ones.  A degenerate triple,
  51one with a repeated vertex, is annihilated for the same reason, so it is charged
  52nothing without anyone stipulating that it should be.
  53
  54## §2.  The cost, additivity, bulk cancellation
  55
  56Faces are not letters: the posting alphabet has three blocks and none of them is the
  57face block.  So the charge is attributed to the top-cell letter that posts it,
  58`facetImbalanceSq K tau` being the sum of the four squared facet imbalances of `tau`
  59(`jFaceCost`).  **The attribution is invisible to the span test.**  A facet interior
  60to a region is a facet of two top cells whose incidences cancel, so it carries zero
  61imbalance and contributes nothing wherever it is booked; a boundary facet belongs to
  62exactly one top cell, so there is nothing to distribute.  The aggregate the census test
  63reads is therefore the same under any attribution, which closes the obvious escape
  64that the route was killed by a bookkeeping choice.
  65
  66Three properties are recorded, the same three A1.5 needed.  `jFaceCost` is a
  67`LetterCost`, its history cost is the top-cell block sum (`historyCost_jFaceCost`), it
  68is gauge equivariant (`jFaceCost_equivariant`), and a top cell all of whose facets
  69balance is charged nothing (`jFaceCost_vanishes_on_balanced_tet`).  The last clause is
  70not vacuous: `twoTets` glues two top cells along one facet ordered so their incidences
  71oppose, and on that complex the shared facet really is balanced while the six others
  72really are not (`twoTets_shared_facet_balanced_others_not`).
  73
  74## §3.  The verdict
  75
  76`jFaceCost` has no fixed kind totals either (`jFaceCost_not_fixedKindTotals`), and the
  77witness says exactly what the cost is: one top cell has four unbalanced facets and
  78costs `2/kappa`, two glued along a facet have six and cost `3/kappa`, so the top-cell
  79block total is a boundary count and not a fixed multiple of the top-cell count.  This
  80is a different failure from A1.5's.  There the block sum was a sum of unbounded
  81squares; here it is a count, and counts are perfectly linear objects.  What defeats it
  82is that the thing being counted is a *surface*.
  83
  84§4 carries the measured moments.  On the four-dimensional Freudenthal cube dilate the
  85oriented-face cost is exactly `48 N^3`, a pure surface term, and A1.5's obstruction
  86functional `cert4 = (0, 1, -2, 2, 0)` returns `48` on it.  The certificate is the same
  87one, which is not a coincidence and is made precise by the sharpest theorem here:
  88
  89* `census4_with_const_span_iff` computes the census span exactly.  A moment vector
  90  lies in the span of the three counts plus a constant **if and only if**
  91  `cert4` annihilates it.  The span is a hyperplane, and the certificate is its normal.
  92* `no_pure_surface_term_in_census_span` is the corollary that matters: for every
  93  nonzero `a`, the moment vector `(0, a, 0, 0, 0)` is outside the span.  **No pure
  94  surface term of the four-dimensional Kuhn cube dilate is a per-kind charge**, whatever
  95  imbalance referent produced it.
  96
  97That subsumes this route's kill through the corollary (its moment is a pure surface
  98term), and A1.5's kill through the iff (its moment is not: the certificate returns 192
  99on it).  It is not a closure of every bulk-cancelling referent: bulk cancellation
 100constrains the interior only, and one whose higher-strata moments satisfy
 101`a - 2b + 2c = 0` lies in the span by the iff, so the tension with census
 102representability holds at the pure-surface stratum rather than universally.  Both parity
 103constituents of the oblique-dihedral family are checked separately with their own
 104certificates, and the two variant readings measured alongside the primary one (the raw
 105ordered-tuple convention, and the circulation of postings around 2-simplices) fail as
 106well.
 107
 108## Scope
 109
 110The verdict is about the recognition cost built from oriented-face imbalance on the
 111Freudenthal carrier, over the cube and oblique-dihedral families, on both parity
 112constituents, at the dilate ranges enumerated (`N` to 23 in three dimensions, 17 in
 113four), plus the period-doubled cell verified identical to the cube at side `2N`.  It
 114closes the oriented-face referent.  It does not flip any flag: no triple was derived,
 115so nothing was compared to unit fugacity, and `gap2_measure_derived` stays as it was.
 116
 117Numbers marked MEASURED come from `scripts/qg/qg_oriented_face_span_20260730.py`, exact
 118integer and rational arithmetic, quasi-polynomial fits verified against held-out
 119dilates.  The vertex-read totals of A1.5 were recomputed by that script as a
 120known-answer check on the instrument and reproduce A1.5's published moments exactly.
 121
 122Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
 123-/
 124
 125namespace IndisputableMonolith
 126namespace Gravity
 127namespace SevenGaps
 128namespace Gap2OrientedFaceSpan
 129
 130open PathSumMeasure GaugeHistoryMeasure Gap2PostingCostDerivation Gap2JEhrhartSpan
 131
 132variable {B : ℕ}
 133
 134/-! ## §1. Oriented faces and their signed incidence with an ordered top cell -/
 135
 136/-- An **oriented face**: a triangle presented as an ordered triple of vertices.  The
 137orientation is the vertex order up to an even permutation, which is what `orientSign`
 138below reads. -/
 139abbrev OFace (n : ℕ) : Type := Fin n × Fin n × Fin n
 140
 141/-- Cyclic rotation of an oriented face.  An even permutation, so it preserves
 142orientation. -/
 143def rotFace {n : ℕ} (f : OFace n) : OFace n := (f.2.1, f.2.2, f.1)
 144
 145/-- Reversal of an oriented face, here the transposition of its first two vertices.
 146An odd permutation, so it reverses orientation. -/
 147def revFace {n : ℕ} (f : OFace n) : OFace n := (f.2.1, f.1, f.2.2)
 148
 149theorem revFace_involutive {n : ℕ} (f : OFace n) : revFace (revFace f) = f := rfl
 150
 151theorem revFace_eq_iff {n : ℕ} (f t : OFace n) : revFace f = t ↔ f = revFace t := by
 152  constructor
 153  · intro h; rw [← h, revFace_involutive]
 154  · intro h; rw [h, revFace_involutive]
 155
 156theorem revFace_inj {n : ℕ} {f t : OFace n} : revFace f = revFace t ↔ f = t := by
 157  rw [revFace_eq_iff, revFace_involutive]
 158
 159/-- Indicator of a decidable proposition, valued in the integers. -/
 160def ind (p : Prop) [Decidable p] : ℤ := if p then 1 else 0
 161
 162/-- Logically equivalent propositions have equal indicators.  Stated as an equation
 163between integers rather than rewritten under the `if`, because the decidability instance
 164travels with the proposition and rewriting the proposition alone leaves a motive that is
 165not type correct. -/
 166theorem ind_congr {p q : Prop} [Decidable p] [Decidable q] (h : p ↔ q) : ind p = ind q := by
 167  by_cases hp : p
 168  · have hq : q := h.mp hp
 169    simp [ind, hp, hq]
 170  · have hq : ¬ q := fun hq => hp (h.mpr hq)
 171    simp [ind, hp, hq]
 172
 173/-- **The signed incidence of two ordered triples.**  `orientSign t f` is `1` when `f`
 174is an even permutation of `t`, `-1` when it is an odd one, and `0` otherwise.  Written
 175as a signed sum of six indicators rather than a case split, because in that form the
 176orientation law `orientSign_rev` is a pairing of the six terms and needs no
 177nondegeneracy hypothesis: a triple with a repeated vertex has its even and odd classes
 178coincide, so the six terms cancel and it is annihilated. -/
 179def orientSign {n : ℕ} (t f : OFace n) : ℤ :=
 180  ind (f = t) + ind (f = rotFace t) + ind (f = rotFace (rotFace t))
 181    - ind (f = revFace t) - ind (f = revFace (rotFace t))
 182    - ind (f = revFace (rotFace (rotFace t)))
 183
 184/-- **Orientation signed, at the incidence.**  Reversing the face flips every
 185incidence sign. -/
 186theorem orientSign_rev {n : ℕ} (t f : OFace n) :
 187    orientSign t (revFace f) = - orientSign t f := by
 188  unfold orientSign
 189  rw [ind_congr (revFace_eq_iff f t),
 190    ind_congr (revFace_eq_iff f (rotFace t)),
 191    ind_congr (revFace_eq_iff f (rotFace (rotFace t))),
 192    ind_congr (revFace_inj (f := f) (t := t)),
 193    ind_congr (revFace_inj (f := f) (t := rotFace t)),
 194    ind_congr (revFace_inj (f := f) (t := rotFace (rotFace t)))]
 195  ring
 196
 197/-! ### Facets of an ordered top cell -/
 198
 199/-- The `i`-th facet of an ordered top cell: drop the `i`-th vertex and keep the other
 200three in their order.  Nothing is stipulated; `BoundedComplex.tetVerts` already orders
 201them. -/
 202def facetTriple (K : BoundedComplex B) (τ : Fin K.nT) (i : Fin 4) : OFace K.nV :=
 203  if i = 0 then (K.tetVerts τ 1, K.tetVerts τ 2, K.tetVerts τ 3)
 204  else if i = 1 then (K.tetVerts τ 0, K.tetVerts τ 2, K.tetVerts τ 3)
 205  else if i = 2 then (K.tetVerts τ 0, K.tetVerts τ 1, K.tetVerts τ 3)
 206  else (K.tetVerts τ 0, K.tetVerts τ 1, K.tetVerts τ 2)
 207
 208/-- The incidence sign of the `i`-th facet, `(-1)^i`: a top cell debits its
 209even-indexed facets and credits its odd-indexed ones. -/
 210def facetSign (i : Fin 4) : ℤ := if i = 0 ∨ i = 2 then 1 else -1
 211
 212/-- **The net recognition imbalance of an oriented face in context.**  Debits minus
 213credits over every top cell of the complex, read off the carrier's own ordered
 214top-cell incidence. -/
 215def faceImbalance (K : BoundedComplex B) (f : OFace K.nV) : ℤ :=
 216  ∑ τ : Fin K.nT, ∑ i : Fin 4, facetSign i * orientSign (facetTriple K τ i) f
 217
 218/-- **Orientation signed, at the face.**  A face and its reverse carry opposite
 219imbalance, in every complex, with no hypothesis on the complex. -/
 220theorem faceImbalance_reverse (K : BoundedComplex B) (f : OFace K.nV) :
 221    faceImbalance K (revFace f) = - faceImbalance K f := by
 222  unfold faceImbalance
 223  rw [← Finset.sum_neg_distrib]
 224  refine Finset.sum_congr rfl ?_
 225  intro τ _
 226  rw [← Finset.sum_neg_distrib]
 227  refine Finset.sum_congr rfl ?_
 228  intro i _
 229  rw [orientSign_rev]
 230  ring
 231
 232/-! ## §2. The derived letter cost -/
 233
 234/-- The integer part of a top cell's charge: the sum of the squared imbalances of its
 235four facets. -/
 236def facetImbalanceSq (K : BoundedComplex B) (τ : Fin K.nT) : ℤ :=
 237  ∑ i : Fin 4, (faceImbalance K (facetTriple K τ i)) ^ 2
 238
 239/-- The integer part of the whole complex's charge. -/
 240def imbalanceSqTotal (K : BoundedComplex B) : ℤ :=
 241  ∑ τ : Fin K.nT, facetImbalanceSq K τ
 242
 243noncomputable section
 244
 245/-- **The recognition cost of a letter in context, oriented-face reading.**  A top-cell
 246letter is charged the squared imbalance of each of the faces it posts, over twice the
 247Casimir.  Vertex and edge letters are not face-posting sources, so they are charged
 248nothing.
 249
 250The attribution to the top-cell block is bookkeeping and the aggregate does not depend
 251on it: an interior facet has two opposing incidences, so its imbalance vanishes and it
 252contributes nothing wherever it is booked, and a boundary facet belongs to one top cell
 253only. -/
 254def jFaceCost (kappa : ℝ) : LetterCost := fun _ K a =>
 255  match a with
 256  | Sum.inr (Sum.inr τ) => ((facetImbalanceSq K τ : ℝ)) / (2 * kappa)
 257  | _ => 0
 258
 259@[simp] theorem jFaceCost_inl (kappa : ℝ) (B : ℕ) (K : BoundedComplex B) (v : Fin K.nV) :
 260    jFaceCost kappa B K (Sum.inl v) = 0 := rfl
 261
 262@[simp] theorem jFaceCost_edge (kappa : ℝ) (B : ℕ) (K : BoundedComplex B) (e : Fin K.nE) :
 263    jFaceCost kappa B K (Sum.inr (Sum.inl e)) = 0 := rfl
 264
 265@[simp] theorem jFaceCost_tet (kappa : ℝ) (B : ℕ) (K : BoundedComplex B) (τ : Fin K.nT) :
 266    jFaceCost kappa B K (Sum.inr (Sum.inr τ))
 267      = ((facetImbalanceSq K τ : ℝ)) / (2 * kappa) := rfl
 268
 269/-- **`J` is the sum over its letters.**  The history cost is the top-cell block sum,
 270because the other two blocks are silent. -/
 271theorem historyCost_jFaceCost (kappa : ℝ) (B : ℕ) (K : BoundedComplex B) :
 272    historyCost (jFaceCost kappa) B K
 273      = ∑ τ : Fin K.nT, jFaceCost kappa B K (Sum.inr (Sum.inr τ)) := by
 274  classical
 275  unfold historyCost
 276  rw [Fintype.sum_sum_type, Fintype.sum_sum_type]
 277  simp
 278
 279/-- The history cost in closed form: the complex's integer charge over twice the
 280Casimir. -/
 281theorem historyCost_jFaceCost_eq (kappa : ℝ) (B : ℕ) (K : BoundedComplex B) :
 282    historyCost (jFaceCost kappa) B K = ((imbalanceSqTotal K : ℝ)) / (2 * kappa) := by
 283  rw [historyCost_jFaceCost]
 284  simp only [jFaceCost_tet]
 285  rw [← Finset.sum_div]
 286  congr 1
 287  unfold imbalanceSqTotal
 288  push_cast
 289  rfl
 290
 291/-- **Bulk cancellation, at the letter.**  A top cell whose facets all balance is
 292charged nothing.  On a region of the Freudenthal carrier an interior facet is a facet
 293of two top cells; whether their incidences oppose is a property of the ordering the
 294carrier supplies, and §4 measures which convention has it. -/
 295theorem jFaceCost_vanishes_on_balanced_tet (kappa : ℝ) (B : ℕ) (K : BoundedComplex B)
 296    (τ : Fin K.nT) (h : ∀ i : Fin 4, faceImbalance K (facetTriple K τ i) = 0) :
 297    jFaceCost kappa B K (Sum.inr (Sum.inr τ)) = 0 := by
 298  have hz : facetImbalanceSq K τ = 0 := by
 299    unfold facetImbalanceSq
 300    refine Finset.sum_eq_zero ?_
 301    intro i _
 302    rw [h i]
 303    ring
 304  rw [jFaceCost_tet, hz]
 305  simp
 306
 307end
 308
 309/-! ### Equivariance: the failure below is not a labelling artifact -/
 310
 311/-- Transport an oriented face along a vertex relabelling. -/
 312def mapTriple {m n : ℕ} (φ : Fin m ≃ Fin n) (t : OFace m) : OFace n :=
 313  (φ t.1, φ t.2.1, φ t.2.2)
 314
 315theorem mapTriple_rotFace {m n : ℕ} (φ : Fin m ≃ Fin n) (t : OFace m) :
 316    rotFace (mapTriple φ t) = mapTriple φ (rotFace t) := rfl
 317
 318theorem mapTriple_revFace {m n : ℕ} (φ : Fin m ≃ Fin n) (t : OFace m) :
 319    revFace (mapTriple φ t) = mapTriple φ (revFace t) := rfl
 320
 321theorem mapTriple_inj {m n : ℕ} (φ : Fin m ≃ Fin n) (x y : OFace m) :
 322    mapTriple φ x = mapTriple φ y ↔ x = y := by
 323  unfold mapTriple
 324  simp [Prod.ext_iff]
 325
 326theorem orientSign_map {m n : ℕ} (φ : Fin m ≃ Fin n) (t f : OFace m) :
 327    orientSign (mapTriple φ t) (mapTriple φ f) = orientSign t f := by
 328  unfold orientSign
 329  simp only [mapTriple_rotFace, mapTriple_revFace, mapTriple_inj]
 330
 331theorem facetTriple_relabel {K K' : BoundedComplex B} (r : Relabel K K')
 332    (τ : Fin K.nT) (i : Fin 4) :
 333    facetTriple K' (r.tEquiv τ) i = mapTriple r.vEquiv (facetTriple K τ i) := by
 334  unfold facetTriple mapTriple
 335  split_ifs <;> simp [r.tet_comm]
 336
 337theorem faceImbalance_relabel {K K' : BoundedComplex B} (r : Relabel K K')
 338    (f : OFace K.nV) : faceImbalance K f = faceImbalance K' (mapTriple r.vEquiv f) := by
 339  unfold faceImbalance
 340  refine Fintype.sum_equiv r.tEquiv _ _ ?_
 341  intro τ
 342  refine Finset.sum_congr rfl ?_
 343  intro i _
 344  rw [facetTriple_relabel r τ i, orientSign_map]
 345
 346theorem facetImbalanceSq_relabel {K K' : BoundedComplex B} (r : Relabel K K')
 347    (τ : Fin K.nT) : facetImbalanceSq K τ = facetImbalanceSq K' (r.tEquiv τ) := by
 348  unfold facetImbalanceSq
 349  refine Finset.sum_congr rfl ?_
 350  intro i _
 351  have h := faceImbalance_relabel r (facetTriple K τ i)
 352  rw [facetTriple_relabel r τ i, ← h]
 353
 354/-- **`jFaceCost` is gauge equivariant.**  Labels are gauge for it, so every negative
 355result below is about the cost and not about a choice of names. -/
 356theorem jFaceCost_equivariant (kappa : ℝ) : Equivariant (jFaceCost kappa) := by
 357  intro B K K' r a
 358  cases a with
 359  | inl v => rfl
 360  | inr b =>
 361      cases b with
 362      | inl e => rfl
 363      | inr τ =>
 364          show jFaceCost kappa B K' (Sum.inr (Sum.inr (r.tEquiv τ)))
 365            = jFaceCost kappa B K (Sum.inr (Sum.inr τ))
 366          rw [jFaceCost_tet, jFaceCost_tet, ← facetImbalanceSq_relabel r τ]
 367
 368/-! ## §3. The verdict at the finite complex: no aggregate-linear letter cost
 369
 370Two explicit complexes.  `oneTet` is a single ordered top cell.  `twoTets` glues two of
 371them along one facet, ordered so their incidences on the shared facet oppose. -/
 372
 373/-- One top cell on four vertices, ordered `(0, 1, 2, 3)`. -/
 374def oneTet : BoundedComplex 4 where
 375  nV := 4
 376  nE := 0
 377  nT := 1
 378  hV := by decide
 379  hE := by decide
 380  hT := by decide
 381  edgeVerts := fun e => e.elim0
 382  tetVerts := fun _ i => i
 383
 384/-- Two top cells on five vertices sharing the facet `(1, 2, 3)`.  The second is
 385ordered `(1, 4, 2, 3)`, which presents the shared facet in slot `1` and so with the
 386opposite incidence sign to the first cell's slot `0`. -/
 387def twoTets : BoundedComplex 5 where
 388  nV := 5
 389  nE := 0
 390  nT := 2
 391  hV := by decide
 392  hE := by decide
 393  hT := by decide
 394  edgeVerts := fun e => e.elim0
 395  tetVerts := fun t i => if t = 0 then ![0, 1, 2, 3] i else ![1, 4, 2, 3] i
 396
 397/-- MEASURED in the kernel: the single top cell has four unbalanced facets. -/
 398theorem facetImbalanceSq_oneTet : facetImbalanceSq oneTet (0 : Fin 1) = 4 := by decide
 399
 400theorem imbalanceSqTotal_oneTet : imbalanceSqTotal oneTet = 4 := by decide
 401
 402/-- MEASURED in the kernel: gluing two top cells along a facet leaves six unbalanced
 403facets, not eight.  The shared facet is charged nothing. -/
 404theorem imbalanceSqTotal_twoTets : imbalanceSqTotal twoTets = 6 := by decide
 405
 406/-- **Non-vacuity of the bulk-cancellation clause.**  On `twoTets` the shared facet
 407really is balanced and the neighbouring facet of the same top cell really is not, so
 408`jFaceCost_vanishes_on_balanced_tet` has an instance and a non-instance on the same
 409complex. -/
 410theorem twoTets_shared_facet_balanced_others_not :
 411    faceImbalance twoTets (facetTriple twoTets (0 : Fin 2) (0 : Fin 4)) = 0
 412      ∧ faceImbalance twoTets (facetTriple twoTets (0 : Fin 2) (1 : Fin 4)) ≠ 0
 413      ∧ faceImbalance twoTets (facetTriple twoTets (1 : Fin 2) (1 : Fin 4)) = 0 := by
 414  decide
 415
 416/-- **Non-vacuity of the orientation law.**  The imbalance really is nonzero somewhere,
 417so `faceImbalance_reverse` is not the statement that `0 = -0`. -/
 418theorem faceImbalance_reverse_nonvacuous :
 419    faceImbalance oneTet (facetTriple oneTet (0 : Fin 1) (0 : Fin 4)) = 1
 420      ∧ faceImbalance oneTet
 421          (revFace (facetTriple oneTet (0 : Fin 1) (0 : Fin 4))) = -1 := by
 422  decide
 423
 424/-- A triple with a repeated vertex is annihilated, without anyone saying it should be. -/
 425theorem orientSign_degenerate_witness :
 426    orientSign ((0, 0, 1) : OFace 4) ((0, 0, 1) : OFace 4) = 0 := by decide
 427
 428noncomputable section
 429
 430theorem blockSum_oneTet (kappa : ℝ) :
 431    (∑ τ : Fin oneTet.nT, jFaceCost kappa 4 oneTet (Sum.inr (Sum.inr τ))) = 2 / kappa := by
 432  rw [← historyCost_jFaceCost, historyCost_jFaceCost_eq, imbalanceSqTotal_oneTet]
 433  push_cast
 434  ring
 435
 436theorem blockSum_twoTets (kappa : ℝ) :
 437    (∑ τ : Fin twoTets.nT, jFaceCost kappa 5 twoTets (Sum.inr (Sum.inr τ)))
 438      = 3 / kappa := by
 439  rw [← historyCost_jFaceCost, historyCost_jFaceCost_eq, imbalanceSqTotal_twoTets]
 440  push_cast
 441  ring
 442
 443/-- **HEADLINE (the route fails at the letter, for a new reason).**  For every nonzero
 444Casimir the oriented-face cost has no fixed kind totals, so
 445`measure_from_fixedKindTotals` cannot be applied to it.
 446
 447The witness says what the object is.  A single top cell has four unbalanced facets and
 448its block sum is `2/kappa`, which forces `cT = 2/kappa`.  Two top cells glued along a
 449facet have six and their block sum is `3/kappa`, which demands `cT = 3/(2 kappa)`.  The
 450top-cell block total counts the *surface* of the complex, and a surface is not a fixed
 451multiple of a volume.
 452
 453This is a different failure from `Gap2JEhrhartSpan.jCost_not_fixedKindTotals`.  There
 454the block sum was a sum of unbounded squares and the obstruction was that a square is
 455not linear.  Here every squared imbalance in the witness is `0` or `1`, the block sum
 456is a plain count, and the obstruction is what is being counted. -/
 457theorem jFaceCost_not_fixedKindTotals (kappa : ℝ) (hk : kappa ≠ 0) :
 458    ¬ FixedKindTotals (jFaceCost kappa) := by
 459  rintro ⟨cV, cE, cT, h⟩
 460  have h1 := (h 4 oneTet).2.2
 461  have h2 := (h 5 twoTets).2.2
 462  rw [blockSum_oneTet kappa] at h1
 463  rw [blockSum_twoTets kappa] at h2
 464  have e1 : ((oneTet.nT : ℕ) : ℝ) = 1 := by
 465    show ((1 : ℕ) : ℝ) = 1
 466    norm_num
 467  have e2 : ((twoTets.nT : ℕ) : ℝ) = 2 := by
 468    show ((2 : ℕ) : ℝ) = 2
 469    norm_num
 470  rw [e1, mul_one] at h1
 471  rw [e2] at h2
 472  rw [← h1] at h2
 473  simp only [div_eq_mul_inv] at h2
 474  have hinv : (kappa : ℝ)⁻¹ = 0 := by linarith
 475  exact hk (inv_eq_zero.mp hinv)
 476
 477end
 478
 479/-! ## §4. The census span test on the measured moment vectors
 480
 481Moment vectors of the Freudenthal (Kuhn) carrier, in the basis `(N^d, ..., N, 1)`.
 482MEASURED by exact enumeration (`scripts/qg/qg_oriented_face_span_20260730.py`); every
 483quasi-polynomial fit reproduces its held-out dilates exactly, and the period-doubled
 484cell was verified identical to the cube at side `2N` on every measured quantity, in
 485three dimensions and in four.
 486
 487The census columns are A1.5's, imported rather than restated, because the carrier and
 488the census are the same and only the target changed.  `mV4`, `mE4`, `mT4`, `mC4`,
 489`dot4` and `cert4` all come from `Gap2JEhrhartSpan`. -/
 490
 491/-- MEASURED moment vector of `2 * kappa * J` for the oriented-face reading on the 4D
 492Freudenthal cube dilate, with the top cells carrying the orientation they inherit from
 493the ambient orientation of `R^4`.  It is exactly `48 N^3`: a pure surface term, which is
 494bulk cancellation in its sharpest quantitative form. -/
 495def mFor4 : Fin 5 → ℚ := ![0, 48, 0, 0, 0]
 496
 497/-- MEASURED moment vector of the same reading with the raw increasing-chain ordering
 498the carrier writes down, `eps = 1` rather than `sign(sigma)`.  Its leading coefficient
 499is nonzero, which is the measurement that the raw convention does **not** bulk-cancel:
 500interior facets carry imbalance `2` or `-2` under it. -/
 501def mForRaw4 : Fin 5 → ℚ := ![240, -48, 0, 0, 0]
 502
 503/-- MEASURED moment vector of the third reading of "oriented face": the circulation of
 504the directed postings around an oriented 2-simplex, the discrete curl of the posting
 505field.  On this carrier the circulation is `1` at every 2-simplex without exception, so
 506this reading is the 2-simplex count and carries no information about the region at all. -/
 507def mCurl4 : Fin 5 → ℚ := ![50, 48, 12, 0, 0]
 508
 509theorem cert4_sees_mFor4 : dot4 cert4 mFor4 = 48 := by
 510  simp [dot4, cert4, mFor4, Fin.sum_univ_five]
 511
 512theorem cert4_sees_mForRaw4 : dot4 cert4 mForRaw4 = -48 := by
 513  simp [dot4, cert4, mForRaw4, Fin.sum_univ_five]
 514
 515theorem cert4_sees_mCurl4 : dot4 cert4 mCurl4 = 24 := by
 516  simp [dot4, cert4, mCurl4, Fin.sum_univ_five]
 517  norm_num
 518
 519/-! ### The census span, computed exactly
 520
 521The sharpest statement in this module, and the one that explains both kills.  The
 522census columns plus a constant span exactly the hyperplane `cert4` annihilates, so
 523membership is a single linear condition and the certificate is the normal. -/
 524
 525/-- **THEOREM (the four-dimensional census span, exactly).**  A moment vector is a
 526rational combination of the three kind counts and a constant if and only if the
 527obstruction functional annihilates it.  The forward direction is A1.5's certificate; the
 528reverse direction exhibits the inverse, so this is an equality of sets and not a
 529one-sided bound. -/
 530theorem census4_with_const_span_iff (t : Fin 5 → ℚ) :
 531    (∃ a b c e : ℚ, ∀ i : Fin 5,
 532        a * mV4 i + b * mE4 i + c * mT4 i + e * mC4 i = t i)
 533      ↔ dot4 cert4 t = 0 := by
 534  constructor
 535  · rintro ⟨a, b, c, e, h⟩
 536    have h1 := h 1
 537    have h2 := h 2
 538    have h3 := h 3
 539    simp [mV4, mE4, mT4, mC4] at h1 h2 h3
 540    simp [dot4, cert4, Fin.sum_univ_five]
 541    linarith
 542  · intro h
 543    simp [dot4, cert4, Fin.sum_univ_five] at h
 544    refine ⟨3 * t 3 / 8 - t 2 / 12, t 2 / 12 - t 3 / 8,
 545      (t 0 - (3 * t 3 / 8 - t 2 / 12) - 15 * (t 2 / 12 - t 3 / 8)) / 24,
 546      t 4 - (3 * t 3 / 8 - t 2 / 12), ?_⟩
 547    intro i
 548    fin_cases i <;> simp [mV4, mE4, mT4, mC4] <;> linarith
 549
 550/-- **THEOREM (no pure surface term is a per-kind charge).**  For every nonzero `a`, the
 551moment vector `(0, a, 0, 0, 0)` of a functional that is exactly `a N^3` on the
 552four-dimensional Kuhn cube dilate lies outside the census span, with or without a
 553constant column.
 554
 555This is the general form of both kills in this line of work, and it is a prediction as
 556well as a verdict: any imbalance referent whatsoever whose recognition cost is a pure
 557surface term on this carrier will fail this test, and no rescoping of the referent
 558changes that. -/
 559theorem no_pure_surface_term_in_census_span (a : ℚ) (ha : a ≠ 0) :
 560    ¬ ∃ p q r s : ℚ, ∀ i : Fin 5,
 561      p * mV4 i + q * mE4 i + r * mT4 i + s * mC4 i
 562        = (![0, a, 0, 0, 0] : Fin 5 → ℚ) i := by
 563  intro hex
 564  have hz := (census4_with_const_span_iff _).mp hex
 565  simp [dot4, cert4, Fin.sum_univ_five] at hz
 566  exact ha hz
 567
 568/-- **HEADLINE (outside the census span, four dimensions).**  No rational triple of kind
 569rates, with or without an additive constant, reproduces the oriented-face cost's measured
 570moment vector on the 4D Freudenthal cube dilate. -/
 571theorem mFor4_not_in_census_span_with_const :
 572    ¬ ∃ a b c e : ℚ, ∀ i : Fin 5,
 573      a * mV4 i + b * mE4 i + c * mT4 i + e * mC4 i = mFor4 i := by
 574  intro hex
 575  have hz := (census4_with_const_span_iff _).mp hex
 576  rw [cert4_sees_mFor4] at hz
 577  norm_num at hz
 578
 579theorem mFor4_not_in_census_span :
 580    ¬ ∃ a b c : ℚ, ∀ i : Fin 5, a * mV4 i + b * mE4 i + c * mT4 i = mFor4 i := by
 581  rintro ⟨a, b, c, h⟩
 582  exact mFor4_not_in_census_span_with_const ⟨a, b, c, 0, by
 583    intro i; rw [← h i]; simp [mC4]⟩
 584
 585/-- The raw ordered-tuple convention fails too, and by the same functional. -/
 586theorem mForRaw4_not_in_census_span_with_const :
 587    ¬ ∃ a b c e : ℚ, ∀ i : Fin 5,
 588      a * mV4 i + b * mE4 i + c * mT4 i + e * mC4 i = mForRaw4 i := by
 589  intro hex
 590  have hz := (census4_with_const_span_iff _).mp hex
 591  rw [cert4_sees_mForRaw4] at hz
 592  norm_num at hz
 593
 594/-- The circulation reading fails too. -/
 595theorem mCurl4_not_in_census_span_with_const :
 596    ¬ ∃ a b c e : ℚ, ∀ i : Fin 5,
 597      a * mV4 i + b * mE4 i + c * mT4 i + e * mC4 i = mCurl4 i := by
 598  intro hex
 599  have hz := (census4_with_const_span_iff _).mp hex
 600  rw [cert4_sees_mCurl4] at hz
 601  norm_num at hz
 602
 603/-! ### The oblique-dihedral family, both parity constituents
 604
 605The cube census has a degenerate negative control (its top-cell column is a pure
 606monomial, so the leading unit vector is a census column), which is why A1.5 also
 607enumerated an oblique-dihedral region whose apex is half-integral and whose census is a
 608genuine period-2 quasi-polynomial.  Both of its parity constituents are carried here
 609with their own obstruction functionals. -/
 610
 611def oV4e : Fin 5 → ℚ := ![1/4, 3/2, 13/4, 3, 1]
 612def oE4e : Fin 5 → ℚ := ![15/4, 17/2, 31/4, 5/2, 0]
 613def oT4 : Fin 5 → ℚ := ![6, -6, 0, 0, 0]
 614
 615/-- MEASURED oriented-face moments on the 4D oblique region, even dilates. -/
 616def oFor4e : Fin 5 → ℚ := ![0, 21, -18, 0, 0]
 617
 618def ocert4e : Fin 5 → ℚ := ![121, 121, -259, 210, 0]
 619
 620def oV4o : Fin 5 → ℚ := ![1/4, 3/2, 3, 5/2, 3/4]
 621def oE4o : Fin 5 → ℚ := ![15/4, 17/2, 6, 1, -1/4]
 622
 623/-- MEASURED oriented-face moments on the 4D oblique region, odd dilates. -/
 624def oFor4o : Fin 5 → ℚ := ![0, 21, -21, 0, 0]
 625
 626def ocert4o : Fin 5 → ℚ := ![32, 32, -77, 70, 0]
 627
 628theorem ocert4e_annihilates_census :
 629    dot4 ocert4e oV4e = 0 ∧ dot4 ocert4e oE4e = 0 ∧ dot4 ocert4e oT4 = 0
 630      ∧ dot4 ocert4e mC4 = 0 := by
 631  refine ⟨?_, ?_, ?_, ?_⟩ <;>
 632    simp [dot4, ocert4e, oV4e, oE4e, oT4, mC4, Fin.sum_univ_five] <;> norm_num
 633
 634theorem ocert4e_sees_oFor4e : dot4 ocert4e oFor4e = 7203 := by
 635  simp [dot4, ocert4e, oFor4e, Fin.sum_univ_five]
 636  norm_num
 637
 638theorem ocert4o_annihilates_census :
 639    dot4 ocert4o oV4o = 0 ∧ dot4 ocert4o oE4o = 0 ∧ dot4 ocert4o oT4 = 0
 640      ∧ dot4 ocert4o mC4 = 0 := by
 641  refine ⟨?_, ?_, ?_, ?_⟩ <;>
 642    simp [dot4, ocert4o, oV4o, oE4o, oT4, mC4, Fin.sum_univ_five] <;> norm_num
 643
 644theorem ocert4o_sees_oFor4o : dot4 ocert4o oFor4o = 2289 := by
 645  simp [dot4, ocert4o, oFor4o, Fin.sum_univ_five]
 646  norm_num
 647
 648/-- **Outside the span on the oblique region, even dilates.** -/
 649theorem oFor4e_not_in_census_span_with_const :
 650    ¬ ∃ a b c e : ℚ, ∀ i : Fin 5,
 651      a * oV4e i + b * oE4e i + c * oT4 i + e * mC4 i = oFor4e i := by
 652  rintro ⟨a, b, c, e, h⟩
 653  have h0 := h 0
 654  have h1 := h 1
 655  have h2 := h 2
 656  have h3 := h 3
 657  simp [oV4e, oE4e, oT4, mC4, oFor4e] at h0 h1 h2 h3
 658  linarith
 659
 660/-- **Outside the span on the oblique region, odd dilates.** -/
 661theorem oFor4o_not_in_census_span_with_const :
 662    ¬ ∃ a b c e : ℚ, ∀ i : Fin 5,
 663      a * oV4o i + b * oE4o i + c * oT4 i + e * mC4 i = oFor4o i := by
 664  rintro ⟨a, b, c, e, h⟩
 665  have h0 := h 0
 666  have h1 := h 1
 667  have h2 := h 2
 668  have h3 := h 3
 669  simp [oV4o, oE4o, oT4, mC4, oFor4o] at h0 h1 h2 h3
 670  linarith
 671
 672/-! ### Three dimensions, where the test with a constant column is vacuous
 673
 674`Gap2JEhrhartSpan.census3_with_const_is_onto` already proved the 3D system with a
 675constant column returns a triple for any input whatever, so only the three-count system
 676discriminates there.  The oriented-face moments are `12 N^2` on the 3D cube dilate. -/
 677
 678/-- MEASURED oriented-face moments on the 3D Freudenthal cube dilate. -/
 679def mFor3 : Fin 4 → ℚ := ![0, 12, 0, 0]
 680
 681theorem cert3_sees_mFor3 : dot3 cert3 mFor3 = 12 := by
 682  simp [dot3, cert3, mFor3, Fin.sum_univ_four]
 683
 684theorem mFor3_not_in_census_span :
 685    ¬ ∃ a b c : ℚ, ∀ i : Fin 4, a * mV3 i + b * mE3 i + c * mT3 i = mFor3 i := by
 686  rintro ⟨a, b, c, h⟩
 687  have h1 := h 1
 688  have h2 := h 2
 689  have h3 := h 3
 690  simp [mV3, mE3, mT3, mFor3] at h1 h2 h3
 691  linarith
 692
 693/-! ## §5. Certificate -/
 694
 695/-- **The C12 oriented-face verdict.**  The oriented-face imbalance is a signed referent
 696read off the carrier's own ordered top-cell incidence; the cost built from it is a gauge
 697equivariant letter cost whose history is the sum over its letters and whose bulk cancels;
 698it has no fixed kind totals; and its measured moment vector lies outside the census span
 699in four dimensions on both region families and both parity constituents.  The census span
 700is computed exactly, so the kill is a hyperplane condition rather than a failed search,
 701and the corollary closes every pure surface term at once. -/
 702structure OrientedFaceSpanVerdict : Prop where
 703  orientation_signed : ∀ (B : ℕ) (K : BoundedComplex B) (f : OFace K.nV),
 704    faceImbalance K (revFace f) = - faceImbalance K f
 705  equivariant : ∀ kappa : ℝ, Equivariant (jFaceCost kappa)
 706  sum_over_letters : ∀ (kappa : ℝ) (B : ℕ) (K : BoundedComplex B),
 707    historyCost (jFaceCost kappa) B K
 708      = ∑ τ : Fin K.nT, jFaceCost kappa B K (Sum.inr (Sum.inr τ))
 709  bulk_cancels : ∀ (kappa : ℝ) (B : ℕ) (K : BoundedComplex B) (τ : Fin K.nT),
 710    (∀ i : Fin 4, faceImbalance K (facetTriple K τ i) = 0) →
 711      jFaceCost kappa B K (Sum.inr (Sum.inr τ)) = 0
 712  bulk_cancellation_nonvacuous :
 713    faceImbalance twoTets (facetTriple twoTets (0 : Fin 2) (0 : Fin 4)) = 0
 714      ∧ faceImbalance twoTets (facetTriple twoTets (0 : Fin 2) (1 : Fin 4)) ≠ 0
 715      ∧ faceImbalance twoTets (facetTriple twoTets (1 : Fin 2) (1 : Fin 4)) = 0
 716  no_kind_totals : ∀ kappa : ℝ, kappa ≠ 0 → ¬ FixedKindTotals (jFaceCost kappa)
 717  span_is_a_hyperplane : ∀ t : Fin 5 → ℚ,
 718    (∃ a b c e : ℚ, ∀ i : Fin 5,
 719        a * mV4 i + b * mE4 i + c * mT4 i + e * mC4 i = t i)
 720      ↔ dot4 cert4 t = 0
 721  no_surface_term : ∀ a : ℚ, a ≠ 0 →
 722    ¬ ∃ p q r s : ℚ, ∀ i : Fin 5,
 723      p * mV4 i + q * mE4 i + r * mT4 i + s * mC4 i
 724        = (![0, a, 0, 0, 0] : Fin 5 → ℚ) i
 725  outside_span_4d_cube :
 726    ¬ ∃ a b c : ℚ, ∀ i : Fin 5, a * mV4 i + b * mE4 i + c * mT4 i = mFor4 i
 727  outside_span_4d_cube_with_const :
 728    ¬ ∃ a b c e : ℚ, ∀ i : Fin 5,
 729      a * mV4 i + b * mE4 i + c * mT4 i + e * mC4 i = mFor4 i
 730  outside_span_4d_oblique_even :
 731    ¬ ∃ a b c e : ℚ, ∀ i : Fin 5,
 732      a * oV4e i + b * oE4e i + c * oT4 i + e * mC4 i = oFor4e i
 733  outside_span_4d_oblique_odd :
 734    ¬ ∃ a b c e : ℚ, ∀ i : Fin 5,
 735      a * oV4o i + b * oE4o i + c * oT4 i + e * mC4 i = oFor4o i
 736  outside_span_3d :
 737    ¬ ∃ a b c : ℚ, ∀ i : Fin 4, a * mV3 i + b * mE3 i + c * mT3 i = mFor3 i
 738  raw_convention_also_outside :
 739    ¬ ∃ a b c e : ℚ, ∀ i : Fin 5,
 740      a * mV4 i + b * mE4 i + c * mT4 i + e * mC4 i = mForRaw4 i
 741  circulation_reading_also_outside :
 742    ¬ ∃ a b c e : ℚ, ∀ i : Fin 5,
 743      a * mV4 i + b * mE4 i + c * mT4 i + e * mC4 i = mCurl4 i
 744
 745theorem orientedFaceSpanVerdict : OrientedFaceSpanVerdict where
 746  orientation_signed := fun _ K f => faceImbalance_reverse K f
 747  equivariant := jFaceCost_equivariant
 748  sum_over_letters := historyCost_jFaceCost
 749  bulk_cancels := jFaceCost_vanishes_on_balanced_tet
 750  bulk_cancellation_nonvacuous := twoTets_shared_facet_balanced_others_not
 751  no_kind_totals := jFaceCost_not_fixedKindTotals
 752  span_is_a_hyperplane := census4_with_const_span_iff
 753  no_surface_term := no_pure_surface_term_in_census_span
 754  outside_span_4d_cube := mFor4_not_in_census_span
 755  outside_span_4d_cube_with_const := mFor4_not_in_census_span_with_const
 756  outside_span_4d_oblique_even := oFor4e_not_in_census_span_with_const
 757  outside_span_4d_oblique_odd := oFor4o_not_in_census_span_with_const
 758  outside_span_3d := mFor3_not_in_census_span
 759  raw_convention_also_outside := mForRaw4_not_in_census_span_with_const
 760  circulation_reading_also_outside := mCurl4_not_in_census_span_with_const
 761
 762/-! ## §6. Flag status
 763
 764Nothing moves.  The condition for reporting a triple of chemical potentials was a
 765consistent system; the system is inconsistent on the discriminating family, so no triple
 766exists and there is nothing to compare against unit fugacity.  Flag
 767`gap2_measure_derived` stays exactly as it was. -/
 768
 769structure OrientedFaceIndex : Type where
 770  /-- The referent is signed, derived from the carrier's ordered top-cell incidence, and
 771  is not the vertex referent of `Gap2JEhrhartSpan`. -/
 772  referent_is_new : Bool
 773  /-- The cost is a gauge-equivariant letter cost summing over its letters. -/
 774  cost_is_wellformed : Bool
 775  /-- Bulk cancellation holds at the letter and the clause has a witness and a
 776  non-witness on one complex. -/
 777  bulk_cancels : Bool
 778  /-- The square is idempotent on this referent, so A1.5's non-linearity obstruction is
 779  NOT inherited.  The failure below has a different cause. -/
 780  inherits_a15_quadratic_obstruction : Bool
 781  /-- The moment vector is outside the census span in four dimensions, on both region
 782  families and both parity constituents. -/
 783  outside_span_4d : Bool
 784  /-- The census span is computed exactly as a hyperplane, so no pure surface term of
 785  this carrier can ever be a per-kind charge. -/
 786  span_computed_exactly : Bool
 787  /-- NOT produced: a triple of chemical potentials.  The system is inconsistent, so no
 788  comparison to unit fugacity was made and none was possible. -/
 789  triple_derived : Bool
 790  /-- NOT moved. -/
 791  measure_flag_moved : Bool
 792
 793def orientedFaceIndex : OrientedFaceIndex where
 794  referent_is_new := true
 795  cost_is_wellformed := true
 796  bulk_cancels := true
 797  inherits_a15_quadratic_obstruction := false
 798  outside_span_4d := true
 799  span_computed_exactly := true
 800  triple_derived := false
 801  measure_flag_moved := false
 802
 803theorem index_no_triple : orientedFaceIndex.triple_derived = false := rfl
 804
 805theorem index_flag_unmoved : orientedFaceIndex.measure_flag_moved = false := rfl
 806
 807theorem index_not_the_a15_obstruction :
 808    orientedFaceIndex.inherits_a15_quadratic_obstruction = false := rfl
 809
 810/-! ## Axiom audit -/
 811
 812#print axioms orientSign_rev
 813#print axioms faceImbalance_reverse
 814#print axioms faceImbalance_reverse_nonvacuous
 815#print axioms orientSign_degenerate_witness
 816#print axioms historyCost_jFaceCost
 817#print axioms historyCost_jFaceCost_eq
 818#print axioms jFaceCost_vanishes_on_balanced_tet
 819#print axioms orientSign_map
 820#print axioms facetTriple_relabel
 821#print axioms faceImbalance_relabel
 822#print axioms facetImbalanceSq_relabel
 823#print axioms jFaceCost_equivariant
 824#print axioms facetImbalanceSq_oneTet
 825#print axioms imbalanceSqTotal_oneTet
 826#print axioms imbalanceSqTotal_twoTets
 827#print axioms twoTets_shared_facet_balanced_others_not
 828#print axioms blockSum_oneTet
 829#print axioms blockSum_twoTets
 830#print axioms jFaceCost_not_fixedKindTotals
 831#print axioms cert4_sees_mFor4
 832#print axioms cert4_sees_mForRaw4
 833#print axioms cert4_sees_mCurl4
 834#print axioms census4_with_const_span_iff
 835#print axioms no_pure_surface_term_in_census_span
 836#print axioms mFor4_not_in_census_span
 837#print axioms mFor4_not_in_census_span_with_const
 838#print axioms mForRaw4_not_in_census_span_with_const
 839#print axioms mCurl4_not_in_census_span_with_const
 840#print axioms ocert4e_annihilates_census
 841#print axioms ocert4e_sees_oFor4e
 842#print axioms ocert4o_annihilates_census
 843#print axioms ocert4o_sees_oFor4o
 844#print axioms oFor4e_not_in_census_span_with_const
 845#print axioms oFor4o_not_in_census_span_with_const
 846#print axioms cert3_sees_mFor3
 847#print axioms mFor3_not_in_census_span
 848#print axioms orientedFaceSpanVerdict
 849
 850end Gap2OrientedFaceSpan
 851end SevenGaps
 852end Gravity
 853end IndisputableMonolith
 854