IndisputableMonolith.Gravity.SevenGaps.Gap2IncidenceParity
IndisputableMonolith/Gravity/SevenGaps/Gap2IncidenceParity.lean · 270 lines · 16 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerCohomology
2
3/-!
4# Gap 2 / C10: parity of the incidence class under reversal involutions
5
6The C10 parity audit of the Track D observable program (panel receipt
7`state/panel/qg-track-d-observable-20260731_20260731_140423.json`): does the
8ledger incidence complex admit an orientation or letter-reversal involution `ι`
9under which the genuine incidence class is parity-ODD, `ι*[c] = −[c]`? The C9
10birefringence bet needs exactly such a sign: a holonomy read off refinement
11histories must flip sign when the history is reversed.
12
13## Verdict: NO. The class is even under every involution the ledger supports,
14and no self-map of the complex space pulls it back to its negative.
15
16The genuine class is `incidenceCost 1`, whose C18 history at `K` is the count
17`properEdgeCount K` (kernel theorem `historyCost_incidenceCost`). Parity is
18read at the level of history functions, because two C18 classes agree exactly
19when their histories agree at every complex (a ledger coboundary is a
20history-zero cost). The library's objects supply three families of candidate
21involutions, and each is EVEN on the class:
22
231. **Letter permutations**, including the serial-name reversal
24 `letterReversal K` below: pulling a cost back along a permutation of the
25 posting alphabet re-indexes the history sum, which changes nothing
26 (`Equiv.sum_comp`). Every class is even under every letter permutation,
27 involutive or not, and no equivariance hypothesis is needed.
282. **Relabelings**: the class is gauge-equivariant
29 (`incidenceCost_equivariant`), so its history is invariant
30 (`historyCost_invariant`).
313. **Edge-orientation reversal** `edgeReverse`: swap the two endpoints of every
32 edge. The carrier's `edgeVerts` is an ordered pair with no ordering
33 constraint, so this is a genuine self-map of `BoundedComplex B`; it is
34 involutive, and it is NOT a relabeling (the label-erasure module records
35 that reversing a directed edge lies outside `Aut`). But the loop/proper
36 dichotomy is symmetric in the two endpoints (`ne_comm`), so
37 `properEdgeCount` is invariant: the class is even here too.
38
39The odd alternative is excluded outright (`no_odd_pullback_of_incidence_class`):
40for `t ≠ 0` there is no self-map `F` of the bounded-complex space, involutive
41or not, with `historyCost (incidenceCost t) B (F B K)` equal to
42`− historyCost (incidenceCost t) B K` at every `K`. At `twoBridges` the class
43has history `2t`; any pullback re-evaluates the same non-negative count
44`t · properEdgeCount (F 2 twoBridges)` at another complex, and that can never
45equal `−2t`. The involution requirement never even enters: a non-negative
46count that is positive somewhere cannot be odd under any pullback, because a
47pullback is still an evaluation of that same count.
48
49## Scope notes
50
51* The scalar map `c ↦ −c` on cochains would make every class of every theory
52 odd trivially; it is a coefficient operation, not an orientation or letter
53 reversal of the ledger's objects, so it is not a candidate the question
54 admits, and adding it would be observable shopping.
55* A28 (`Gap2GaugeTransport`) concerns configuration-level count-functionals.
56 This lane is history/class level: the pairing is the C18 history of a letter
57 cost, and the kill mechanism is the sign of a count, not the A28 washout.
58 A28 is neither used nor contradicted here.
59* Consequence: the C9 birefringence lane closes on the scope of the genuine
60 incidence class (the exhibited H^1 generator), and the C10 leg of the panel's
61 frozen signing condition is SATISFIED permanently by the even/absent verdict.
62 The banking sentence stays unsigned because C11 returned a nonzero branch
63 (the class is visible to ratio probes) and the C2 audit is still out.
64 The transgression
65 question on 1-cycles is moot: there is no odd class to transgress.
66 No flag moves; `FullTheoryLedger` is not imported.
67
68Expected axiom footprint: `[propext, Classical.choice, Quot.sound]`.
69-/
70
71namespace IndisputableMonolith
72namespace Gravity
73namespace SevenGaps
74namespace Gap2IncidenceParity
75
76open PathSumMeasure ExactShellGaugePreflight Gap2GaugeVolume Gap2GluingDerivation
77open GaugeHistoryMeasure Gap2SizeBlindnessReach Gap2PostingCostDerivation
78open Gap2LetterCostDichotomy Gap2LedgerCohomology
79
80noncomputable section
81
82variable {B : ℕ}
83
84/-! ## §1. The letter-reversal involution -/
85
86/-- **Letter reversal**: reverse the serial-name order within each letter kind
87(`Fin.revPerm` on vertices, edges, and tetrahedra), transported across the
88posting alphabet by the library's own `postingAlphEquiv`. This is the
89letter-reversal involution the question names: it permutes which letter sits
90at which serial position, reversing the posting order. -/
91def letterReversal (K : BoundedComplex B) : Equiv.Perm (PostingAlphabet K) :=
92 postingAlphEquiv Fin.revPerm Fin.revPerm Fin.revPerm
93
94/-- Letter reversal is an involution: reversing the serial names twice returns
95every letter to itself. -/
96theorem letterReversal_involutive (K : BoundedComplex B) :
97 Function.Involutive (letterReversal K) := by
98 intro a
99 rcases a with v | (e | t)
100 · exact congrArg Sum.inl (Fin.rev_involutive v)
101 · exact congrArg (Sum.inr ∘ Sum.inl) (Fin.rev_involutive e)
102 · exact congrArg (Sum.inr ∘ Sum.inr) (Fin.rev_involutive t)
103
104/-- Pullback of a letter cost along a family of letter permutations:
105precomposition on the posting alphabet. -/
106def letterPullback (c : LetterCost)
107 (π : ∀ (B : ℕ) (K : BoundedComplex B), Equiv.Perm (PostingAlphabet K)) :
108 LetterCost :=
109 fun B K a => c B K (π B K a)
110
111/-- Every letter permutation is EVEN on every class: re-indexing a finite sum
112changes nothing. No equivariance hypothesis is needed. -/
113theorem historyCost_letterPullback (c : LetterCost)
114 (π : ∀ (B : ℕ) (K : BoundedComplex B), Equiv.Perm (PostingAlphabet K))
115 (B : ℕ) (K : BoundedComplex B) :
116 historyCost (letterPullback c π) B K = historyCost c B K :=
117 Equiv.sum_comp (π B K) (fun a => c B K a)
118
119/-- **The genuine incidence class is even under letter reversal.** -/
120theorem incidence_class_even_under_letterReversal
121 (t : ℝ) (B : ℕ) (K : BoundedComplex B) :
122 historyCost (letterPullback (incidenceCost t) (fun _ K' => letterReversal K')) B K
123 = historyCost (incidenceCost t) B K :=
124 historyCost_letterPullback _ _ _ _
125
126/-! ## §2. The edge-orientation reversal involution -/
127
128/-- **Orientation reversal**: swap the two endpoints of every edge. The
129carrier is directed and ordered (`edgeVerts e : Fin nV × Fin nV`, loops
130allowed, no ordering constraint), so swapping endpoints yields another bounded
131complex with the same letters. -/
132def edgeReverse (K : BoundedComplex B) : BoundedComplex B where
133 nV := K.nV
134 nE := K.nE
135 nT := K.nT
136 hV := K.hV
137 hE := K.hE
138 hT := K.hT
139 edgeVerts := fun e => (K.edgeVerts e).swap
140 tetVerts := K.tetVerts
141
142/-- Swapping a pair twice returns it. (Stated locally so the involution
143proofs do not depend on Mathlib lemma roulette.) -/
144private theorem swap_swap {α β : Type*} (p : α × β) : Prod.swap (Prod.swap p) = p := by
145 cases p
146 rfl
147
148/-- Orientation reversal is an involution on the incidence data: swapping both
149endpoints of every edge twice returns every edge to itself. -/
150theorem edgeReverse_edgeVerts_involutive (K : BoundedComplex B) (e : Fin K.nE) :
151 (edgeReverse (edgeReverse K)).edgeVerts e = K.edgeVerts e :=
152 swap_swap _
153
154/-- Orientation reversal is an involution of the complex itself. -/
155theorem edgeReverse_involutive (B : ℕ) :
156 Function.Involutive (edgeReverse (B := B)) := by
157 intro K
158 cases K
159 congr
160
161/-- Orientation reversal as a permutation of the labeled carrier. -/
162def edgeReverseEquiv (B : ℕ) : Equiv.Perm (BoundedComplex B) where
163 toFun := edgeReverse
164 invFun := edgeReverse
165 left_inv := edgeReverse_involutive B
166 right_inv := edgeReverse_involutive B
167
168/-- `properEdgeCount` is invariant under orientation reversal: the loop/proper
169dichotomy `v₁ ≠ v₂` is symmetric in the two endpoints. -/
170theorem properEdgeCount_edgeReverse (K : BoundedComplex B) :
171 properEdgeCount (edgeReverse K) = properEdgeCount K := by
172 unfold properEdgeCount
173 exact congrArg Finset.card (Finset.filter_congr (fun i _ => ne_comm))
174
175/-- **The genuine incidence class is even under orientation reversal.** The
176pullback re-evaluates the history at the reversed complex, and the history is
177unchanged because `properEdgeCount` is invariant. -/
178theorem incidence_class_even_under_edgeReverse (t : ℝ) (B : ℕ) (K : BoundedComplex B) :
179 historyCost (incidenceCost t) B (edgeReverse K)
180 = historyCost (incidenceCost t) B K := by
181 rw [historyCost_incidenceCost, historyCost_incidenceCost,
182 properEdgeCount_edgeReverse]
183
184/-- **The genuine incidence class is even under every relabeling**: gauge
185equivariance of `incidenceCost`, restated at the level of the class. -/
186theorem incidence_class_even_under_relabel (t : ℝ) {K K' : BoundedComplex B}
187 (r : Relabel K K') :
188 historyCost (incidenceCost t) B K = historyCost (incidenceCost t) B K' :=
189 historyCost_invariant (incidenceCost_equivariant t) r
190
191/-! ## §3. No odd pullback exists -/
192
193/-- **C10 headline: the incidence class admits no odd pullback.** For `t ≠ 0`
194there is no self-map `F` of the bounded-complex space, involutive or not,
195pulling `[incidenceCost t]` back to its negative. The parity-odd equation
196fails at `twoBridges`: the class has history `2t` there, while any pullback
197re-evaluates the same non-negative count `t · properEdgeCount (F 2 twoBridges)`
198at another complex, which cannot equal `−2t`. Equality of C18 classes is
199equality of history functions (a ledger coboundary is exactly a history-zero
200cost), so the class-level odd equation fails already as a function equation. -/
201theorem no_odd_pullback_of_incidence_class {t : ℝ} (ht : t ≠ 0) :
202 ¬ ∃ F : (B : ℕ) → BoundedComplex B → BoundedComplex B,
203 ∀ (B : ℕ) (K : BoundedComplex B),
204 historyCost (incidenceCost t) B (F B K)
205 = - historyCost (incidenceCost t) B K := by
206 rintro ⟨F, hF⟩
207 have h := hF 2 twoBridges
208 rw [historyCost_incidenceCost, historyCost_incidenceCost,
209 properEdgeCount_twoBridges] at h
210 have h2 : t * (properEdgeCount (F 2 twoBridges) : ℝ) = t * (-2) := by
211 rw [h]
212 ring
213 have h3 : (properEdgeCount (F 2 twoBridges) : ℝ) = -2 := mul_left_cancel₀ ht h2
214 have hnonneg : (0 : ℝ) ≤ (properEdgeCount (F 2 twoBridges) : ℝ) := Nat.cast_nonneg _
215 linarith
216
217/-- **No odd involution exists** (the C10 question at the genuine class
218`incidenceCost 1`). Every self-map of the complex space, and so every
219involution, pulls the class's history back to a non-negative count, never to
220its negative. -/
221theorem no_odd_involution_exists :
222 ¬ ∃ F : (B : ℕ) → BoundedComplex B → BoundedComplex B,
223 ∀ (B : ℕ) (K : BoundedComplex B),
224 historyCost (incidenceCost (1 : ℝ)) B (F B K)
225 = - historyCost (incidenceCost (1 : ℝ)) B K :=
226 no_odd_pullback_of_incidence_class one_ne_zero
227
228/-! ## §4. Verdict package -/
229
230/-- **C10 parity verdict.** The genuine incidence class is EVEN under every
231involution the ledger's objects support (letter reversal, edge-orientation
232reversal, and every relabeling), and it admits no odd pullback at all. The C9
233birefringence lane, which needed a sign-changing holonomy on refinement
234histories, has no substrate in the incidence complex; the unsigned banking
235sentence's C10 condition fails. Flag unmoved. -/
236theorem incidence_parity_verdict (t : ℝ) (ht : t ≠ 0) :
237 (∀ (K : BoundedComplex B), Function.Involutive (letterReversal K))
238 ∧ Function.Involutive (edgeReverse (B := B))
239 ∧ (∀ (K : BoundedComplex B),
240 historyCost (incidenceCost t) B (edgeReverse K)
241 = historyCost (incidenceCost t) B K)
242 ∧ ¬ ∃ F : (B : ℕ) → BoundedComplex B → BoundedComplex B,
243 ∀ (B : ℕ) (K : BoundedComplex B),
244 historyCost (incidenceCost t) B (F B K)
245 = - historyCost (incidenceCost t) B K :=
246 ⟨letterReversal_involutive, edgeReverse_involutive B,
247 fun K => incidence_class_even_under_edgeReverse t _ K,
248 no_odd_pullback_of_incidence_class ht⟩
249
250end
251
252/-! ## Axiom audit -/
253
254#print axioms letterReversal_involutive
255#print axioms historyCost_letterPullback
256#print axioms incidence_class_even_under_letterReversal
257#print axioms edgeReverse_edgeVerts_involutive
258#print axioms edgeReverse_involutive
259#print axioms properEdgeCount_edgeReverse
260#print axioms incidence_class_even_under_edgeReverse
261#print axioms incidence_class_even_under_relabel
262#print axioms no_odd_pullback_of_incidence_class
263#print axioms no_odd_involution_exists
264#print axioms incidence_parity_verdict
265
266end Gap2IncidenceParity
267end SevenGaps
268end Gravity
269end IndisputableMonolith
270