IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerCohomology
IndisputableMonolith/Gravity/SevenGaps/Gap2LedgerCohomology.lean · 467 lines · 53 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.Gap2LetterCostDichotomy
2
3/-!
4# Gap 2 / C18: ledger cohomology of natural local posting costs
5
6The panel's repaired form of incidence silence (C18): compute
7`H¹_natural(PostingLedger; ℝ)`, the space of relabeling-natural, local,
8path-independent additive costs on the posting ledger, modulo ledger
9coboundaries, and ask whether it equals `span{dn_V, dn_E, dn_T}`.
10
11## Verdict (MEASURED at caps 1–3, kernel-certified)
12
13It does **not**. On the incidence-local feature basis
14`(f_V, f_E_loop, f_E_proper, f_T)` the history space has dimension
15
16| cap | dim H¹ (histories) | dim span{nV,nE,nT} | incidence class |
17|----:|-------------------:|-------------------:|-----------------|
18| 1 | 3 | 3 | coboundary (no proper edges exist) |
19| 2 | 4 | 3 | **genuine class** |
20| 3 | 4 | 3 | **genuine class** |
21
22Receipt: `scripts/qg/out/ledger_cohomology_20260730.json`
23(runner `scripts/qg/qg_ledger_cohomology_20260730.py`, Bigbird 2026-07-30).
24
25The obstruction is exhibited, not asserted: `incidenceCost t` is
26gauge-equivariant, incidence-local, path-independent (its step cost at an
27edge post depends only on whether the two endpoints differ, data available
28at posting time), has history `t · properEdgeCount`, and that history is
29not a function of the three sort counts (`twoLoops` vs `twoBridges` at
30size `(2,2,0)`). It is therefore a concrete new referent in H¹ outside
31the count span. The A1.7 escape witness `kindRateCost 1 0 (-1/24)` is by
32contrast a count combination (rates `(1,0,-1/24)`), not a coboundary and
33not a new class.
34
35## What this closes, and what it does not
36
37On the ledger-generated class the numerator question for flag 8 asked
38whether every natural local path-independent cost is history-zero after
39atom normalizations. The count span alone would have forced that (A1.7 /
40`fixedKindTotals_and_atoms_force_zero_historyCost`). The obstruction
41shows the premise "natural + local + path-independent" does **not** force
42count-linearity, so it does not force history-zero. The centered fibre
43(`centeredIncidenceCost`) remains a coboundary in the history sense
44(history identically zero) and is not the obstruction. No flag moves.
45
46## Cochain complex (definitions)
47
48* **0-cochains.** Natural potentials on complexes: relabeling-invariant
49 real functions of a `BoundedComplex`.
50* **1-cochains.** Additive costs on legal single-letter posts. Realized
51 here as `LetterCost`s; the history is the path integral empty → K.
52* **Coboundary.** `dφ` has history `φ(K) - φ(∅)`. A cost is a *ledger
53 coboundary* in the C18 sense when its history vanishes identically
54 (invisible to the Boltzmann weight); `centeredIncidenceCost` lives here.
55* **Path-independence.** The path integral depends only on the final
56 complex. Automatic for every `LetterCost`; for step costs, the
57 incidence basis satisfies the diamond cocycle by inspection (each
58 feature is a finished-complex letter count).
59* **Locality / naturality.** A letter's cost depends only on
60 relabeling-invariant local incidence data of that letter. The
61 incidence basis is the spanning set measured above.
62
63Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
64-/
65
66namespace IndisputableMonolith
67namespace Gravity
68namespace SevenGaps
69namespace Gap2LedgerCohomology
70
71open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume Gap2GluingDerivation
72open GaugeHistoryMeasure Gap2SizeBlindnessReach Gap2PostingCostDerivation
73open Gap2LetterCostDichotomy
74
75noncomputable section
76
77variable {B : ℕ}
78
79/-! ## §1. The cochain complex -/
80
81/-- A **natural potential**: a relabeling-invariant real function of a complex. -/
82def NaturalPotential : Type :=
83 { φ : ∀ (B : ℕ), BoundedComplex B → ℝ //
84 ∀ (B : ℕ) (K K' : BoundedComplex B), Equivalent K K' → φ B K = φ B K' }
85
86/-- The **coboundary** of a natural potential, as a letter cost that charges
87the whole complex's potential change onto no particular letter: its history
88is `φ(K) - φ(∅)`. Used only to name the comparison; the C18 quotient is by
89history-zero costs below. -/
90def historyOfPotential (φ : NaturalPotential) (B : ℕ) (K : BoundedComplex B) : ℝ :=
91 φ.1 B K - φ.1 B (emptyComplex B)
92
93/-- **Ledger coboundary** (C18): a letter cost whose history vanishes at every
94complex. These are invisible to `postedWeight` and form the subspace the
95panel called the centered-incidence fibre. -/
96def IsLedgerCoboundary (c : LetterCost) : Prop :=
97 ∀ (B : ℕ) (K : BoundedComplex B), historyCost c B K = 0
98
99/-- **Count-linear**: the history is a fixed linear combination of the three
100sort counts. Equivalent to `FixedKindTotals`. -/
101def IsCountLinear (c : LetterCost) : Prop := FixedKindTotals c
102
103/-- The three **count differentials**: charge one unit per letter of the
104named kind. These are `dn_V`, `dn_E`, `dn_T` as letter costs. -/
105def dnV : LetterCost := kindRateCost 1 0 0
106def dnE : LetterCost := kindRateCost 0 1 0
107def dnT : LetterCost := kindRateCost 0 0 1
108
109theorem dnV_kindRates : KindRates dnV 1 0 0 := kindRateCost_kindRates 1 0 0
110theorem dnE_kindRates : KindRates dnE 0 1 0 := kindRateCost_kindRates 0 1 0
111theorem dnT_kindRates : KindRates dnT 0 0 1 := kindRateCost_kindRates 0 0 1
112
113theorem dnV_countLinear : IsCountLinear dnV := kindRateCost_fixedKindTotals 1 0 0
114theorem dnE_countLinear : IsCountLinear dnE := kindRateCost_fixedKindTotals 0 1 0
115theorem dnT_countLinear : IsCountLinear dnT := kindRateCost_fixedKindTotals 0 0 1
116
117theorem dnV_equivariant : Equivariant dnV := kindRateCost_equivariant 1 0 0
118theorem dnE_equivariant : Equivariant dnE := kindRateCost_equivariant 0 1 0
119theorem dnT_equivariant : Equivariant dnT := kindRateCost_equivariant 0 0 1
120
121/-- **History of a count differential.** -/
122theorem historyCost_dnV (B : ℕ) (K : BoundedComplex B) :
123 historyCost dnV B K = (K.nV : ℝ) := by
124 simpa using historyCost_of_kindRates dnV_kindRates B K
125
126theorem historyCost_dnE (B : ℕ) (K : BoundedComplex B) :
127 historyCost dnE B K = (K.nE : ℝ) := by
128 simpa using historyCost_of_kindRates dnE_kindRates B K
129
130theorem historyCost_dnT (B : ℕ) (K : BoundedComplex B) :
131 historyCost dnT B K = (K.nT : ℝ) := by
132 simpa using historyCost_of_kindRates dnT_kindRates B K
133
134/-! ## §2. Incidence locality -/
135
136/-- **Incidence locality**: there exist reals `cV`, `cLoop`, `cProper`, `cT`
137such that every edge letter is charged exactly by the loop/proper dichotomy,
138and vertex/tet letters are charged by fixed kind rates. This is the feature
139basis measured in the C18 enumeration. -/
140def IncidenceLocal (c : LetterCost) (cV cLoop cProper cT : ℝ) : Prop :=
141 (∀ (B : ℕ) (K : BoundedComplex B) (v : Fin K.nV), c B K (Sum.inl v) = cV)
142 ∧ (∀ (B : ℕ) (K : BoundedComplex B) (e : Fin K.nE),
143 c B K (Sum.inr (Sum.inl e))
144 = if (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 then cProper else cLoop)
145 ∧ (∀ (B : ℕ) (K : BoundedComplex B) (τ : Fin K.nT),
146 c B K (Sum.inr (Sum.inr τ)) = cT)
147
148/-- The cost with the four incidence-local rates. -/
149def incidenceLocalCost (cV cLoop cProper cT : ℝ) : LetterCost := fun _ K a =>
150 match a with
151 | Sum.inl _ => cV
152 | Sum.inr (Sum.inl e) =>
153 if (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 then cProper else cLoop
154 | Sum.inr (Sum.inr _) => cT
155
156theorem incidenceLocalCost_is (cV cLoop cProper cT : ℝ) :
157 IncidenceLocal (incidenceLocalCost cV cLoop cProper cT) cV cLoop cProper cT := by
158 refine ⟨fun _ _ _ => rfl, ?_, fun _ _ _ => rfl⟩
159 intro B K e
160 rfl
161
162/-- **History of an incidence-local cost**, in loop/proper form. -/
163theorem historyCost_incidenceLocal (cV cLoop cProper cT : ℝ)
164 (B : ℕ) (K : BoundedComplex B) :
165 historyCost (incidenceLocalCost cV cLoop cProper cT) B K
166 = cV * (K.nV : ℝ)
167 + cLoop * (K.nE : ℝ)
168 + (cProper - cLoop) * (properEdgeCount K : ℝ)
169 + cT * (K.nT : ℝ) := by
170 classical
171 unfold historyCost
172 rw [Fintype.sum_sum_type, Fintype.sum_sum_type]
173 have hV : ∑ v : Fin K.nV, incidenceLocalCost cV cLoop cProper cT B K (Sum.inl v)
174 = cV * (K.nV : ℝ) := by
175 simp only [incidenceLocalCost, Finset.sum_const, Finset.card_univ, Fintype.card_fin,
176 nsmul_eq_mul]
177 ring
178 have hT : ∑ τ : Fin K.nT, incidenceLocalCost cV cLoop cProper cT B K (Sum.inr (Sum.inr τ))
179 = cT * (K.nT : ℝ) := by
180 simp only [incidenceLocalCost, Finset.sum_const, Finset.card_univ, Fintype.card_fin,
181 nsmul_eq_mul]
182 ring
183 have hE :
184 (∑ e : Fin K.nE, incidenceLocalCost cV cLoop cProper cT B K (Sum.inr (Sum.inl e)))
185 = cLoop * (K.nE : ℝ) + (cProper - cLoop) * (properEdgeCount K : ℝ) := by
186 have hterm : ∀ e : Fin K.nE,
187 incidenceLocalCost cV cLoop cProper cT B K (Sum.inr (Sum.inl e))
188 = cLoop + (if (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 then cProper - cLoop else 0) := by
189 intro e
190 simp only [incidenceLocalCost]
191 split_ifs <;> ring
192 rw [Finset.sum_congr rfl (fun e _ => hterm e), Finset.sum_add_distrib,
193 Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
194 have hP : (∑ e : Fin K.nE,
195 if (K.edgeVerts e).1 ≠ (K.edgeVerts e).2 then cProper - cLoop else (0 : ℝ))
196 = (cProper - cLoop) * (properEdgeCount K : ℝ) := by
197 rw [← Finset.sum_filter, Finset.sum_const, nsmul_eq_mul]
198 unfold properEdgeCount
199 ring
200 rw [hP]
201 ring
202 rw [hV, hE, hT]
203 ring
204
205/-- Count-linear costs are incidence-local with `cLoop = cProper`. -/
206theorem kindRateCost_incidenceLocal (cV cE cT : ℝ) :
207 IncidenceLocal (kindRateCost cV cE cT) cV cE cE cT := by
208 refine ⟨fun _ _ _ => rfl, fun _ _ _ => by split_ifs <;> rfl, fun _ _ _ => rfl⟩
209
210/-- `incidenceCost t` is incidence-local with rates `(0, 0, t, 0)`. -/
211theorem incidenceCost_incidenceLocal (t : ℝ) :
212 IncidenceLocal (incidenceCost t) 0 0 t 0 :=
213 ⟨fun _ _ _ => rfl, fun _ _ _ => rfl, fun _ _ _ => rfl⟩
214
215/-- Equivariance of an incidence-local cost. -/
216theorem incidenceLocalCost_equivariant (cV cLoop cProper cT : ℝ) :
217 Equivariant (incidenceLocalCost cV cLoop cProper cT) := by
218 intro B K K' r a
219 rcases a with x | (y | z)
220 · rfl
221 · rw [show postingAlphEquiv r.vEquiv r.eEquiv r.tEquiv (Sum.inr (Sum.inl y))
222 = Sum.inr (Sum.inl (r.eEquiv y)) from rfl]
223 simp only [incidenceLocalCost]
224 exact if_congr (not_congr (loop_iff_of_relabel r y).symm) rfl rfl
225 · rfl
226
227/-! ## §3. Cap-1 collapse: H¹ equals the count span when proper edges cannot exist -/
228
229/-- **MEASURED / kernel-certified at cap 1.** On every complex with `nV ≤ 1`,
230an incidence-local history reduces to a count-linear combination, because
231`properEdgeCount = 0` and therefore `n_loop = nE`. -/
232theorem incidenceLocal_history_countLinear_of_nV_le_one
233 (cV cLoop cProper cT : ℝ) (B : ℕ) (K : BoundedComplex B) (h : K.nV ≤ 1) :
234 historyCost (incidenceLocalCost cV cLoop cProper cT) B K
235 = cV * (K.nV : ℝ) + cLoop * (K.nE : ℝ) + cT * (K.nT : ℝ) := by
236 rw [historyCost_incidenceLocal, properEdgeCount_eq_zero_of_nV_le_one K h]
237 ring
238
239/-- At `nV ≤ 1` the proper-edge feature is history-invisible: charging proper
240edges anything is a ledger coboundary relative to charging them nothing. -/
241theorem properFeature_invisible_at_nV_le_one (t : ℝ) (B : ℕ)
242 (K : BoundedComplex B) (h : K.nV ≤ 1) :
243 historyCost (incidenceCost t) B K = 0 := by
244 rw [historyCost_incidenceCost, properEdgeCount_eq_zero_of_nV_le_one K h]
245 simp
246
247/-! ## §4. The obstruction: incidence is a genuine H¹ class -/
248
249/-- **Not a ledger coboundary.** At `twoBridges`, `incidenceCost 1` has history 2. -/
250theorem incidenceCost_not_coboundary :
251 ¬ IsLedgerCoboundary (incidenceCost (1 : ℝ)) := by
252 intro h
253 have h2 := h 2 twoBridges
254 rw [historyCost_incidenceCost, properEdgeCount_twoBridges] at h2
255 norm_num at h2
256
257/-- **Not count-linear.** `twoLoops` and `twoBridges` share the count triple
258`(2,2,0)` but carry histories `0` and `2` under `incidenceCost 1`. -/
259theorem incidenceCost_history_not_a_function_of_counts :
260 twoLoops.nV = twoBridges.nV ∧ twoLoops.nE = twoBridges.nE ∧ twoLoops.nT = twoBridges.nT
261 ∧ historyCost (incidenceCost (1 : ℝ)) 2 twoLoops
262 ≠ historyCost (incidenceCost (1 : ℝ)) 2 twoBridges := by
263 refine ⟨rfl, rfl, rfl, ?_⟩
264 rw [historyCost_incidenceCost, historyCost_incidenceCost,
265 properEdgeCount_twoLoops, properEdgeCount_twoBridges]
266 norm_num
267
268theorem incidenceCost_not_countLinear :
269 ¬ IsCountLinear (incidenceCost (1 : ℝ)) := by
270 rintro ⟨cV, cE, cT, hc⟩
271 have hL := historyCost_of_kindTotalRates hc 2 twoLoops
272 have hB := historyCost_of_kindTotalRates hc 2 twoBridges
273 have hEq : historyCost (incidenceCost (1 : ℝ)) 2 twoLoops
274 = historyCost (incidenceCost (1 : ℝ)) 2 twoBridges := by
275 rw [hL, hB]; simp [twoLoops, twoBridges]
276 exact (incidenceCost_history_not_a_function_of_counts).2.2.2 hEq
277
278/-- **THEOREM (the C18 obstruction).** `incidenceCost 1` is gauge-equivariant,
279incidence-local, not a ledger coboundary, and not count-linear. It is the
280exhibited generator of H¹ outside `span{dn_V, dn_E, dn_T}`. -/
281theorem incidence_is_genuine_H1_class :
282 Equivariant (incidenceCost (1 : ℝ))
283 ∧ IncidenceLocal (incidenceCost (1 : ℝ)) 0 0 1 0
284 ∧ ¬ IsLedgerCoboundary (incidenceCost (1 : ℝ))
285 ∧ ¬ IsCountLinear (incidenceCost (1 : ℝ))
286 ∧ historyCost (incidenceCost (1 : ℝ)) 2 twoLoops = 0
287 ∧ historyCost (incidenceCost (1 : ℝ)) 2 twoBridges = 2
288 ∧ twoLoops.nV = twoBridges.nV
289 ∧ twoLoops.nE = twoBridges.nE
290 ∧ twoLoops.nT = twoBridges.nT := by
291 refine ⟨incidenceCost_equivariant 1, incidenceCost_incidenceLocal 1,
292 incidenceCost_not_coboundary, incidenceCost_not_countLinear, ?_, ?_, rfl, rfl, rfl⟩
293 · rw [historyCost_incidenceCost, properEdgeCount_twoLoops]; norm_num
294 · rw [historyCost_incidenceCost, properEdgeCount_twoBridges]; norm_num
295
296/-! ## §5. The A1.7 escape is a count combination -/
297
298/-- **Classification of A1.7's escape witness.** `kindRateCost 1 0 (-1/24)` is
299count-linear with rates `(1, 0, -1/24)`, gauge-equivariant, and not a ledger
300coboundary (its history at the vertex atom is 1). It is not a new H¹ class. -/
301theorem a17_escape_history_at_dust :
302 historyCost (kindRateCost 1 0 (-(1 / 24))) 1 (dust 1) = 1 :=
303 historyCost_kindRateCost_dust_one 1 0 (-(1 / 24))
304
305theorem a17_escape_not_coboundary :
306 ¬ IsLedgerCoboundary (kindRateCost 1 0 (-(1 / 24))) := by
307 intro h
308 have h1 := h 1 (dust 1)
309 rw [a17_escape_history_at_dust] at h1
310 exact (by norm_num : (1 : ℝ) ≠ 0) h1
311
312theorem a17_escape_is_count_combination :
313 IsCountLinear (kindRateCost 1 0 (-(1 / 24)))
314 ∧ Equivariant (kindRateCost 1 0 (-(1 / 24)))
315 ∧ ¬ IsLedgerCoboundary (kindRateCost 1 0 (-(1 / 24)))
316 ∧ historyCost (kindRateCost 1 0 (-(1 / 24))) 1 (dust 1) = 1
317 ∧ KindRates (kindRateCost 1 0 (-(1 / 24))) 1 0 (-(1 / 24)) :=
318 ⟨kindRateCost_fixedKindTotals 1 0 (-(1 / 24)),
319 kindRateCost_equivariant 1 0 (-(1 / 24)),
320 a17_escape_not_coboundary,
321 a17_escape_history_at_dust,
322 kindRateCost_kindRates 1 0 (-(1 / 24))⟩
323
324/-- The same witness's census history is the measured A1.7 polynomial
325`4N³ + 6N² + 4N + 1` (imported from the dichotomy module). -/
326theorem a17_escape_census_history (F : CensusDilateFamily) (N : ℕ) :
327 historyCost (kindRateCost 1 0 (-(1 / 24))) (F.cap N) (F.K N)
328 = 4 * (N : ℝ) ^ 3 + 6 * (N : ℝ) ^ 2 + 4 * (N : ℝ) + 1 :=
329 (purity_of_the_surface_term_is_load_bearing F).2.2.2 N
330
331/-! ## §6. The count span is three-dimensional -/
332
333/-- The three count histories are independent as class functions: there is no
334nontrivial rate triple giving history zero at the three atoms
335`dust 1` (1,0,0), `bouquet 1 0` (1,1,0), `bouquet 0 1` (1,0,1). -/
336theorem count_span_rank_three :
337 ∀ cV cE cT : ℝ,
338 historyCost (kindRateCost cV cE cT) 1 (dust 1) = 0 →
339 historyCost (kindRateCost cV cE cT) 2 (bouquet 1 0) = 0 →
340 historyCost (kindRateCost cV cE cT) 2 (bouquet 0 1) = 0 →
341 cV = 0 ∧ cE = 0 ∧ cT = 0 := by
342 intro cV cE cT hV hE hT
343 rw [historyCost_of_kindRates (kindRateCost_kindRates cV cE cT)] at hV hE hT
344 simp only [dust_nV, dust_nE, dust_nT, bouquet_nV, bouquet_nE, bouquet_nT,
345 Nat.cast_one, Nat.cast_zero, mul_one, mul_zero, add_zero] at hV hE hT
346 exact ⟨hV, by linarith, by linarith⟩
347
348/-- **Linear independence of the three count differentials.** No nontrivial
349linear combination is a ledger coboundary. -/
350theorem count_differentials_independent {cV cE cT : ℝ}
351 (h : IsLedgerCoboundary (kindRateCost cV cE cT)) :
352 cV = 0 ∧ cE = 0 ∧ cT = 0 :=
353 count_span_rank_three cV cE cT (h 1 (dust 1)) (h 2 (bouquet 1 0)) (h 2 (bouquet 0 1))
354
355/-! ## §7. Measured dimensions (cap-restricted, kernel-mirrored) -/
356
357/-- Cap-by-cap H¹ dimensions from the Bigbird enumeration
358(`scripts/qg/out/ledger_cohomology_20260730.json`). Scoped as MEASURED data
359mirrored into the kernel; the obstruction theorems of §4 are the
360kernel-certified content. -/
361def measuredH1Dim : ℕ → ℕ
362 | 1 => 3
363 | 2 => 4
364 | 3 => 4
365 | _ => 0
366
367def measuredCountSpanDim : ℕ → ℕ
368 | 1 => 3
369 | 2 => 3
370 | 3 => 3
371 | _ => 0
372
373theorem measured_H1_cap1 : measuredH1Dim 1 = 3 := rfl
374theorem measured_H1_cap2 : measuredH1Dim 2 = 4 := rfl
375theorem measured_H1_cap3 : measuredH1Dim 3 = 4 := rfl
376theorem measured_count_cap1 : measuredCountSpanDim 1 = 3 := rfl
377theorem measured_count_cap2 : measuredCountSpanDim 2 = 3 := rfl
378theorem measured_count_cap3 : measuredCountSpanDim 3 = 3 := rfl
379
380theorem measured_H1_exceeds_count_at_cap2 :
381 measuredCountSpanDim 2 < measuredH1Dim 2 := by decide
382
383theorem measured_H1_exceeds_count_at_cap3 :
384 measuredCountSpanDim 3 < measuredH1Dim 3 := by decide
385
386theorem measured_H1_equals_count_at_cap1 :
387 measuredH1Dim 1 = measuredCountSpanDim 1 := rfl
388
389/-! ## §8. Centered incidence is a ledger coboundary (not the obstruction) -/
390
391theorem centeredIncidence_is_coboundary (t : ℝ) :
392 IsLedgerCoboundary (centeredIncidenceCost t) :=
393 fun B K => historyCost_centeredIncidenceCost t B K
394
395/-! ## §9. Verdict package -/
396
397/-- **C18 verdict.** The target equality
398`H¹_natural = span{dn_V, dn_E, dn_T}` fails on the incidence-local class:
399the obstruction `incidenceCost 1` is exhibited. The A1.7 escape is a count
400combination. Cap 1 collapses to the count span because proper edges cannot
401exist. Flag unmoved. -/
402structure LedgerCohomologyVerdict where
403 obstruction : Equivariant (incidenceCost (1 : ℝ))
404 ∧ ¬ IsLedgerCoboundary (incidenceCost (1 : ℝ))
405 ∧ ¬ IsCountLinear (incidenceCost (1 : ℝ))
406 a17_escape_count : IsCountLinear (kindRateCost 1 0 (-(1 / 24)))
407 ∧ ¬ IsLedgerCoboundary (kindRateCost 1 0 (-(1 / 24)))
408 count_span_rank : ∀ cV cE cT : ℝ,
409 historyCost (kindRateCost cV cE cT) 1 (dust 1) = 0 →
410 historyCost (kindRateCost cV cE cT) 2 (bouquet 1 0) = 0 →
411 historyCost (kindRateCost cV cE cT) 2 (bouquet 0 1) = 0 →
412 cV = 0 ∧ cE = 0 ∧ cT = 0
413 cap1_collapse : ∀ (cV cLoop cProper cT : ℝ) (B : ℕ) (K : BoundedComplex B),
414 K.nV ≤ 1 →
415 historyCost (incidenceLocalCost cV cLoop cProper cT) B K
416 = cV * (K.nV : ℝ) + cLoop * (K.nE : ℝ) + cT * (K.nT : ℝ)
417 measured_dims : measuredH1Dim 1 = 3 ∧ measuredH1Dim 2 = 4 ∧ measuredH1Dim 3 = 4
418 ∧ measuredCountSpanDim 2 = 3 ∧ measuredCountSpanDim 2 < measuredH1Dim 2
419 centered_is_coboundary : ∀ t : ℝ, IsLedgerCoboundary (centeredIncidenceCost t)
420 measure_flag_moved : Bool := false
421
422def ledgerCohomologyVerdict : LedgerCohomologyVerdict where
423 obstruction := ⟨(incidence_is_genuine_H1_class).1,
424 (incidence_is_genuine_H1_class).2.2.1,
425 (incidence_is_genuine_H1_class).2.2.2.1⟩
426 a17_escape_count := ⟨(a17_escape_is_count_combination).1,
427 (a17_escape_is_count_combination).2.2.1⟩
428 count_span_rank := count_span_rank_three
429 cap1_collapse := fun cV cLoop cProper cT B K h =>
430 incidenceLocal_history_countLinear_of_nV_le_one cV cLoop cProper cT B K h
431 measured_dims := ⟨rfl, rfl, rfl, rfl, measured_H1_exceeds_count_at_cap2⟩
432 centered_is_coboundary := centeredIncidence_is_coboundary
433 measure_flag_moved := false
434
435theorem index_flag_unmoved : ledgerCohomologyVerdict.measure_flag_moved = false := rfl
436
437end
438
439/-! ## Axiom audit -/
440
441#print axioms historyCost_dnV
442#print axioms historyCost_dnE
443#print axioms historyCost_dnT
444#print axioms historyCost_incidenceLocal
445#print axioms incidenceLocalCost_equivariant
446#print axioms incidenceCost_incidenceLocal
447#print axioms incidenceLocal_history_countLinear_of_nV_le_one
448#print axioms properFeature_invisible_at_nV_le_one
449#print axioms incidenceCost_not_coboundary
450#print axioms incidenceCost_history_not_a_function_of_counts
451#print axioms incidenceCost_not_countLinear
452#print axioms incidence_is_genuine_H1_class
453#print axioms a17_escape_history_at_dust
454#print axioms a17_escape_not_coboundary
455#print axioms a17_escape_is_count_combination
456#print axioms a17_escape_census_history
457#print axioms count_differentials_independent
458#print axioms count_span_rank_three
459#print axioms centeredIncidence_is_coboundary
460#print axioms measured_H1_exceeds_count_at_cap2
461#print axioms ledgerCohomologyVerdict
462
463end Gap2LedgerCohomology
464end SevenGaps
465end Gravity
466end IndisputableMonolith
467