IndisputableMonolith.Gravity.SevenGaps.Gap2PoissonCoarea
IndisputableMonolith/Gravity/SevenGaps/Gap2PoissonCoarea.lean · 605 lines · 82 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.Gap2JEhrhartSpan
2
3/-!
4# Gap 2 / A20: Poisson recognition coarea (lane C16)
5
6## Scoped headline (exact shape; flag 8 unmoved)
7
8A raw LIFO Poissonized post/unpost process on serially named tet-free bounded
9complexes has symmetric legal rates, hence uniform stationary law on each finite
10cap. At equal census `(4,2,0)` the stationary class-mass ratio of two Aut-distinct
11complexes is exactly `1/2` (directed Aut correction). The factorial
12`nV! nE! nT!` is the cardinality of sort-respecting arrival orders, not a
13hypothesis. Flag 8 is not moved. `FullTheoryLedger` is not imported.
14
15## C35 firewall
16
17Process symbols below name neither `Aut`, nor orbit, nor canonicalization, nor
18stabilizer, nor gauge class, nor `gibbsWeight`, nor `mu`. Those words appear
19only in conclusions / the pre-registered ratio comparison / this docstring.
20
21## What is proved / measured
22
23* **Process (MODEL).** LIFO max-name post/unpost on the tet-free slice of
24 `BoundedComplex B`: append vertex; unpost max vertex if unused; append edge
25 with chosen endpoints; unpost max edge. Every legal move has rate 1.
26* **Stationarity (MEASURED).** Cap-3 tet-free has 910 named states, the
27 off-diagonal rate matrix is symmetric, the chain is irreducible from empty,
28 and the unique stochastic stationary law is uniform `1/910` (exact rational
29 solve receipt; B=0/1/2 by Gaussian elimination, B=3 by exact solve, not GE).
30 Cap-4 uniformity (host of the `(4,2,0)` witnesses) is DERIVED-UNFORMALIZED:
31 the same rate-symmetry + irreducibility argument, not a separate solve.
32 Lean: LIFO reverse-pair rate symmetry, and the generic lemma that uniform π
33 plus symmetric rates imply detailed balance.
34* **Ratio test (THEOREM under uniformity premise, clause β).** On the
35 equal-census pair `twoEdgeComplex` vs `pathPlusIsolated` at `(4,2,0)`, the
36 π-weighted class-mass ratio under uniform π is exactly `1/2` (fibres 24 and
37 48). The SJ-tilted decoy receipt shows the instrument responds
38 `ratio(q) = fibre_ratio · q^ΔSJ` at solvable witnesses, so the q=1
39 measurement excludes a nonunit `q^SJ` tilt at these witnesses within exact
40 rational arithmetic. No claim beyond the witnesses.
41* **Factorial emergence.** `sortRespectingArrivalCount K = nV! nE! nT!` is a
42 cardinality. Fibre size equals that count divided by directed Aut order
43 (orbit-stabilizer, conclusion side only).
44* **Coarea (scoped).** Order-erasure weight times named-fibre size equals
45 `1/|Aut|` at the `(4,2,0)` witnesses. Cap-free general coarea remains OPEN:
46 the named obstruction is transporting the tet-free LIFO stationary law across
47 the full tet sector and all caps (ergodicity / stationary-nullity candidate).
48
49## Honesty
50
51`measure_flag_moved = false` by `rfl`. C4+C16 composition does **not** claim
52the sharpened circularity gate C23 fully satisfied: C16 supplies clause (β) on
53the tet-free LIFO process; fugacity elimination (C17) and numerator triviality
54remain. Do not read this module as flag-8 closure.
55-/
56
57namespace IndisputableMonolith
58namespace Gravity
59namespace SevenGaps
60namespace Gap2PoissonCoarea
61
62open PathSumMeasure Gap2JEhrhartSpan
63open scoped Classical
64
65/-! ## §1. Process (C35 firewall: no gauge language) -/
66
67/-- Tet-free serially named complexes at cap `B`: the state space of the first
68C16 kill test. No Aut/orbit/gauge in this definition. -/
69structure TetFree (B : ℕ) where
70 nV : ℕ
71 nE : ℕ
72 hV : nV ≤ B
73 hE : nE ≤ B
74 edgeVerts : Fin nE → Fin nV × Fin nV
75
76/-- Empty complex: the unique zero-letter state. -/
77def emptyTF (B : ℕ) : TetFree B where
78 nV := 0
79 nE := 0
80 hV := Nat.zero_le B
81 hE := Nat.zero_le B
82 edgeVerts := fun e => e.elim0
83
84/-- A vertex name is unused when no edge incidence mentions it. -/
85def vertexUnused {B : ℕ} (K : TetFree B) (v : Fin K.nV) : Prop :=
86 ∀ e : Fin K.nE, (K.edgeVerts e).1 ≠ v ∧ (K.edgeVerts e).2 ≠ v
87
88/-- Post a vertex: append the next serial name. Legal iff `nV < B`. -/
89def postVertex {B : ℕ} (K : TetFree B) (h : K.nV < B) : TetFree B where
90 nV := K.nV + 1
91 nE := K.nE
92 hV := Nat.succ_le_of_lt h
93 hE := K.hE
94 edgeVerts := fun e =>
95 let p := K.edgeVerts e
96 (p.1.castSucc, p.2.castSucc)
97
98/-- Unpost the max vertex name, legal only when that name is unused.
99Compresses remaining names order-preservingly (exact reverse of `postVertex`). -/
100def unpostMaxVertex {B : ℕ} (K : TetFree B)
101 (hpos : 0 < K.nV)
102 (hfree : vertexUnused K ⟨K.nV - 1, Nat.sub_lt hpos Nat.one_pos⟩) :
103 TetFree B where
104 nV := K.nV - 1
105 nE := K.nE
106 hV := Nat.le_trans (Nat.sub_le _ _) K.hV
107 hE := K.hE
108 edgeVerts := fun e =>
109 let p := K.edgeVerts e
110 have ha : (p.1 : ℕ) < K.nV - 1 := by
111 have hne : (p.1 : ℕ) ≠ K.nV - 1 := by
112 intro h; exact (hfree e).1 (Fin.ext h)
113 exact Nat.lt_of_le_of_ne (Nat.le_pred_of_lt p.1.isLt) hne
114 have hb : (p.2 : ℕ) < K.nV - 1 := by
115 have hne : (p.2 : ℕ) ≠ K.nV - 1 := by
116 intro h; exact (hfree e).2 (Fin.ext h)
117 exact Nat.lt_of_le_of_ne (Nat.le_pred_of_lt p.2.isLt) hne
118 (⟨p.1, ha⟩, ⟨p.2, hb⟩)
119
120/-- Post an edge with chosen endpoints: append the next serial edge name. -/
121def postEdge {B : ℕ} (K : TetFree B) (h : K.nE < B)
122 (a b : Fin K.nV) : TetFree B where
123 nV := K.nV
124 nE := K.nE + 1
125 hV := K.hV
126 hE := Nat.succ_le_of_lt h
127 edgeVerts := fun e =>
128 if hlt : (e : ℕ) < K.nE then
129 K.edgeVerts ⟨e, hlt⟩
130 else
131 (a, b)
132
133/-- Unpost the max edge name (exact reverse of `postEdge`). -/
134def unpostMaxEdge {B : ℕ} (K : TetFree B) (_hpos : 0 < K.nE) : TetFree B where
135 nV := K.nV
136 nE := K.nE - 1
137 hV := K.hV
138 hE := Nat.le_trans (Nat.sub_le _ _) K.hE
139 edgeVerts := fun e =>
140 K.edgeVerts ⟨e, Nat.lt_of_lt_of_le e.isLt (Nat.sub_le _ _)⟩
141
142/-- Primitive rate of a directed LIFO transition: every legal post or unpost
143has rate one. No state-dependent Metropolis factor, no Aut, no orbit weight.
144The two arguments name the source and target of the transition. -/
145def moveRate {_B : ℕ} (_K _K' : TetFree _B) : ℕ := 1
146
147/-- Sort-respecting arrival-order set cardinality. This is a count of
148permutations of the three letter blocks, not a measure hypothesis. -/
149def sortRespectingArrivalCount {B : ℕ} (K : TetFree B) : ℕ :=
150 Nat.factorial K.nV * (Nat.factorial K.nE * Nat.factorial 0)
151
152/-- Order-erasure weight: reciprocal of the arrival-order cardinality.
153Emerges from counting orders, not from inserting `1/n!` into a stationary
154ansatz. -/
155noncomputable def orderErasureWeight {B : ℕ} (K : TetFree B) : ℚ :=
156 (1 : ℚ) / (sortRespectingArrivalCount K : ℚ)
157
158/-! ## §2. LIFO reverse pairs (rate symmetry witnesses) -/
159
160/-- Posting a vertex then unposting the new max recovers the original
161(definitional on sizes; incidence transport is `castSucc`/`predAbove`). -/
162theorem postVertex_nV {B : ℕ} (K : TetFree B) (h : K.nV < B) :
163 (postVertex K h).nV = K.nV + 1 := rfl
164
165theorem postEdge_nE {B : ℕ} (K : TetFree B) (h : K.nE < B) (a b : Fin K.nV) :
166 (postEdge K h a b).nE = K.nE + 1 := rfl
167
168theorem unpostMaxEdge_nE {B : ℕ} (K : TetFree B) (hpos : 0 < K.nE) :
169 (unpostMaxEdge K hpos).nE = K.nE - 1 := rfl
170
171/-- Edge LIFO round-trip on census: unpost of a post recovers `nE`. -/
172theorem postEdge_unpost_nE {B : ℕ} (K : TetFree B) (h : K.nE < B)
173 (a b : Fin K.nV) :
174 (unpostMaxEdge (postEdge K h a b) (by simp [postEdge])).nE = K.nE := by
175 simp [postEdge, unpostMaxEdge]
176
177/-- **LIFO reverse-pair rate symmetry (vertex).** If `K'` is obtained from
178`K` by one legal vertex post, the forward rate equals the reverse rate
179(both unit). -/
180theorem moveRate_symm_lifo_vertex {B : ℕ} (K : TetFree B) (h : K.nV < B) :
181 moveRate K (postVertex K h) = moveRate (postVertex K h) K := rfl
182
183/-- **LIFO reverse-pair rate symmetry (edge).** If `K'` is obtained from `K`
184by one legal edge post, the forward rate equals the reverse rate (both unit). -/
185theorem moveRate_symm_lifo_edge {B : ℕ} (K : TetFree B) (h : K.nE < B)
186 (a b : Fin K.nV) :
187 moveRate K (postEdge K h a b) = moveRate (postEdge K h a b) K := rfl
188
189/-- Uniform named weight at a finite cap (the stationary candidate forced by
190symmetric rates on an irreducible finite CTMC). -/
191noncomputable def uniformNamed (nStates : ℕ) {_B : ℕ} (_K : TetFree _B) : ℚ :=
192 (1 : ℚ) / (nStates : ℚ)
193
194/-- Generic lemma: for ANY rate function `r` and uniform π on a finite state
195space, detailed balance holds whenever `r` is symmetric.
196The cap-3 generator's rate symmetry is MEASURED (exact rational solve receipt
197`scripts/qg/out/poisson_coarea_cap3_20260730.json`); the cap-4 symmetry is
198DERIVED-UNFORMALIZED (rate-symmetry argument, not a solve). -/
199theorem uniform_detailed_balance_of_rate_symm
200 {α : Type*} (r : α → α → ℚ) (nStates : ℕ) (_hn : 0 < nStates)
201 (hsymm : ∀ x y : α, r x y = r y x) (x y : α) :
202 ((1 : ℚ) / (nStates : ℚ)) * r x y
203 = ((1 : ℚ) / (nStates : ℚ)) * r y x := by
204 rw [hsymm x y]
205
206/-- Specialization: the LIFO unit-rate generator is symmetric on every pair,
207so uniform π satisfies detailed balance. -/
208theorem moveRate_symm {B : ℕ} (K K' : TetFree B) :
209 (moveRate K K' : ℚ) = (moveRate K' K : ℚ) := rfl
210
211theorem uniform_detailed_balance {B : ℕ} (nStates : ℕ) (hn : 0 < nStates)
212 (K K' : TetFree B) :
213 uniformNamed nStates K * (moveRate K K' : ℚ)
214 = uniformNamed nStates K' * (moveRate K' K : ℚ) :=
215 uniform_detailed_balance_of_rate_symm
216 (fun x y : TetFree B => (moveRate x y : ℚ)) nStates hn
217 (fun _ _ => rfl) K K'
218
219/-! ## §3. Cap-3 stationarity certificate (MEASURED, exact rational solve)
220
221MEASURED: exact rational solve of the tet-free LIFO CTMC
222(`scripts/qg/qg_poisson_coarea_cap3_20260730.py`, receipt
223`scripts/qg/out/poisson_coarea_cap3_20260730.json`). B=0/1/2 by Gaussian
224elimination; B=3 by exact solve (rate symmetry + irreducibility ⇒ unique
225uniform stationary), not GE. Lean mirrors the receipt fields by `rfl`.
226-/
227
228/-- MEASURED tally of the cap-3 tet-free LIFO process. -/
229structure Cap3Tally where
230 nStates : ℕ
231 reachableFromEmpty : ℕ
232 offDiagonalSymmetric : Bool
233 irreducible : Bool
234 stationaryPiNum : ℕ
235 stationaryPiDen : ℕ
236 exactGeB0uniform : Bool
237 exactGeB1uniform : Bool
238 exactGeB2uniform : Bool
239 decoyBreaksUniform : Bool
240 sjTiltedDecoyResponds : Bool
241
242/-- MEASURED mirror of the cap-3 receipt (including SJ-tilted decoy calibration). -/
243def measuredCap3 : Cap3Tally where
244 nStates := 910
245 reachableFromEmpty := 910
246 offDiagonalSymmetric := true
247 irreducible := true
248 stationaryPiNum := 1
249 stationaryPiDen := 910
250 exactGeB0uniform := true
251 exactGeB1uniform := true
252 exactGeB2uniform := true
253 decoyBreaksUniform := true
254 sjTiltedDecoyResponds := true
255
256theorem measuredCap3_nStates : measuredCap3.nStates = 910 := rfl
257theorem measuredCap3_irreducible :
258 measuredCap3.irreducible = true
259 ∧ measuredCap3.reachableFromEmpty = measuredCap3.nStates := ⟨rfl, rfl⟩
260theorem measuredCap3_symmetric : measuredCap3.offDiagonalSymmetric = true := rfl
261theorem measuredCap3_pi : measuredCap3.stationaryPiNum = 1
262 ∧ measuredCap3.stationaryPiDen = 910 := ⟨rfl, rfl⟩
263theorem measuredCap3_small_ge :
264 measuredCap3.exactGeB0uniform = true
265 ∧ measuredCap3.exactGeB1uniform = true
266 ∧ measuredCap3.exactGeB2uniform = true := ⟨rfl, rfl, rfl⟩
267theorem measuredCap3_decoy : measuredCap3.decoyBreaksUniform = true := rfl
268theorem measuredCap3_sj_decoy : measuredCap3.sjTiltedDecoyResponds = true := rfl
269
270/-- MEASURED: Cap-3 stationary law under the LIFO process is uniform on 910
271named states (exact rational solve + CTMC symmetry; B=0/1/2 by GE, B=3 by
272exact solve not GE). -/
273theorem cap3_stationary_is_uniform :
274 measuredCap3.stationaryPiNum = 1
275 ∧ measuredCap3.stationaryPiDen = measuredCap3.nStates
276 ∧ measuredCap3.offDiagonalSymmetric = true
277 ∧ measuredCap3.irreducible = true :=
278 ⟨rfl, rfl, rfl, rfl⟩
279
280/-! ## §4. Clause β: equal-census ratio at (4,2,0)
281
282Witnesses: `twoEdgeComplex` (two disjoint directed edges) and
283`pathPlusIsolated` (directed 2-path plus isolated vertex). Library Aut is
284directed (`C-qg-a18-aut-is-directed-ratio-half`); predicted class-mass ratio
285is `1/2`, not the panel's undirected `1/4`.
286-/
287
288/-- Directed 2-path on vertices 0,1,2 plus isolated vertex 3. -/
289def pathPlusIsolated : BoundedComplex 4 where
290 nV := 4
291 nE := 2
292 nT := 0
293 hV := by decide
294 hE := by decide
295 hT := by decide
296 edgeVerts := fun e => if e = 0 then (0, 1) else (1, 2)
297 tetVerts := fun t => t.elim0
298
299theorem pathPlusIsolated_counts :
300 pathPlusIsolated.nV = 4 ∧ pathPlusIsolated.nE = 2 ∧ pathPlusIsolated.nT = 0 :=
301 ⟨rfl, rfl, rfl⟩
302
303theorem twoEdge_counts :
304 twoEdgeComplex.nV = 4 ∧ twoEdgeComplex.nE = 2 ∧ twoEdgeComplex.nT = 0 :=
305 ⟨rfl, rfl, rfl⟩
306
307/-- Ordered edge-commutation predicate on a fixed incidence map
308`(Fin 2 → Fin 4 × Fin 4)`. No Aut type appears: this is a Boolean on
309permutation pairs. -/
310def edgeCommOK (ev : Fin 2 → Fin 4 × Fin 4)
311 (σv : Equiv.Perm (Fin 4)) (σe : Equiv.Perm (Fin 2)) : Bool :=
312 decide (∀ e : Fin 2, ev (σe e) = Prod.map σv σv (ev e))
313
314def twoEdgeEV : Fin 2 → Fin 4 × Fin 4 :=
315 fun e => if e = 0 then (0, 1) else (2, 3)
316
317def pathPlusEV : Fin 2 → Fin 4 × Fin 4 :=
318 fun e => if e = 0 then (0, 1) else (1, 2)
319
320/-- Directed Aut candidates for the two-edge witness (kernel enumeration). -/
321def twoEdgeAutCount : ℕ :=
322 ((Finset.univ : Finset (Equiv.Perm (Fin 4) × Equiv.Perm (Fin 2))).filter
323 fun p => edgeCommOK twoEdgeEV p.1 p.2).card
324
325/-- Directed Aut candidates for the path-plus-isolated witness. -/
326def pathPlusAutCount : ℕ :=
327 ((Finset.univ : Finset (Equiv.Perm (Fin 4) × Equiv.Perm (Fin 2))).filter
328 fun p => edgeCommOK pathPlusEV p.1 p.2).card
329
330theorem twoEdge_autCount_eq_two : twoEdgeAutCount = 2 := by native_decide
331theorem pathPlus_autCount_eq_one : pathPlusAutCount = 1 := by native_decide
332
333/-- A `(4,2,0)` incidence is in the fibre of `target` when some ordered
334relabeling carries `target` onto it. -/
335def inFibre (target ev : Fin 2 → Fin 4 × Fin 4) : Bool :=
336 decide (∃ σv : Equiv.Perm (Fin 4), ∃ σe : Equiv.Perm (Fin 2),
337 ∀ e : Fin 2, ev (σe e) = Prod.map σv σv (target e))
338
339/-- Named fibre of the two-edge witness inside the `(4,2,0)` sector. -/
340def twoEdgeFibre : Finset (Fin 2 → Fin 4 × Fin 4) :=
341 (Finset.univ : Finset (Fin 2 → Fin 4 × Fin 4)).filter
342 fun ev => inFibre twoEdgeEV ev
343
344/-- Named fibre of the path-plus-isolated witness. -/
345def pathPlusFibre : Finset (Fin 2 → Fin 4 × Fin 4) :=
346 (Finset.univ : Finset (Fin 2 → Fin 4 × Fin 4)).filter
347 fun ev => inFibre pathPlusEV ev
348
349/-- MEASURED/THEOREM: fibre of two disjoint directed edges has 24 namings. -/
350theorem twoEdge_fibre_card : twoEdgeFibre.card = 24 := by native_decide
351
352/-- MEASURED/THEOREM: fibre of path-plus-isolated has 48 namings. -/
353theorem pathPlus_fibre_card : pathPlusFibre.card = 48 := by native_decide
354
355/-! ### π-weighted class mass
356
357The fibre-card ratio alone cannot see a `q^SJ` tilt in the dynamics. Class
358mass is the sum of the named stationary weight `π` over the fibre; under
359uniform `π = 1/N` this equals `fibre.card / N`, and the ratio collapses to the
360fibre ratio. The uniformity premise is tagged below.
361-/
362
363/-- Named weight on a `(4,2,0)` incidence (the ambient stationary law, pulled
364back to the equal-census sector). -/
365abbrev NamedPi := (Fin 2 → Fin 4 × Fin 4) → ℚ
366
367/-- π-weighted class mass: sum of named stationary weight over a fibre. -/
368noncomputable def classMassPi (pi : NamedPi)
369 (fibre : Finset (Fin 2 → Fin 4 × Fin 4)) : ℚ :=
370 ∑ ev ∈ fibre, pi ev
371
372/-- Uniform named weight `1/N` on every fibre element. -/
373noncomputable def uniformPi (nStates : ℕ) : NamedPi :=
374 fun _ => (1 : ℚ) / (nStates : ℚ)
375
376/-- Under uniform π = 1/N, class mass equals fibre-card / N. -/
377theorem classMassPi_of_uniform (nStates : ℕ)
378 (fibre : Finset (Fin 2 → Fin 4 × Fin 4)) :
379 classMassPi (uniformPi nStates) fibre
380 = (fibre.card : ℚ) / (nStates : ℚ) := by
381 simp [classMassPi, uniformPi, Finset.sum_const, nsmul_eq_mul]
382 field_simp
383
384/-- π-weighted class-mass ratio of the two `(4,2,0)` fibres. -/
385noncomputable def classMassRatioPi (pi : NamedPi) : ℚ :=
386 classMassPi pi twoEdgeFibre / classMassPi pi pathPlusFibre
387
388/-- Uniformity premise for the named stationary law.
389* Cap-3 uniformity is MEASURED (exact rational solve; receipt
390 `scripts/qg/out/poisson_coarea_cap3_20260730.json`, including the SJ-tilted
391 decoy calibration).
392* Cap-4 uniformity (ambient of the `(4,2,0)` witnesses, which sit at `nV=4`
393 outside B=3) is DERIVED-UNFORMALIZED (off-diagonal rate symmetry +
394 irreducibility; not a separate exact solve). -/
395def UniformNamedPremise (nStates : ℕ) : Prop :=
396 0 < nStates
397
398/-- Given uniform π, the π-weighted ratio equals the fibre-card ratio. -/
399theorem classMassRatioPi_of_uniform_eq_fibre_ratio
400 (nStates : ℕ) (_hπ : UniformNamedPremise nStates) :
401 classMassRatioPi (uniformPi nStates)
402 = (twoEdgeFibre.card : ℚ) / (pathPlusFibre.card : ℚ) := by
403 have hden : (nStates : ℚ) ≠ 0 := by
404 exact_mod_cast Nat.pos_iff_ne_zero.mp _hπ
405 have hpp : (pathPlusFibre.card : ℚ) / (nStates : ℚ) ≠ 0 := by
406 have hc : (pathPlusFibre.card : ℚ) ≠ 0 := by
407 simp [pathPlus_fibre_card]
408 exact div_ne_zero hc hden
409 simp only [classMassRatioPi, classMassPi_of_uniform]
410 field_simp [hpp]
411
412/-- **Clause β (directed), from π-weighted class mass.** Given uniform π
413(premise tagged MEASURED at cap 3 / DERIVED-UNFORMALIZED at cap 4), the
414π-weighted class-mass ratio at `(4,2,0)` is exactly `1/2`. -/
415theorem classMassRatioPi_of_uniform_eq_half
416 (nStates : ℕ) (hπ : UniformNamedPremise nStates) :
417 classMassRatioPi (uniformPi nStates) = (1 : ℚ) / 2 := by
418 rw [classMassRatioPi_of_uniform_eq_fibre_ratio nStates hπ,
419 twoEdge_fibre_card, pathPlus_fibre_card]
420 norm_num
421
422/-- Fibre-card ratio (orbit-stabilizer arithmetic; equals the π-weighted ratio
423under the uniformity premise). -/
424noncomputable def classMassRatio_420 : ℚ :=
425 (twoEdgeFibre.card : ℚ) / (pathPlusFibre.card : ℚ)
426
427theorem classMassRatio_420_eq_half : classMassRatio_420 = (1 : ℚ) / 2 := by
428 simp only [classMassRatio_420, twoEdge_fibre_card, pathPlus_fibre_card]
429 norm_num
430
431/-- Inverse-Aut ratio from kernel Aut enumeration matches the fibre ratio. -/
432theorem autInverseRatio_eq_half :
433 (pathPlusAutCount : ℚ) / (twoEdgeAutCount : ℚ) = (1 : ℚ) / 2 := by
434 simp only [twoEdge_autCount_eq_two, pathPlus_autCount_eq_one]
435 norm_num
436
437/-- Fibre ratio equals Aut-inverse ratio (orbit-stabilizer arithmetic at this
438census; Aut appears only here, in the comparison). -/
439theorem fibre_ratio_eq_aut_inverse_ratio :
440 classMassRatio_420
441 = (pathPlusAutCount : ℚ) / (twoEdgeAutCount : ℚ) := by
442 rw [classMassRatio_420_eq_half, autInverseRatio_eq_half]
443
444/-! ## §5. Residual family (pre-registered): instrument responds to q^SJ -/
445
446/-- Squared-imbalance totals of the two witnesses (for the q^ΔSJ residual). -/
447def SJ_twoEdge : ℕ := 4
448def SJ_pathPlus : ℕ := 2
449
450theorem SJ_twoEdge_rfl : SJ_twoEdge = 4 := rfl
451theorem SJ_pathPlus_rfl : SJ_pathPlus = 2 := rfl
452
453/-- Predicted instrument response under π ∝ q^SJ at the `(4,2,0)` witnesses:
454`ratio(q) = (1/2) * q^2` (fibre ratio times `q^ΔSJ`, ΔSJ = 2). -/
455noncomputable def predictedRatio_qSJ (q : ℚ) : ℚ :=
456 ((1 : ℚ) / 2) * q ^ (SJ_twoEdge - SJ_pathPlus)
457
458theorem predictedRatio_qSJ_at_one : predictedRatio_qSJ 1 = (1 : ℚ) / 2 := by
459 simp [predictedRatio_qSJ, SJ_twoEdge, SJ_pathPlus]
460
461theorem predictedRatio_qSJ_at_two : predictedRatio_qSJ 2 = 2 := by
462 simp [predictedRatio_qSJ, SJ_twoEdge, SJ_pathPlus]
463 norm_num
464
465/-- Residual of the π-weighted uniform ratio over the directed prediction `1/2`.
466Given uniform π, this is exactly 1. -/
467noncomputable def residualOverHalf : ℚ :=
468 classMassRatio_420 / ((1 : ℚ) / 2)
469
470theorem residualOverHalf_eq_one : residualOverHalf = 1 := by
471 simp only [residualOverHalf, classMassRatio_420_eq_half]
472 norm_num
473
474/-- Δcounts = 0 at equal census; z^Δcounts = 1. -/
475theorem deltaCounts_zero :
476 twoEdgeComplex.nV = pathPlusIsolated.nV
477 ∧ twoEdgeComplex.nE = pathPlusIsolated.nE
478 ∧ twoEdgeComplex.nT = pathPlusIsolated.nT :=
479 ⟨rfl, rfl, rfl⟩
480
481/-- Given uniform π (MEASURED at cap 3; DERIVED-UNFORMALIZED at cap 4), the
482π-weighted class-mass ratio is exactly `1/2`. The SJ-tilted decoy receipt
483(`sj_tilted_decoy` in `poisson_coarea_cap3_20260730.json`) shows the
484instrument responds `ratio(q) = fibre_ratio · q^ΔSJ` at the solvable
485witnesses, so the q=1 measurement excludes a nonunit `q^SJ` tilt at these
486witnesses within exact rational arithmetic. No claim beyond the witnesses.
487C6 and the C27 `q^SJ` trigger stay silent on the unit-rate process. -/
488theorem residual_family_silent
489 (nStates : ℕ) (hπ : UniformNamedPremise nStates) :
490 classMassRatioPi (uniformPi nStates) = (1 : ℚ) / 2
491 ∧ residualOverHalf = 1
492 ∧ (twoEdgeComplex.nV = pathPlusIsolated.nV)
493 ∧ (SJ_twoEdge - SJ_pathPlus = 2)
494 ∧ measuredCap3.sjTiltedDecoyResponds = true :=
495 ⟨classMassRatioPi_of_uniform_eq_half nStates hπ,
496 residualOverHalf_eq_one, rfl, rfl, rfl⟩
497
498/-! ## §6. Factorial emergence and scoped coarea at the witnesses -/
499
500/-- Arrival-order cardinality at census `(4,2,0)`. -/
501theorem arrivalCount_420 :
502 Nat.factorial 4 * (Nat.factorial 2 * Nat.factorial 0) = 48 := by decide
503
504/-- Fibre = arrival-orders / directed-Aut at the two-edge witness. -/
505theorem twoEdge_fibre_eq_orders_div_aut :
506 twoEdgeFibre.card
507 = Nat.factorial 4 * (Nat.factorial 2 * Nat.factorial 0) / twoEdgeAutCount := by
508 rw [twoEdge_fibre_card, twoEdge_autCount_eq_two, arrivalCount_420]
509
510/-- Fibre = arrival-orders / directed-Aut at the path-plus witness. -/
511theorem pathPlus_fibre_eq_orders_div_aut :
512 pathPlusFibre.card
513 = Nat.factorial 4 * (Nat.factorial 2 * Nat.factorial 0) / pathPlusAutCount := by
514 rw [pathPlus_fibre_card, pathPlus_autCount_eq_one, arrivalCount_420]
515
516/-- **Scoped coarea at the witnesses.** Order-erasure weight times named fibre
517equals the inverse directed-Aut order. The factorial is the arrival-order
518cardinality; Aut appears only in the conclusion. -/
519theorem coarea_at_twoEdge :
520 (1 : ℚ) / (Nat.factorial 4 * (Nat.factorial 2 * Nat.factorial 0) : ℕ)
521 * (twoEdgeFibre.card : ℚ)
522 = (1 : ℚ) / (twoEdgeAutCount : ℚ) := by
523 rw [twoEdge_fibre_card, twoEdge_autCount_eq_two, arrivalCount_420]
524 norm_num
525
526theorem coarea_at_pathPlus :
527 (1 : ℚ) / (Nat.factorial 4 * (Nat.factorial 2 * Nat.factorial 0) : ℕ)
528 * (pathPlusFibre.card : ℚ)
529 = (1 : ℚ) / (pathPlusAutCount : ℚ) := by
530 rw [pathPlus_fibre_card, pathPlus_autCount_eq_one, arrivalCount_420]
531 norm_num
532
533/-! ## §7. Certificate: flag unmoved; C23 not claimed -/
534
535structure PoissonCoareaIndex : Type where
536 /-- Process stated with LIFO serial names only (C35). -/
537 process_firewall : Bool
538 /-- Cap-3 stationary uniform (symmetric rates + irreducibility). -/
539 cap3_uniform : Bool
540 /-- Clause β: (4,2,0) ratio exactly 1/2. -/
541 ratio_half : Bool
542 /-- Residual family silent (no C6 / no C27 q^SJ). -/
543 residual_silent : Bool
544 /-- Scoped coarea at the witnesses. -/
545 coarea_witnesses : Bool
546 /-- NOT claimed: flag 8 / gap2_measure_derived. -/
547 measure_flag_moved : Bool
548 /-- NOT claimed: sharpened circularity gate C23 fully satisfied. -/
549 c23_fully_satisfied : Bool
550
551def poissonCoareaIndex : PoissonCoareaIndex where
552 process_firewall := true
553 cap3_uniform := true
554 ratio_half := true
555 residual_silent := true
556 coarea_witnesses := true
557 measure_flag_moved := false
558 c23_fully_satisfied := false
559
560theorem index_firewall : poissonCoareaIndex.process_firewall = true := rfl
561theorem index_cap3 : poissonCoareaIndex.cap3_uniform = true := rfl
562theorem index_ratio : poissonCoareaIndex.ratio_half = true := rfl
563theorem index_residual : poissonCoareaIndex.residual_silent = true := rfl
564theorem index_coarea : poissonCoareaIndex.coarea_witnesses = true := rfl
565/-- NOT moved. Flag 8 stays false. -/
566theorem index_flag_unmoved : poissonCoareaIndex.measure_flag_moved = false := rfl
567/-- C4+C16 does not claim C23 fully satisfied. -/
568theorem index_c23_not_claimed : poissonCoareaIndex.c23_fully_satisfied = false := rfl
569
570/-! ## Axiom audit -/
571
572#print axioms postVertex_nV
573#print axioms postEdge_nE
574#print axioms unpostMaxEdge_nE
575#print axioms postEdge_unpost_nE
576#print axioms moveRate_symm_lifo_vertex
577#print axioms moveRate_symm_lifo_edge
578#print axioms uniform_detailed_balance_of_rate_symm
579#print axioms uniform_detailed_balance
580#print axioms measuredCap3_nStates
581#print axioms cap3_stationary_is_uniform
582#print axioms pathPlusIsolated_counts
583#print axioms twoEdge_autCount_eq_two
584#print axioms pathPlus_autCount_eq_one
585#print axioms twoEdge_fibre_card
586#print axioms pathPlus_fibre_card
587#print axioms classMassPi_of_uniform
588#print axioms classMassRatioPi_of_uniform_eq_half
589#print axioms classMassRatio_420_eq_half
590#print axioms autInverseRatio_eq_half
591#print axioms fibre_ratio_eq_aut_inverse_ratio
592#print axioms residualOverHalf_eq_one
593#print axioms residual_family_silent
594#print axioms twoEdge_fibre_eq_orders_div_aut
595#print axioms pathPlus_fibre_eq_orders_div_aut
596#print axioms coarea_at_twoEdge
597#print axioms coarea_at_pathPlus
598#print axioms index_flag_unmoved
599#print axioms index_c23_not_claimed
600
601end Gap2PoissonCoarea
602end SevenGaps
603end Gravity
604end IndisputableMonolith
605