IndisputableMonolith.Gravity.SevenGaps.Gap2JDiamondRank
IndisputableMonolith/Gravity/SevenGaps/Gap2JDiamondRank.lean · 1164 lines · 117 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpan
2
3/-!
4# Gap 2 / C15: the J-diamond rank lattice
5
6`Gap2JEhrhartSpan` killed the census-inversion route to the three per-kind rates:
7the recognition cost `J` built from vertex-level ledger imbalance has no fixed
8kind totals, is not a valuation, and its moment vector lies outside the census
9span. This module runs the successor test that A15 named and did not build: the
10rank and consistency test on **J-diamonds**, the four-term inclusion-exclusion
11defect of `J` on overlapping regions.
12
13## §1. What a J-diamond is
14
15A **subcomplex** of a posting graph is a subset of its edges together with a
16vertex subset closed under their endpoints. A **J-diamond** on `K` is an
17unordered pair of proper subcomplexes whose union is `K`; it is the stand-off
18between two accumulation orders of the same complex: evaluate `J` directly on
19`K`, or evaluate it on the two sides and subtract the interface (the
20inclusion-exclusion order). The **diamond defect** is the four-term difference
21
22 D(A, B; I) = SJ(A) + SJ(B) - SJ(I) - SJ(K),
23
24where `SJ = 2 * kappa * J` is the integer squared-imbalance total. A valuation
25has `D = 0` on every diamond; `J` is not a valuation (A15), so defects are
26nonzero in general. The A15 witness, two edges glued along one vertex with
27defect `1 / kappa`, is the smallest nonzero diamond (`seed_diamond_defect`,
28`diamond_J_seed`).
29
30## §2. The defect is the interface imbalance coupling (the localization theorem)
31
32The main theorem, `diamondDefect_eq_neg_two_inner`: for an edge-partition of `K`
33into two subcomplexes, the defect factors through the two imbalance fields as
34
35 D = -2 * sum over interface vertices v of m_A(v) * m_B(v).
36
37Two consequences. Gluing along an empty interface is always exact
38(`diamondDefect_eq_zero_of_inter_empty`), so disjoint union never fails
39inclusion-exclusion. And a diamond whose interface carries no two-sided
40imbalance cannot fail (`diamondDefect_eq_zero_of_interface_balanced`): the
41gluing asymmetry of `J` accrues only where the ledger imbalance lives. The
42panel's Euler-gauge lemma says the boundary strata are the only unexcluded
43domicile for asymmetry; this is an independent, finite proof of the same
44localization content for posting-graph diamonds, not a re-proof of the Pachner
45statement. A parity consequence of the same algebra: `SJ(K)` is always even
46(`imbalanceSq_even`), matching the measured defect spectrum, which is supported
47on even integers.
48
49## §5-§6. The relation lattice and its rank
50
51Each accumulation order of each complex at the smallest caps gives one row
52`a . C = b` on the scaled rate triple `C = 2 * kappa * (c_V, c_E, c_T)`: `a` is
53the count vector of the complex produced (identical for the two orders of a
54diamond, since counts are valuations) and `b` is the measured accumulated cost.
55The rows were enumerated exactly at caps 1 to 4
56(`scripts/qg/qg_j_diamond_rank_20260730.py`, receipt
57`scripts/qg/out/j_diamond_rank_20260730.json`; MEASURED). The kernel checks the
58decisive finite facts:
59
60* the left-hand rank is exactly 2 (`lattice_lhs_rank_two`): every measured row
61 has zero `c_T` coefficient, because `J` charges top-cell letters nothing
62 (`jCost_tet`), so the tet rate direction is structurally invisible to every
63 J-relation;
64* the augmented rank is 3 (`seed_augmented_independent`), so the right-hand
65 sides carry information the left-hand side cannot: the system is
66 **inconsistent**, and the four seed rows already show it
67 (`lattice_inconsistent_seed`: the two orders of the A15 diamond demand
68 `3 C_V + 2 C_E = 2` and `= 4` at once);
69* the conflict precedes any gluing: the count vector `(2, 1, 0)` is carried by
70 two complexes with different costs (`jCost_not_a_function_of_counts`), so `J`
71 is not a function of the three counts at all.
72
73**Verdict (scoped).** Outcome three of the C15 charge fires: inconsistent RHS,
74so the vertex-imbalance `J` induces no additive letter cost, with the A15
75diamond as the exhibited witness. The lattice rank is 2, the augmented rank 3.
76The scope is exactly the J-relation lattice at the enumerated caps: it says
77nothing about referents other than vertex-level imbalance (C12's oriented-face
78route is untouched), and it does not claim the rates are underivable in general.
79
80## §7. Measured tallies
81
82Cap-by-cap enumeration tallies are mirrored as rational data with provenance,
83and each decisive tally is restated as a kernel-checked fact
84(`measured_rank_cap4`, `measured_bilinear_perfect`,
85`measured_no_localization_violations`). The positive control in the script (a
86genuinely additive statistic through the same machinery) returns a consistent
87system with the right solution, so the instrument discriminates.
88
89Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
90-/
91
92namespace IndisputableMonolith
93namespace Gravity
94namespace SevenGaps
95namespace Gap2JDiamondRank
96
97open PathSumMeasure GaugeHistoryMeasure Gap2PostingCostDerivation Gap2JEhrhartSpan
98
99variable {B : ℕ}
100
101/-! ## §1. Subcomplexes, the sub-imbalance, and the diamond defect -/
102
103/-- A **subcomplex** of a bounded complex: a subset of the edges together with a
104vertex subset closed under their endpoints. -/
105structure Subcomplex (K : BoundedComplex B) where
106 verts : Finset (Fin K.nV)
107 edges : Finset (Fin K.nE)
108 tail_mem : ∀ e ∈ edges, (K.edgeVerts e).1 ∈ verts
109 head_mem : ∀ e ∈ edges, (K.edgeVerts e).2 ∈ verts
110
111/-- In-postings of a vertex within an edge subset. -/
112def subIndeg (K : BoundedComplex B) (E : Finset (Fin K.nE)) (v : Fin K.nV) : ℕ :=
113 (E.filter fun e => (K.edgeVerts e).2 = v).card
114
115/-- Out-postings of a vertex within an edge subset. -/
116def subOutdeg (K : BoundedComplex B) (E : Finset (Fin K.nE)) (v : Fin K.nV) : ℕ :=
117 (E.filter fun e => (K.edgeVerts e).1 = v).card
118
119/-- The imbalance an edge subset assigns to a vertex: its own in-postings minus
120its own out-postings. Vanishes off the vertex set of any subcomplex owning the
121edges, by endpoint closure. -/
122def subImbalance (K : BoundedComplex B) (E : Finset (Fin K.nE)) (v : Fin K.nV) : ℤ :=
123 (subIndeg K E v : ℤ) - (subOutdeg K E v : ℤ)
124
125/-- The integer recognition charge of a subcomplex: the squared-imbalance total
126over its vertices. In units of `1 / (2 * kappa)` this is its `J`. -/
127def subCharge (K : BoundedComplex B) (S : Subcomplex K) : ℤ :=
128 ∑ v ∈ S.verts, (subImbalance K S.edges v) ^ 2
129
130/-- The **diamond defect** of a pair of subcomplexes: the four-term
131inclusion-exclusion defect `SJ(A) + SJ(B) - SJ(I) - SJ(K)`, where the interface
132charge is written explicitly so the definition needs no disjointness. -/
133def diamondDefect (K : BoundedComplex B) (A Bd : Subcomplex K) : ℤ :=
134 subCharge K A + subCharge K Bd
135 - (∑ v ∈ A.verts ∩ Bd.verts, (subImbalance K (A.edges ∩ Bd.edges) v) ^ 2)
136 - imbalanceSq K
137
138theorem subImbalance_eq_zero_of_not_mem (K : BoundedComplex B) (S : Subcomplex K)
139 {v : Fin K.nV} (hv : v ∉ S.verts) :
140 subImbalance K S.edges v = 0 := by
141 classical
142 have h1 : ∀ e ∈ S.edges, (K.edgeVerts e).2 ≠ v := by
143 intro e he hh
144 exact hv (hh ▸ S.head_mem e he)
145 have h2 : ∀ e ∈ S.edges, (K.edgeVerts e).1 ≠ v := by
146 intro e he hh
147 exact hv (hh ▸ S.tail_mem e he)
148 unfold subImbalance subIndeg subOutdeg
149 rw [Finset.filter_eq_empty_iff.mpr h1, Finset.filter_eq_empty_iff.mpr h2]
150 simp
151
152/-- **Edge-partition additivity.** Splitting the edge set splits the imbalance
153at every vertex: each posting lands on exactly one side. -/
154theorem subImbalance_union (K : BoundedComplex B) {A Bd : Finset (Fin K.nE)}
155 (h : Disjoint A Bd) (v : Fin K.nV) :
156 subImbalance K (A ∪ Bd) v = subImbalance K A v + subImbalance K Bd v := by
157 classical
158 unfold subImbalance subIndeg subOutdeg
159 rw [Finset.filter_union, Finset.filter_union,
160 Finset.card_union_of_disjoint
161 (Disjoint.mono (Finset.filter_subset _ _) (Finset.filter_subset _ _) h),
162 Finset.card_union_of_disjoint
163 (Disjoint.mono (Finset.filter_subset _ _) (Finset.filter_subset _ _) h)]
164 push_cast
165 ring
166
167/-! ## §2. The localization theorem: the defect is the interface imbalance coupling -/
168
169/-- **THEOREM (the diamond defect is the interface imbalance coupling).** For an
170edge-partition of `K` into two subcomplexes, the four-term defect equals minus
171twice the inner product of the two imbalance fields, summed over the interface.
172In particular the defect is supported where both sides carry imbalance. -/
173theorem diamondDefect_eq_neg_two_inner (K : BoundedComplex B) (A Bd : Subcomplex K)
174 (he : A.edges ∪ Bd.edges = Finset.univ) (hd : Disjoint A.edges Bd.edges) :
175 diamondDefect K A Bd
176 = -2 * ∑ v ∈ A.verts ∩ Bd.verts,
177 subImbalance K A.edges v * subImbalance K Bd.edges v := by
178 classical
179 have hI : A.edges ∩ Bd.edges = ∅ := Finset.disjoint_iff_inter_eq_empty.mp hd
180 have key : ∀ v : Fin K.nV, vertexImbalance K v
181 = subImbalance K A.edges v + subImbalance K Bd.edges v := by
182 intro v
183 have hu : subImbalance K Finset.univ v
184 = subImbalance K A.edges v + subImbalance K Bd.edges v := by
185 rw [← he]
186 exact subImbalance_union K hd v
187 exact hu
188 have hsK : imbalanceSq K
189 = ∑ v : Fin K.nV, (subImbalance K A.edges v + subImbalance K Bd.edges v) ^ 2 := by
190 show (∑ v : Fin K.nV, (vertexImbalance K v) ^ 2) = _
191 exact Finset.sum_congr rfl (fun v _ => by rw [key v])
192 have supp : ∀ (S : Subcomplex K),
193 (∑ v : Fin K.nV, (subImbalance K S.edges v) ^ 2) = subCharge K S := by
194 intro S
195 show (∑ v : Fin K.nV, (subImbalance K S.edges v) ^ 2)
196 = ∑ v ∈ S.verts, (subImbalance K S.edges v) ^ 2
197 exact (Finset.sum_subset (Finset.subset_univ S.verts) (fun x _ hx => by
198 rw [subImbalance_eq_zero_of_not_mem K S hx]
199 norm_num)).symm
200 have prodsupp :
201 (∑ v : Fin K.nV, subImbalance K A.edges v * subImbalance K Bd.edges v)
202 = ∑ v ∈ A.verts ∩ Bd.verts,
203 subImbalance K A.edges v * subImbalance K Bd.edges v := by
204 symm
205 apply Finset.sum_subset (Finset.subset_univ _)
206 intro x _ hx
207 rw [Finset.mem_inter, not_and] at hx
208 by_cases hA : x ∈ A.verts
209 · have hB : x ∉ Bd.verts := hx hA
210 rw [subImbalance_eq_zero_of_not_mem K Bd hB, mul_zero]
211 · rw [subImbalance_eq_zero_of_not_mem K A hA, zero_mul]
212 have hIz : (∑ v ∈ A.verts ∩ Bd.verts,
213 (subImbalance K (∅ : Finset (Fin K.nE)) v) ^ 2) = 0 := by
214 apply Finset.sum_eq_zero
215 intro v _
216 have hz : subImbalance K (∅ : Finset (Fin K.nE)) v = 0 := by
217 simp [subImbalance, subIndeg, subOutdeg]
218 rw [hz]
219 norm_num
220 have mid : (∑ v : Fin K.nV, 2 * subImbalance K A.edges v * subImbalance K Bd.edges v)
221 = 2 * (∑ v : Fin K.nV, subImbalance K A.edges v * subImbalance K Bd.edges v) := by
222 rw [Finset.mul_sum]
223 exact Finset.sum_congr rfl (fun v _ => mul_assoc _ _ _)
224 have expand : (∑ v : Fin K.nV, (subImbalance K A.edges v + subImbalance K Bd.edges v) ^ 2)
225 = (∑ v : Fin K.nV, (subImbalance K A.edges v) ^ 2)
226 + (∑ v : Fin K.nV, (subImbalance K Bd.edges v) ^ 2)
227 + 2 * (∑ v : Fin K.nV, subImbalance K A.edges v * subImbalance K Bd.edges v) := by
228 rw [Finset.sum_congr rfl (fun v _ => add_sq _ _)]
229 simp only [Finset.sum_add_distrib]
230 rw [mid]
231 ring
232 unfold diamondDefect
233 rw [hI, hIz, sub_zero, hsK, ← supp A, ← supp Bd, expand, prodsupp]
234 ring
235
236/-- **Empty interface, exact gluing.** A disjoint union never fails
237inclusion-exclusion: there is no shared vertex for the two imbalance fields to
238meet at. -/
239theorem diamondDefect_eq_zero_of_inter_empty (K : BoundedComplex B) (A Bd : Subcomplex K)
240 (he : A.edges ∪ Bd.edges = Finset.univ) (hd : Disjoint A.edges Bd.edges)
241 (hi : A.verts ∩ Bd.verts = ∅) :
242 diamondDefect K A Bd = 0 := by
243 rw [diamondDefect_eq_neg_two_inner K A Bd he hd, hi, Finset.sum_empty, mul_zero]
244
245/-- **The localization, Euler-gauge form.** A diamond whose interface carries no
246two-sided imbalance cannot fail. The gluing asymmetry of `J` accrues only where
247the ledger imbalance lives: the boundary strata are the only domicile for the
248defect, which is the localization content of the panel's Euler-gauge lemma,
249proved here independently and finitely for posting-graph diamonds. -/
250theorem diamondDefect_eq_zero_of_interface_balanced (K : BoundedComplex B)
251 (A Bd : Subcomplex K)
252 (he : A.edges ∪ Bd.edges = Finset.univ) (hd : Disjoint A.edges Bd.edges)
253 (hb : ∀ v ∈ A.verts ∩ Bd.verts,
254 subImbalance K A.edges v = 0 ∨ subImbalance K Bd.edges v = 0) :
255 diamondDefect K A Bd = 0 := by
256 rw [diamondDefect_eq_neg_two_inner K A Bd he hd]
257 rw [Finset.sum_eq_zero (fun v hv => by
258 obtain h | h := hb v hv
259 · rw [h, zero_mul]
260 · rw [h, mul_zero])]
261 ring
262
263/-! ## §3. The spectrum is even
264
265Every edge contributes one debit and one credit, so the imbalances sum to zero,
266and a sum of squares of integers summing to zero is even. The measured defect
267spectrum at caps 2 to 4 is supported on even integers, exactly as this forces. -/
268
269/-- **The imbalance fields sum to zero.** Each posting debits one vertex and
270credits one, so the totals cancel vertex by vertex summed over all vertices. -/
271theorem sum_vertexImbalance (K : BoundedComplex B) :
272 (∑ v : Fin K.nV, vertexImbalance K v) = 0 := by
273 classical
274 have headsum : ∀ e : Fin K.nE,
275 (∑ v : Fin K.nV, (if (K.edgeVerts e).2 = v then (1 : ℤ) else 0)) = 1 := by
276 intro e
277 rw [Finset.sum_ite_eq Finset.univ (K.edgeVerts e).2 (fun _ => (1 : ℤ))]
278 simp
279 have tailsum : ∀ e : Fin K.nE,
280 (∑ v : Fin K.nV, (if (K.edgeVerts e).1 = v then (1 : ℤ) else 0)) = 1 := by
281 intro e
282 rw [Finset.sum_ite_eq Finset.univ (K.edgeVerts e).1 (fun _ => (1 : ℤ))]
283 simp
284 have h2 : (∑ v : Fin K.nV, ((Finset.univ.filter fun e => (K.edgeVerts e).2 = v).card : ℤ))
285 = (K.nE : ℤ) := by
286 simp only [Finset.card_filter]
287 push_cast
288 rw [Finset.sum_comm]
289 rw [Finset.sum_congr rfl (fun e _ => headsum e)]
290 simp
291 have h1 : (∑ v : Fin K.nV, ((Finset.univ.filter fun e => (K.edgeVerts e).1 = v).card : ℤ))
292 = (K.nE : ℤ) := by
293 simp only [Finset.card_filter]
294 push_cast
295 rw [Finset.sum_comm]
296 rw [Finset.sum_congr rfl (fun e _ => tailsum e)]
297 simp
298 unfold vertexImbalance indeg outdeg
299 rw [Finset.sum_sub_distrib, h2, h1, sub_self]
300
301/-- **THEOREM (the charge spectrum is even).** `SJ(K)` is divisible by two for
302every bounded complex, matching the measured defect histograms, whose support is
303entirely even. -/
304theorem imbalanceSq_even (K : BoundedComplex B) : 2 ∣ imbalanceSq K := by
305 have hsum := sum_vertexImbalance K
306 have h : (∑ v : Fin K.nV, (vertexImbalance K v) ^ 2)
307 = (∑ v : Fin K.nV, (vertexImbalance K v) ^ 2)
308 - (∑ v : Fin K.nV, vertexImbalance K v) := by rw [hsum, sub_zero]
309 have hsq : imbalanceSq K
310 = ∑ v : Fin K.nV, (vertexImbalance K v * (vertexImbalance K v - 1)) := by
311 show (∑ v : Fin K.nV, (vertexImbalance K v) ^ 2) = _
312 rw [h, ← Finset.sum_sub_distrib]
313 exact Finset.sum_congr rfl (fun v _ => by ring)
314 rw [hsq]
315 apply Finset.dvd_sum
316 intro v _
317 rcases Int.even_or_odd (vertexImbalance K v) with h | h
318 · obtain ⟨k, hk⟩ := h
319 exact ⟨k * (k + k - 1), by rw [hk]; ring⟩
320 · obtain ⟨k, hk⟩ := h
321 exact ⟨(2 * k + 1) * k, by rw [hk]; ring⟩
322
323/-! ## §4. The explicit witnesses at cap 4
324
325The A15 complexes (`pointComplex`, `edgeComplex`, `pathComplex`, `twoEdgeComplex`)
326plus four more: the two-edge out-fork, the three-edge path, the three-edge
327out-star, and the loop with an isolated vertex (the second carrier of the count
328vector `(2, 1, 0)`). -/
329
330/-- A two-edge out-fork `1 <- 0 -> 2`. -/
331def forkComplex : BoundedComplex 4 where
332 nV := 3
333 nE := 2
334 nT := 0
335 hV := by decide
336 hE := by decide
337 hT := by decide
338 edgeVerts := fun e => if e = 0 then (0, 1) else (0, 2)
339 tetVerts := fun t => t.elim0
340
341/-- A three-edge path `0 -> 1 -> 2 -> 3`. -/
342def threePathComplex : BoundedComplex 4 where
343 nV := 4
344 nE := 3
345 nT := 0
346 hV := by decide
347 hE := by decide
348 hT := by decide
349 edgeVerts := fun e => if e = 0 then (0, 1) else if e = 1 then (1, 2) else (2, 3)
350 tetVerts := fun t => t.elim0
351
352/-- A three-edge out-star `0 -> 1`, `0 -> 2`, `0 -> 3`. -/
353def outStarComplex : BoundedComplex 4 where
354 nV := 4
355 nE := 3
356 nT := 0
357 hV := by decide
358 hE := by decide
359 hT := by decide
360 edgeVerts := fun e => if e = 0 then (0, 1) else if e = 1 then (0, 2) else (0, 3)
361 tetVerts := fun t => t.elim0
362
363/-- One loop at vertex `0` with one isolated vertex. Its count vector is
364`(2, 1, 0)`, the same as the proper edge, but every posting balances at its own
365vertex, so it pays nothing. -/
366def loopPointComplex : BoundedComplex 4 where
367 nV := 2
368 nE := 1
369 nT := 0
370 hV := by decide
371 hE := by decide
372 hT := by decide
373 edgeVerts := fun _ => (0, 0)
374 tetVerts := fun t => t.elim0
375
376theorem imbalance_fork_zero : vertexImbalance forkComplex (0 : Fin 3) = -2 := by decide
377
378theorem imbalance_fork_one : vertexImbalance forkComplex (1 : Fin 3) = 1 := by decide
379
380theorem imbalance_fork_two : vertexImbalance forkComplex (2 : Fin 3) = 1 := by decide
381
382theorem imbalance_threePath_zero : vertexImbalance threePathComplex (0 : Fin 4) = -1 := by decide
383
384theorem imbalance_threePath_one : vertexImbalance threePathComplex (1 : Fin 4) = 0 := by decide
385
386theorem imbalance_threePath_two : vertexImbalance threePathComplex (2 : Fin 4) = 0 := by decide
387
388theorem imbalance_threePath_three : vertexImbalance threePathComplex (3 : Fin 4) = 1 := by decide
389
390theorem imbalance_outStar_zero : vertexImbalance outStarComplex (0 : Fin 4) = -3 := by decide
391
392theorem imbalance_outStar_one : vertexImbalance outStarComplex (1 : Fin 4) = 1 := by decide
393
394theorem imbalance_outStar_two : vertexImbalance outStarComplex (2 : Fin 4) = 1 := by decide
395
396theorem imbalance_outStar_three : vertexImbalance outStarComplex (3 : Fin 4) = 1 := by decide
397
398theorem imbalance_twoEdge_zero : vertexImbalance twoEdgeComplex (0 : Fin 4) = -1 := by decide
399
400theorem imbalance_twoEdge_one : vertexImbalance twoEdgeComplex (1 : Fin 4) = 1 := by decide
401
402theorem imbalance_twoEdge_two : vertexImbalance twoEdgeComplex (2 : Fin 4) = -1 := by decide
403
404theorem imbalance_twoEdge_three : vertexImbalance twoEdgeComplex (3 : Fin 4) = 1 := by decide
405
406theorem imbalance_loopPoint_zero : vertexImbalance loopPointComplex (0 : Fin 2) = 0 := by decide
407
408theorem imbalance_loopPoint_one : vertexImbalance loopPointComplex (1 : Fin 2) = 0 := by decide
409
410theorem imbalanceSq_fork : imbalanceSq forkComplex = 6 := by decide
411
412theorem imbalanceSq_threePath : imbalanceSq threePathComplex = 2 := by decide
413
414theorem imbalanceSq_outStar : imbalanceSq outStarComplex = 12 := by decide
415
416theorem imbalanceSq_twoEdge : imbalanceSq twoEdgeComplex = 4 := by decide
417
418theorem imbalanceSq_loopPoint : imbalanceSq loopPointComplex = 0 := by decide
419
420noncomputable section
421
422/-- The history cost of `jCost` is the integer charge over twice the Casimir. -/
423theorem historyCost_jCost_eq (kappa : ℝ) (B : ℕ) (K : BoundedComplex B) :
424 historyCost (jCost kappa) B K = (imbalanceSq K : ℝ) / (2 * kappa) := by
425 rw [historyCost_jCost]
426 unfold imbalanceSq
427 push_cast
428 rw [Finset.sum_div]
429 exact Finset.sum_congr rfl (fun v _ => jCost_inl kappa B K v)
430
431theorem historyCost_edge (kappa : ℝ) (hk : kappa ≠ 0) :
432 historyCost (jCost kappa) 4 edgeComplex = 1 / kappa := by
433 rw [historyCost_jCost, blockSum_edge kappa hk]
434
435theorem historyCost_path (kappa : ℝ) (hk : kappa ≠ 0) :
436 historyCost (jCost kappa) 4 pathComplex = 1 / kappa := by
437 rw [historyCost_jCost, blockSum_path kappa hk]
438
439theorem historyCost_point (kappa : ℝ) :
440 historyCost (jCost kappa) 4 pointComplex = 0 := by
441 rw [historyCost_jCost, blockSum_point kappa]
442
443theorem imbalanceSq_emptyComplex : imbalanceSq (emptyComplex 4) = 0 := by decide
444
445theorem historyCost_empty (kappa : ℝ) :
446 historyCost (jCost kappa) 4 (emptyComplex 4) = 0 := by
447 rw [historyCost_jCost_eq, imbalanceSq_emptyComplex]
448 norm_num
449
450theorem blockSum_twoEdge (kappa : ℝ) (hk : kappa ≠ 0) :
451 (∑ v : Fin twoEdgeComplex.nV, jCost kappa 4 twoEdgeComplex (Sum.inl v)) = 2 / kappa := by
452 show (∑ v : Fin 4, jCost kappa 4 twoEdgeComplex (Sum.inl v)) = 2 / kappa
453 rw [Fin.sum_univ_four]
454 simp only [jCost_inl, imbalance_twoEdge_zero, imbalance_twoEdge_one,
455 imbalance_twoEdge_two, imbalance_twoEdge_three]
456 push_cast
457 field_simp <;> norm_num
458
459theorem historyCost_twoEdge (kappa : ℝ) (hk : kappa ≠ 0) :
460 historyCost (jCost kappa) 4 twoEdgeComplex = 2 / kappa := by
461 rw [historyCost_jCost, blockSum_twoEdge kappa hk]
462
463theorem blockSum_fork (kappa : ℝ) (hk : kappa ≠ 0) :
464 (∑ v : Fin forkComplex.nV, jCost kappa 4 forkComplex (Sum.inl v)) = 3 / kappa := by
465 show (∑ v : Fin 3, jCost kappa 4 forkComplex (Sum.inl v)) = 3 / kappa
466 rw [Fin.sum_univ_three]
467 simp only [jCost_inl, imbalance_fork_zero, imbalance_fork_one, imbalance_fork_two]
468 push_cast
469 field_simp <;> norm_num
470
471theorem historyCost_fork (kappa : ℝ) (hk : kappa ≠ 0) :
472 historyCost (jCost kappa) 4 forkComplex = 3 / kappa := by
473 rw [historyCost_jCost, blockSum_fork kappa hk]
474
475theorem blockSum_threePath (kappa : ℝ) (hk : kappa ≠ 0) :
476 (∑ v : Fin threePathComplex.nV, jCost kappa 4 threePathComplex (Sum.inl v)) = 1 / kappa := by
477 show (∑ v : Fin 4, jCost kappa 4 threePathComplex (Sum.inl v)) = 1 / kappa
478 rw [Fin.sum_univ_four]
479 simp only [jCost_inl, imbalance_threePath_zero, imbalance_threePath_one,
480 imbalance_threePath_two, imbalance_threePath_three]
481 push_cast
482 field_simp <;> norm_num
483
484theorem historyCost_threePath (kappa : ℝ) (hk : kappa ≠ 0) :
485 historyCost (jCost kappa) 4 threePathComplex = 1 / kappa := by
486 rw [historyCost_jCost, blockSum_threePath kappa hk]
487
488theorem blockSum_outStar (kappa : ℝ) (hk : kappa ≠ 0) :
489 (∑ v : Fin outStarComplex.nV, jCost kappa 4 outStarComplex (Sum.inl v)) = 6 / kappa := by
490 show (∑ v : Fin 4, jCost kappa 4 outStarComplex (Sum.inl v)) = 6 / kappa
491 rw [Fin.sum_univ_four]
492 simp only [jCost_inl, imbalance_outStar_zero, imbalance_outStar_one,
493 imbalance_outStar_two, imbalance_outStar_three]
494 push_cast
495 field_simp <;> norm_num
496
497theorem historyCost_outStar (kappa : ℝ) (hk : kappa ≠ 0) :
498 historyCost (jCost kappa) 4 outStarComplex = 6 / kappa := by
499 rw [historyCost_jCost, blockSum_outStar kappa hk]
500
501theorem historyCost_loopPoint (kappa : ℝ) :
502 historyCost (jCost kappa) 4 loopPointComplex = 0 := by
503 rw [historyCost_jCost]
504 show (∑ v : Fin 2, jCost kappa 4 loopPointComplex (Sum.inl v)) = 0
505 rw [Fin.sum_univ_two]
506 simp only [jCost_inl, imbalance_loopPoint_zero, imbalance_loopPoint_one]
507 norm_num
508
509/-- **The seed diamond, exact value.** The two orders of the A15 witness: two
510edges glued along their shared vertex against the two-edge path directly. The
511glued order accumulates `2 / kappa`, the direct order `1 / kappa`, and the defect
512is exactly `1 / kappa`. (A15 proved the two orders differ; this gives the
513value.) -/
514theorem diamond_J_seed (kappa : ℝ) (hk : kappa ≠ 0) :
515 historyCost (jCost kappa) 4 edgeComplex
516 + historyCost (jCost kappa) 4 edgeComplex
517 - historyCost (jCost kappa) 4 pointComplex
518 - historyCost (jCost kappa) 4 pathComplex = 1 / kappa := by
519 rw [historyCost_edge kappa hk, historyCost_point kappa, historyCost_path kappa hk]
520 field_simp <;> norm_num
521
522/-- **A second diamond, same sign.** The three-edge path split as its front
523two-edge path plus its last edge along the middle vertex: glued `2 / kappa`,
524direct `1 / kappa`. -/
525theorem diamond_J_threePath (kappa : ℝ) (hk : kappa ≠ 0) :
526 historyCost (jCost kappa) 4 pathComplex
527 + historyCost (jCost kappa) 4 edgeComplex
528 - historyCost (jCost kappa) 4 pointComplex
529 - historyCost (jCost kappa) 4 threePathComplex = 1 / kappa := by
530 rw [historyCost_path kappa hk, historyCost_edge kappa hk, historyCost_point kappa,
531 historyCost_threePath kappa hk]
532 field_simp <;> norm_num
533
534/-- **A third diamond, negative.** The three-edge out-star split as its front
535out-fork plus its last edge along the hub: glued `3 / kappa + 1 / kappa`, direct
536`6 / kappa`, defect `-2 / kappa`. Defects come in both signs. -/
537theorem diamond_J_outStar (kappa : ℝ) (hk : kappa ≠ 0) :
538 historyCost (jCost kappa) 4 forkComplex
539 + historyCost (jCost kappa) 4 edgeComplex
540 - historyCost (jCost kappa) 4 pointComplex
541 - historyCost (jCost kappa) 4 outStarComplex = -2 / kappa := by
542 rw [historyCost_fork kappa hk, historyCost_edge kappa hk, historyCost_point kappa,
543 historyCost_outStar kappa hk]
544 field_simp <;> norm_num
545
546/-- **The control.** Disjoint union is exact: two disjoint edges accumulate
547`2 / kappa` either way. Not every diamond fails. -/
548theorem diamond_J_disjoint (kappa : ℝ) (hk : kappa ≠ 0) :
549 historyCost (jCost kappa) 4 edgeComplex
550 + historyCost (jCost kappa) 4 edgeComplex
551 - historyCost (jCost kappa) 4 (emptyComplex 4)
552 - historyCost (jCost kappa) 4 twoEdgeComplex = 0 := by
553 rw [historyCost_edge kappa hk, historyCost_empty kappa, historyCost_twoEdge kappa hk]
554 field_simp <;> norm_num
555
556/-- **J is not a function of the three counts.** The count vector `(2, 1, 0)`
557is carried by two complexes whose costs differ: the proper edge pays `1 / kappa`,
558the loop with an isolated vertex pays nothing. The lattice conflict therefore
559precedes any gluing diamond. -/
560theorem jCost_not_a_function_of_counts (kappa : ℝ) (hk : kappa ≠ 0) :
561 edgeComplex.nV = loopPointComplex.nV ∧ edgeComplex.nE = loopPointComplex.nE
562 ∧ edgeComplex.nT = loopPointComplex.nT
563 ∧ historyCost (jCost kappa) 4 edgeComplex
564 ≠ historyCost (jCost kappa) 4 loopPointComplex := by
565 refine ⟨rfl, rfl, rfl, ?_⟩
566 rw [historyCost_edge kappa hk, historyCost_loopPoint kappa]
567 exact one_div_ne_zero hk
568
569end
570
571/-! ### The seed diamonds in subcomplex form, with the localization identity checked
572
573Finset union and intersection values do not reduce in the kernel (they carry
574nodup proof terms), and finset equality and disjointness decidability route
575through quotient instances the kernel cannot unfold, so the cover, disjointness,
576and interface facts below are proved propositionally. Only the sub-imbalance
577values, which are filter-and-card computations, are kernel-decided. -/
578
579/-- The left edge of the two-edge path, with its two vertices. -/
580def pathLeft : Subcomplex pathComplex where
581 verts := ({0, 1} : Finset (Fin 3))
582 edges := ({0} : Finset (Fin 2))
583 tail_mem := by
584 intro e he
585 obtain rfl := Finset.mem_singleton.mp he
586 exact Finset.mem_insert_self _ _
587 head_mem := by
588 intro e he
589 obtain rfl := Finset.mem_singleton.mp he
590 exact Finset.mem_insert_of_mem (Finset.mem_singleton_self _)
591
592/-- The right edge of the two-edge path, with its two vertices. -/
593def pathRight : Subcomplex pathComplex where
594 verts := ({1, 2} : Finset (Fin 3))
595 edges := ({1} : Finset (Fin 2))
596 tail_mem := by
597 intro e he
598 obtain rfl := Finset.mem_singleton.mp he
599 exact Finset.mem_insert_self _ _
600 head_mem := by
601 intro e he
602 obtain rfl := Finset.mem_singleton.mp he
603 exact Finset.mem_insert_of_mem (Finset.mem_singleton_self _)
604
605theorem seed_edges_cover : pathLeft.edges ∪ pathRight.edges = Finset.univ := by
606 rw [Finset.eq_univ_iff_forall]
607 intro e
608 fin_cases e <;> simp [pathLeft, pathRight]
609
610theorem seed_edges_disjoint : Disjoint pathLeft.edges pathRight.edges := by
611 rw [Finset.disjoint_iff_ne]
612 intro a ha b hb
613 obtain rfl := Finset.mem_singleton.mp (show a ∈ ({0} : Finset (Fin 2)) from ha)
614 obtain rfl := Finset.mem_singleton.mp (show b ∈ ({1} : Finset (Fin 2)) from hb)
615 exact Fin.zero_ne_one
616
617theorem seed_interface : pathLeft.verts ∩ pathRight.verts = ({1} : Finset (Fin 3)) := by
618 ext v
619 fin_cases v <;> simp [pathLeft, pathRight]
620
621theorem subImbalance_pathLeft_one :
622 subImbalance pathComplex pathLeft.edges (1 : Fin 3) = 1 := by decide
623
624theorem subImbalance_pathRight_one :
625 subImbalance pathComplex pathRight.edges (1 : Fin 3) = -1 := by decide
626
627/-- **The seed diamond, kernel-computed.** The A15 witness in its lattice form:
628defect `2` in units of `1 / (2 * kappa)`, i.e. `1 / kappa` in `J` units. -/
629theorem seed_diamond_defect : diamondDefect pathComplex pathLeft pathRight = 2 := by
630 rw [diamondDefect_eq_neg_two_inner _ _ _ seed_edges_cover seed_edges_disjoint,
631 seed_interface, Finset.sum_singleton, subImbalance_pathLeft_one,
632 subImbalance_pathRight_one] <;> norm_num
633
634/-- The interface imbalance coupling on the seed: the shared vertex carries
635`m_A = 1` and `m_B = -1`, and `-2 * (1 * -1) = 2` is the defect. -/
636theorem seed_diamond_localized :
637 diamondDefect pathComplex pathLeft pathRight
638 = -2 * ∑ v ∈ pathLeft.verts ∩ pathRight.verts,
639 subImbalance pathComplex pathLeft.edges v
640 * subImbalance pathComplex pathRight.edges v :=
641 diamondDefect_eq_neg_two_inner pathComplex pathLeft pathRight
642 seed_edges_cover seed_edges_disjoint
643
644theorem seed_inner_product :
645 (∑ v ∈ pathLeft.verts ∩ pathRight.verts,
646 subImbalance pathComplex pathLeft.edges v
647 * subImbalance pathComplex pathRight.edges v) = -1 := by
648 rw [seed_interface, Finset.sum_singleton, subImbalance_pathLeft_one,
649 subImbalance_pathRight_one] <;> norm_num
650
651/-- The front two edges of the three-edge path. -/
652def threePathLeft : Subcomplex threePathComplex where
653 verts := ({0, 1, 2} : Finset (Fin 4))
654 edges := ({0, 1} : Finset (Fin 3))
655 tail_mem := by
656 intro e he
657 rcases Finset.mem_insert.mp he with rfl | h
658 · exact Finset.mem_insert_self _ _
659 · obtain rfl := Finset.mem_singleton.mp h
660 exact Finset.mem_insert_of_mem (Finset.mem_insert_self _ _)
661 head_mem := by
662 intro e he
663 rcases Finset.mem_insert.mp he with rfl | h
664 · exact Finset.mem_insert_of_mem (Finset.mem_insert_self _ _)
665 · obtain rfl := Finset.mem_singleton.mp h
666 exact Finset.mem_insert_of_mem
667 (Finset.mem_insert_of_mem (Finset.mem_singleton_self _))
668
669/-- The last edge of the three-edge path. -/
670def threePathRight : Subcomplex threePathComplex where
671 verts := ({2, 3} : Finset (Fin 4))
672 edges := ({2} : Finset (Fin 3))
673 tail_mem := by
674 intro e he
675 obtain rfl := Finset.mem_singleton.mp he
676 exact Finset.mem_insert_self _ _
677 head_mem := by
678 intro e he
679 obtain rfl := Finset.mem_singleton.mp he
680 exact Finset.mem_insert_of_mem (Finset.mem_singleton_self _)
681
682theorem threePath_edges_cover : threePathLeft.edges ∪ threePathRight.edges = Finset.univ := by
683 show (({0, 1} : Finset (Fin 3)) ∪ ({2} : Finset (Fin 3))) = Finset.univ
684 rw [Finset.eq_univ_iff_forall]
685 intro e
686 fin_cases e <;> simp
687
688theorem threePath_edges_disjoint : Disjoint threePathLeft.edges threePathRight.edges := by
689 rw [Finset.disjoint_iff_ne]
690 intro a ha b hb
691 have ha' : a ∈ ({0, 1} : Finset (Fin 3)) := ha
692 rcases Finset.mem_insert.mp ha' with rfl | h
693 · obtain rfl := Finset.mem_singleton.mp (show b ∈ ({2} : Finset (Fin 3)) from hb)
694 decide
695 · obtain rfl := Finset.mem_singleton.mp h
696 obtain rfl := Finset.mem_singleton.mp (show b ∈ ({2} : Finset (Fin 3)) from hb)
697 decide
698
699theorem threePath_interface :
700 threePathLeft.verts ∩ threePathRight.verts = ({2} : Finset (Fin 4)) := by
701 show (({0, 1, 2} : Finset (Fin 4)) ∩ ({2, 3} : Finset (Fin 4))) = {2}
702 ext v
703 fin_cases v <;> simp
704
705theorem subImbalance_threePathLeft_two :
706 subImbalance threePathComplex threePathLeft.edges (2 : Fin 4) = 1 := by decide
707
708theorem subImbalance_threePathRight_two :
709 subImbalance threePathComplex threePathRight.edges (2 : Fin 4) = -1 := by decide
710
711/-- The three-edge path diamond, kernel-computed: defect `2`. The middle vertex
712carries `m_A = 1` and `m_B = -1`. -/
713theorem threePath_diamond_defect :
714 diamondDefect threePathComplex threePathLeft threePathRight = 2 := by
715 rw [diamondDefect_eq_neg_two_inner _ _ _ threePath_edges_cover threePath_edges_disjoint,
716 threePath_interface, Finset.sum_singleton, subImbalance_threePathLeft_two,
717 subImbalance_threePathRight_two] <;> norm_num
718
719/-- The front fork of the out-star. -/
720def outStarFork : Subcomplex outStarComplex where
721 verts := ({0, 1, 2} : Finset (Fin 4))
722 edges := ({0, 1} : Finset (Fin 3))
723 tail_mem := by
724 intro e he
725 rcases Finset.mem_insert.mp he with rfl | h
726 · exact Finset.mem_insert_self _ _
727 · obtain rfl := Finset.mem_singleton.mp h
728 exact Finset.mem_insert_self _ _
729 head_mem := by
730 intro e he
731 rcases Finset.mem_insert.mp he with rfl | h
732 · exact Finset.mem_insert_of_mem (Finset.mem_insert_self _ _)
733 · obtain rfl := Finset.mem_singleton.mp h
734 exact Finset.mem_insert_of_mem
735 (Finset.mem_insert_of_mem (Finset.mem_singleton_self _))
736
737/-- The last spur of the out-star. -/
738def outStarSpur : Subcomplex outStarComplex where
739 verts := ({0, 3} : Finset (Fin 4))
740 edges := ({2} : Finset (Fin 3))
741 tail_mem := by
742 intro e he
743 obtain rfl := Finset.mem_singleton.mp he
744 exact Finset.mem_insert_self _ _
745 head_mem := by
746 intro e he
747 obtain rfl := Finset.mem_singleton.mp he
748 exact Finset.mem_insert_of_mem (Finset.mem_singleton_self _)
749
750theorem outStar_edges_cover : outStarFork.edges ∪ outStarSpur.edges = Finset.univ := by
751 show (({0, 1} : Finset (Fin 3)) ∪ ({2} : Finset (Fin 3))) = Finset.univ
752 rw [Finset.eq_univ_iff_forall]
753 intro e
754 fin_cases e <;> simp
755
756theorem outStar_edges_disjoint : Disjoint outStarFork.edges outStarSpur.edges := by
757 rw [Finset.disjoint_iff_ne]
758 intro a ha b hb
759 have ha' : a ∈ ({0, 1} : Finset (Fin 3)) := ha
760 rcases Finset.mem_insert.mp ha' with rfl | h
761 · obtain rfl := Finset.mem_singleton.mp (show b ∈ ({2} : Finset (Fin 3)) from hb)
762 decide
763 · obtain rfl := Finset.mem_singleton.mp h
764 obtain rfl := Finset.mem_singleton.mp (show b ∈ ({2} : Finset (Fin 3)) from hb)
765 decide
766
767theorem outStar_interface :
768 outStarFork.verts ∩ outStarSpur.verts = ({0} : Finset (Fin 4)) := by
769 show (({0, 1, 2} : Finset (Fin 4)) ∩ ({0, 3} : Finset (Fin 4))) = {0}
770 ext v
771 fin_cases v <;> simp
772
773theorem subImbalance_outStarFork_zero :
774 subImbalance outStarComplex outStarFork.edges (0 : Fin 4) = -2 := by decide
775
776theorem subImbalance_outStarSpur_zero :
777 subImbalance outStarComplex outStarSpur.edges (0 : Fin 4) = -1 := by decide
778
779/-- The out-star diamond, kernel-computed: defect `-4` in units of
780`1 / (2 * kappa)`, i.e. `-2 / kappa` in `J` units. The hub carries `m_A = -2`
781and `m_B = -1`, and `-2 * ((-2) * (-1)) = -4`. -/
782theorem outStar_diamond_defect :
783 diamondDefect outStarComplex outStarFork outStarSpur = -4 := by
784 rw [diamondDefect_eq_neg_two_inner _ _ _ outStar_edges_cover outStar_edges_disjoint,
785 outStar_interface, Finset.sum_singleton, subImbalance_outStarFork_zero,
786 subImbalance_outStarSpur_zero] <;> norm_num
787
788theorem outStar_localized :
789 diamondDefect outStarComplex outStarFork outStarSpur
790 = -2 * ∑ v ∈ outStarFork.verts ∩ outStarSpur.verts,
791 subImbalance outStarComplex outStarFork.edges v
792 * subImbalance outStarComplex outStarSpur.edges v :=
793 diamondDefect_eq_neg_two_inner outStarComplex outStarFork outStarSpur
794 outStar_edges_cover outStar_edges_disjoint
795
796theorem outStar_inner_product :
797 (∑ v ∈ outStarFork.verts ∩ outStarSpur.verts,
798 subImbalance outStarComplex outStarFork.edges v
799 * subImbalance outStarComplex outStarSpur.edges v) = 2 := by
800 rw [outStar_interface, Finset.sum_singleton, subImbalance_outStarFork_zero,
801 subImbalance_outStarSpur_zero] <;> norm_num
802
803/-- The first edge of the two disjoint edges. -/
804def twoEdgeLeft : Subcomplex twoEdgeComplex where
805 verts := ({0, 1} : Finset (Fin 4))
806 edges := ({0} : Finset (Fin 2))
807 tail_mem := by
808 intro e he
809 obtain rfl := Finset.mem_singleton.mp he
810 exact Finset.mem_insert_self _ _
811 head_mem := by
812 intro e he
813 obtain rfl := Finset.mem_singleton.mp he
814 exact Finset.mem_insert_of_mem (Finset.mem_singleton_self _)
815
816/-- The second of the two disjoint edges. -/
817def twoEdgeRight : Subcomplex twoEdgeComplex where
818 verts := ({2, 3} : Finset (Fin 4))
819 edges := ({1} : Finset (Fin 2))
820 tail_mem := by
821 intro e he
822 obtain rfl := Finset.mem_singleton.mp he
823 exact Finset.mem_insert_self _ _
824 head_mem := by
825 intro e he
826 obtain rfl := Finset.mem_singleton.mp he
827 exact Finset.mem_insert_of_mem (Finset.mem_singleton_self _)
828
829theorem twoEdge_edges_cover : twoEdgeLeft.edges ∪ twoEdgeRight.edges = Finset.univ := by
830 rw [Finset.eq_univ_iff_forall]
831 intro e
832 fin_cases e <;> simp [twoEdgeLeft, twoEdgeRight]
833
834theorem twoEdge_edges_disjoint : Disjoint twoEdgeLeft.edges twoEdgeRight.edges := by
835 rw [Finset.disjoint_iff_ne]
836 intro a ha b hb
837 obtain rfl := Finset.mem_singleton.mp (show a ∈ ({0} : Finset (Fin 2)) from ha)
838 obtain rfl := Finset.mem_singleton.mp (show b ∈ ({1} : Finset (Fin 2)) from hb)
839 exact Fin.zero_ne_one
840
841theorem twoEdge_interface_empty : twoEdgeLeft.verts ∩ twoEdgeRight.verts = ∅ := by
842 ext v
843 fin_cases v <;> simp [twoEdgeLeft, twoEdgeRight]
844
845/-- The disjoint control, kernel-computed: defect `0`, as the empty-interface
846corollary forces. -/
847theorem twoEdge_diamond_defect :
848 diamondDefect twoEdgeComplex twoEdgeLeft twoEdgeRight = 0 :=
849 diamondDefect_eq_zero_of_inter_empty twoEdgeComplex twoEdgeLeft twoEdgeRight
850 twoEdge_edges_cover twoEdge_edges_disjoint twoEdge_interface_empty
851
852/-! ## §5. The relation lattice: rank, the null direction, and the inconsistency -/
853
854/-- **MEASURED: the distinct left-hand rows of the cap-4 J-diamond lattice.**
855Every realized count vector: the empty complex, and `(nV, nE, 0)` for
856`1 ≤ nV ≤ 4`, `0 ≤ nE ≤ 4`. Provenance: `scripts/qg/out/j_diamond_rank_20260730.json`.
857Every row has zero `c_T` coefficient because `J` charges top-cell letters nothing
858(`jCost_tet`), so no J-relation can ever see the tet rate. -/
859def latticeLHS : List (ℚ × ℚ × ℚ) :=
860 [(0, 0, 0),
861 (1, 0, 0), (1, 1, 0), (1, 2, 0), (1, 3, 0), (1, 4, 0),
862 (2, 0, 0), (2, 1, 0), (2, 2, 0), (2, 3, 0), (2, 4, 0),
863 (3, 0, 0), (3, 1, 0), (3, 2, 0), (3, 3, 0), (3, 4, 0),
864 (4, 0, 0), (4, 1, 0), (4, 2, 0), (4, 3, 0), (4, 4, 0)]
865
866theorem latticeLHS_count : latticeLHS.length = 21 := rfl
867
868/-- Every measured row has zero `c_T` coefficient: the tet rate is a structural
869null direction of the whole lattice. -/
870theorem latticeLHS_cT_null : ∀ r ∈ latticeLHS, r.2.2 = 0 := by decide
871
872/-- The two directions every row lies along: the point and the single loop. -/
873def rowU : ℚ × ℚ × ℚ := (1, 0, 0)
874
875/-- The single loop at a vertex. -/
876def rowW : ℚ × ℚ × ℚ := (1, 1, 0)
877
878theorem latticeLHS_mem_U : rowU ∈ latticeLHS := by decide
879
880theorem latticeLHS_mem_W : rowW ∈ latticeLHS := by decide
881
882theorem lattice_lhs_in_span : ∀ r ∈ latticeLHS,
883 r = (r.1 - r.2.1) • rowU + r.2.1 • rowW := by
884 intro r hr
885 obtain ⟨a, b, c⟩ := r
886 have hc : c = 0 := latticeLHS_cT_null _ hr
887 subst hc
888 rw [Prod.ext_iff, Prod.ext_iff]
889 refine ⟨?_, ?_, ?_⟩ <;> simp [rowU, rowW] <;> ring
890
891theorem lattice_rows_independent (x y : ℚ)
892 (h : x • rowU + y • rowW = 0) : x = 0 ∧ y = 0 := by
893 have h1 := congrArg (fun p : ℚ × ℚ × ℚ => p.1) h
894 have h2 := congrArg (fun p : ℚ × ℚ × ℚ => p.2.1) h
895 simp only [rowU, rowW, Prod.fst, Prod.snd, smul_eq_mul] at h1 h2
896 simp at h1 h2
897 constructor <;> linarith
898
899/-- **The left-hand rank of the lattice is exactly two.** Every measured row
900lies in the span of two measured rows, and those two are independent. The
901missing third direction is the tet rate, which `J` cannot see. -/
902theorem lattice_lhs_rank_two :
903 (∀ r ∈ latticeLHS, r = (r.1 - r.2.1) • rowU + r.2.1 • rowW)
904 ∧ (∀ x y : ℚ, x • rowU + y • rowW = 0 → x = 0 ∧ y = 0)
905 ∧ rowU ∈ latticeLHS ∧ rowW ∈ latticeLHS :=
906 ⟨lattice_lhs_in_span, lattice_rows_independent, latticeLHS_mem_U, latticeLHS_mem_W⟩
907
908/-- The augmented seed row of the point: `C_V = 0`. -/
909def augPoint : ℚ × ℚ × ℚ × ℚ := (1, 0, 0, 0)
910
911/-- The augmented seed row of the edge: `2 C_V + C_E = 2`. -/
912def augEdge : ℚ × ℚ × ℚ × ℚ := (2, 1, 0, 2)
913
914/-- The augmented seed row of the two-edge path, direct order:
915`3 C_V + 2 C_E = 2`. -/
916def augPath : ℚ × ℚ × ℚ × ℚ := (3, 2, 0, 2)
917
918/-- **The augmented rank is three.** The point, edge, and path rows with their
919right-hand sides attached are independent, so the right-hand side carries
920information the three left-hand directions cannot: the system overshoots the
921left-hand rank by exactly one. -/
922theorem seed_augmented_independent (x y z : ℚ)
923 (h : x • augPoint + y • augEdge + z • augPath = 0) : x = 0 ∧ y = 0 ∧ z = 0 := by
924 have h0 := congrArg (fun p : ℚ × ℚ × ℚ × ℚ => p.1) h
925 have h1 := congrArg (fun p : ℚ × ℚ × ℚ × ℚ => p.2.1) h
926 have h3 := congrArg (fun p : ℚ × ℚ × ℚ × ℚ => p.2.2.2) h
927 simp only [augPoint, augEdge, augPath, Prod.fst, Prod.snd, smul_eq_mul] at h0 h1 h3
928 simp at h0 h1 h3
929 refine ⟨?_, ?_, ?_⟩ <;> linarith
930
931/-- **HEADLINE (the lattice is inconsistent).** No rational rate triple solves
932the four seed rows: the point forces `C_V = 0`, the edge forces `C_E = 2`, the
933direct path then demands `2 = 2` while the glued path demands `2 = 4`. The two
934accumulation orders of the A15 diamond cannot both be paid by any additive
935letter cost. -/
936theorem lattice_inconsistent_seed :
937 ¬ ∃ C : Fin 3 → ℚ,
938 C 0 = 0
939 ∧ 2 * C 0 + C 1 = 2
940 ∧ 3 * C 0 + 2 * C 1 = 2
941 ∧ 3 * C 0 + 2 * C 1 = 4 := by
942 rintro ⟨C, h0, h1, h2, h3⟩
943 linarith
944
945/-- **The conflict precedes any gluing.** The count vector `(2, 1, 0)` alone
946demands `2 C_V + C_E` equal both `0` (loop with an isolated vertex) and `2`
947(proper edge): `J` is not even a function of the three counts. -/
948theorem lattice_inconsistent_counts :
949 ¬ ∃ C : Fin 3 → ℚ,
950 C 0 = 0 ∧ 2 * C 0 + C 1 = 2 ∧ 2 * C 0 + C 1 = 0 := by
951 rintro ⟨C, h0, h1, h2⟩
952 linarith
953
954/-! ## §6. The measured tallies, mirrored
955
956Exact integer enumeration, `scripts/qg/qg_j_diamond_rank_20260730.py`, receipt
957`scripts/qg/out/j_diamond_rank_20260730.json`. Every tally below is MEASURED;
958each decisive one is restated as a kernel-checked fact immediately after. -/
959
960/-- Per-cap enumeration tallies. `rankA` is the left-hand rank of the lattice
961at that cap, `rankAug` the augmented rank; the two differ exactly when the
962lattice is inconsistent. -/
963structure CapTally where
964 classes : ℕ
965 wide : ℕ
966 genuine : ℕ
967 genuineNonzero : ℕ
968 elementary : ℕ
969 elementaryNonzero : ℕ
970 bilinearChecked : ℕ
971 bilinearOk : ℕ
972 localizationViolations : ℕ
973 maxAbsDefect : ℤ
974 rankA : ℕ
975 rankAug : ℕ
976
977/-- MEASURED tallies at caps 1, 2, 3, 4. -/
978def measuredCaps : Fin 4 → CapTally :=
979 ![{ classes := 3, wide := 0, genuine := 0, genuineNonzero := 0,
980 elementary := 0, elementaryNonzero := 0,
981 bilinearChecked := 0, bilinearOk := 0, localizationViolations := 0,
982 maxAbsDefect := 0, rankA := 2, rankAug := 2 },
983 { classes := 13, wide := 21, genuine := 14, genuineNonzero := 2,
984 elementary := 7, elementaryNonzero := 0,
985 bilinearChecked := 19, bilinearOk := 19, localizationViolations := 0,
986 maxAbsDefect := 4, rankA := 2, rankAug := 3 },
987 { classes := 68, wide := 1051, genuine := 814, genuineNonzero := 258,
988 elementary := 146, elementaryNonzero := 17,
989 bilinearChecked := 619, bilinearOk := 619, localizationViolations := 0,
990 maxAbsDefect := 8, rankA := 2, rankAug := 3 },
991 { classes := 437, wide := 42823, genuine := 36079, genuineNonzero := 15359,
992 elementary := 2132, elementaryNonzero := 389,
993 bilinearChecked := 16988, bilinearOk := 16988, localizationViolations := 0,
994 maxAbsDefect := 16, rankA := 2, rankAug := 3 }]
995
996/-- MEASURED, restated in the kernel: at cap 4 the left-hand rank is 2 and the
997augmented rank is 3, so the lattice is inconsistent there. -/
998theorem measured_rank_cap4 :
999 (measuredCaps 3).rankA = 2 ∧ (measuredCaps 3).rankAug = 3 := ⟨rfl, rfl⟩
1000
1001/-- MEASURED, restated: the bilinear identity held on every edge-disjoint
1002diamond enumerated, at every cap. This is the measured half of
1003`diamondDefect_eq_neg_two_inner`. -/
1004theorem measured_bilinear_perfect :
1005 ∀ i : Fin 4, (measuredCaps i).bilinearChecked = (measuredCaps i).bilinearOk := by
1006 decide
1007
1008/-- MEASURED, restated: no nonzero edge-disjoint defect lacked a two-sided
1009imbalanced interface vertex, at any cap. The measured half of
1010`diamondDefect_eq_zero_of_interface_balanced`. -/
1011theorem measured_no_localization_violations :
1012 ∀ i : Fin 4, (measuredCaps i).localizationViolations = 0 := by decide
1013
1014/-- MEASURED, restated: the seed diamond enters at cap 3, where 17 of the 146
1015elementary diamonds are nonzero; the verdict is already inconsistent at cap 2
1016through the count conflict. -/
1017theorem measured_seed_enters_cap3 :
1018 (measuredCaps 1).rankAug = 3
1019 ∧ (measuredCaps 2).elementary = 146
1020 ∧ (measuredCaps 2).elementaryNonzero = 17 := ⟨rfl, rfl, rfl⟩
1021
1022/-! ## §7. The verdict -/
1023
1024/-- **The C15 J-diamond lattice verdict.** The localization theorem and its two
1025corollaries; the evenness of the spectrum; the three kernel-computed J-unit
1026diamonds and the disjoint control; the count conflict; the rank facts; and the
1027inconsistency of the seed rows. -/
1028structure JDiamondRankVerdict : Prop where
1029 defect_is_interface_coupling : ∀ (K : BoundedComplex 4) (A Bd : Subcomplex K),
1030 A.edges ∪ Bd.edges = Finset.univ → Disjoint A.edges Bd.edges →
1031 diamondDefect K A Bd
1032 = -2 * ∑ v ∈ A.verts ∩ Bd.verts,
1033 subImbalance K A.edges v * subImbalance K Bd.edges v
1034 interface_localization : ∀ (K : BoundedComplex 4) (A Bd : Subcomplex K),
1035 A.edges ∪ Bd.edges = Finset.univ → Disjoint A.edges Bd.edges →
1036 (∀ v ∈ A.verts ∩ Bd.verts,
1037 subImbalance K A.edges v = 0 ∨ subImbalance K Bd.edges v = 0) →
1038 diamondDefect K A Bd = 0
1039 empty_interface_exact : ∀ (K : BoundedComplex 4) (A Bd : Subcomplex K),
1040 A.edges ∪ Bd.edges = Finset.univ → Disjoint A.edges Bd.edges →
1041 A.verts ∩ Bd.verts = ∅ → diamondDefect K A Bd = 0
1042 spectrum_even : ∀ K : BoundedComplex 4, 2 ∣ imbalanceSq K
1043 seed_defect_kernel : diamondDefect pathComplex pathLeft pathRight = 2
1044 seed_diamond_J : ∀ kappa : ℝ, kappa ≠ 0 →
1045 historyCost (jCost kappa) 4 edgeComplex
1046 + historyCost (jCost kappa) 4 edgeComplex
1047 - historyCost (jCost kappa) 4 pointComplex
1048 - historyCost (jCost kappa) 4 pathComplex = 1 / kappa
1049 negative_diamond_J : ∀ kappa : ℝ, kappa ≠ 0 →
1050 historyCost (jCost kappa) 4 forkComplex
1051 + historyCost (jCost kappa) 4 edgeComplex
1052 - historyCost (jCost kappa) 4 pointComplex
1053 - historyCost (jCost kappa) 4 outStarComplex = -2 / kappa
1054 disjoint_control_J : ∀ kappa : ℝ, kappa ≠ 0 →
1055 historyCost (jCost kappa) 4 edgeComplex
1056 + historyCost (jCost kappa) 4 edgeComplex
1057 - historyCost (jCost kappa) 4 (emptyComplex 4)
1058 - historyCost (jCost kappa) 4 twoEdgeComplex = 0
1059 not_a_function_of_counts : ∀ kappa : ℝ, kappa ≠ 0 →
1060 edgeComplex.nV = loopPointComplex.nV ∧ edgeComplex.nE = loopPointComplex.nE
1061 ∧ edgeComplex.nT = loopPointComplex.nT
1062 ∧ historyCost (jCost kappa) 4 edgeComplex
1063 ≠ historyCost (jCost kappa) 4 loopPointComplex
1064 lhs_null_direction : ∀ r ∈ latticeLHS, r.2.2 = 0
1065 lhs_rank_two :
1066 (∀ r ∈ latticeLHS, r = (r.1 - r.2.1) • rowU + r.2.1 • rowW)
1067 ∧ (∀ x y : ℚ, x • rowU + y • rowW = 0 → x = 0 ∧ y = 0)
1068 ∧ rowU ∈ latticeLHS ∧ rowW ∈ latticeLHS
1069 augmented_rank_three : ∀ x y z : ℚ,
1070 x • augPoint + y • augEdge + z • augPath = 0 → x = 0 ∧ y = 0 ∧ z = 0
1071 inconsistent_seed :
1072 ¬ ∃ C : Fin 3 → ℚ,
1073 C 0 = 0
1074 ∧ 2 * C 0 + C 1 = 2
1075 ∧ 3 * C 0 + 2 * C 1 = 2
1076 ∧ 3 * C 0 + 2 * C 1 = 4
1077 inconsistent_counts :
1078 ¬ ∃ C : Fin 3 → ℚ,
1079 C 0 = 0 ∧ 2 * C 0 + C 1 = 2 ∧ 2 * C 0 + C 1 = 0
1080 measured_rank : (measuredCaps 3).rankA = 2 ∧ (measuredCaps 3).rankAug = 3
1081 measured_bilinear : ∀ i : Fin 4,
1082 (measuredCaps i).bilinearChecked = (measuredCaps i).bilinearOk
1083 measured_localization : ∀ i : Fin 4, (measuredCaps i).localizationViolations = 0
1084
1085theorem jDiamondRankVerdict : JDiamondRankVerdict where
1086 defect_is_interface_coupling := diamondDefect_eq_neg_two_inner
1087 interface_localization := diamondDefect_eq_zero_of_interface_balanced
1088 empty_interface_exact := diamondDefect_eq_zero_of_inter_empty
1089 spectrum_even := imbalanceSq_even
1090 seed_defect_kernel := seed_diamond_defect
1091 seed_diamond_J := diamond_J_seed
1092 negative_diamond_J := diamond_J_outStar
1093 disjoint_control_J := diamond_J_disjoint
1094 not_a_function_of_counts := jCost_not_a_function_of_counts
1095 lhs_null_direction := latticeLHS_cT_null
1096 lhs_rank_two := lattice_lhs_rank_two
1097 augmented_rank_three := seed_augmented_independent
1098 inconsistent_seed := lattice_inconsistent_seed
1099 inconsistent_counts := lattice_inconsistent_counts
1100 measured_rank := measured_rank_cap4
1101 measured_bilinear := measured_bilinear_perfect
1102 measured_localization := measured_no_localization_violations
1103
1104/-! ## Axiom audit -/
1105
1106#print axioms subImbalance_eq_zero_of_not_mem
1107#print axioms subImbalance_union
1108#print axioms diamondDefect_eq_neg_two_inner
1109#print axioms diamondDefect_eq_zero_of_inter_empty
1110#print axioms diamondDefect_eq_zero_of_interface_balanced
1111#print axioms sum_vertexImbalance
1112#print axioms imbalanceSq_even
1113#print axioms historyCost_jCost_eq
1114#print axioms historyCost_edge
1115#print axioms historyCost_twoEdge
1116#print axioms historyCost_fork
1117#print axioms historyCost_outStar
1118#print axioms historyCost_loopPoint
1119#print axioms historyCost_empty
1120#print axioms diamond_J_seed
1121#print axioms diamond_J_threePath
1122#print axioms diamond_J_outStar
1123#print axioms diamond_J_disjoint
1124#print axioms jCost_not_a_function_of_counts
1125#print axioms seed_edges_cover
1126#print axioms seed_edges_disjoint
1127#print axioms seed_interface
1128#print axioms subImbalance_pathLeft_one
1129#print axioms subImbalance_pathRight_one
1130#print axioms seed_diamond_defect
1131#print axioms seed_diamond_localized
1132#print axioms seed_inner_product
1133#print axioms threePath_edges_cover
1134#print axioms threePath_edges_disjoint
1135#print axioms threePath_interface
1136#print axioms threePath_diamond_defect
1137#print axioms outStar_edges_cover
1138#print axioms outStar_edges_disjoint
1139#print axioms outStar_interface
1140#print axioms outStar_diamond_defect
1141#print axioms outStar_localized
1142#print axioms outStar_inner_product
1143#print axioms twoEdge_edges_cover
1144#print axioms twoEdge_edges_disjoint
1145#print axioms twoEdge_interface_empty
1146#print axioms twoEdge_diamond_defect
1147#print axioms latticeLHS_cT_null
1148#print axioms lattice_lhs_in_span
1149#print axioms lattice_rows_independent
1150#print axioms lattice_lhs_rank_two
1151#print axioms seed_augmented_independent
1152#print axioms lattice_inconsistent_seed
1153#print axioms lattice_inconsistent_counts
1154#print axioms measured_rank_cap4
1155#print axioms measured_bilinear_perfect
1156#print axioms measured_no_localization_violations
1157#print axioms measured_seed_enters_cap3
1158#print axioms jDiamondRankVerdict
1159
1160end Gap2JDiamondRank
1161end SevenGaps
1162end Gravity
1163end IndisputableMonolith
1164