IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidence4D
IndisputableMonolith/Gravity/Analysis/ReggeBlochLocalIncidence4D.lean · 319 lines · 36 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D
3import IndisputableMonolith.Gravity.Analysis.ReggeBlochAllOrbitSymbol4D
4import IndisputableMonolith.Gravity.Analysis.ReggeBlochOrbitTransport4D
5import IndisputableMonolith.Gravity.Analysis.ReggeBlochFold4D
6import IndisputableMonolith.Gravity.Analysis.ReggeHinge4DStarKernel
7
8/-!
9# Path B: 3D-style local-incidence kernels (4D continuum)
10
11Missing-factor blocker path B. Two layers:
12
131. **Mean-local (vacuous).** `K_local = K_star / r_τ` at each slot.
14 Equals Path A distinct-hinge by linearity of class-dot / pushforward.
152. **Position-resolved (non-vacuous).** Expand the star as
16 `Σ_m assembleStarMember m` evaluated at cube-translate bases
17 `hingeBase + perm(offset_m)`, then weight `1/r_τ`.
18
19MEASURED (Python receipt
20`state/qg_full_theory/probe_pathB_local_incidence_20260721.json`):
21position-resolved t11 agrees with distinct-hinge on tested TT rays;
22extending to t12 breaks symbolDir plus/cross agreement and does not hit
23EH `-1/4`. No `gap_action_recovery` flip.
24-/
25
26namespace IndisputableMonolith
27namespace Gravity
28namespace Analysis
29namespace ReggeBlochLocalIncidence4D
30
31open BigOperators
32open ReggeEdgeStencil4D
33open ReggeHinge4DOrbitClassification
34open ReggeBlochAllOrbitSymbol4D (isOrbit phaseScaleDir)
35open ReggeBlochOrbitTransport4D
36open ReggeBlochTransportedAllOrbit4D
37open ReggeBlochFold4D
38open EdgeTTDecomposition4D
39open ReggeHinge4DStarKernel (CubeTranslate)
40
41noncomputable section
42
43abbrev Mat4 := Matrix (Fin 4) (Fin 4) ℝ
44
45/-! ## §1. Vacuous mean-local Path B (= distinct-hinge) -/
46
47/-- Mean of the `r_τ` star-member local deficit kernels (= full-star / `r_τ`). -/
48def orbitMeanLocalKernel (ty : HingeOrbitType) : Fin 15 → ℝ :=
49 fun d => (orbitStarSize ty)⁻¹ * orbitSeedKernel ty d
50
51theorem orbitMeanLocalKernel_t11 (d : Fin 15) :
52 orbitMeanLocalKernel .t11 d =
53 (6 : ℝ)⁻¹ * ReggeHinge4DStarKernel.fullStarClassKernel d :=
54 rfl
55
56theorem orbitMeanLocalKernel_t11_eq_assembled_mean (d : Fin 15) :
57 orbitMeanLocalKernel .t11 d =
58 (6 : ℝ)⁻¹ * ReggeHinge4DStarKernel.fullStarClassKernelAssembled d := by
59 rw [orbitMeanLocalKernel_t11, ReggeHinge4DStarKernel.fullStarClassKernel_eq]
60
61theorem orbitMeanLocalKernel_smul_star (ty : HingeOrbitType) (d : Fin 15) :
62 orbitStarSize ty * orbitMeanLocalKernel ty d = orbitSeedKernel ty d := by
63 unfold orbitMeanLocalKernel
64 field_simp [orbitStarSize_ne_zero ty]
65
66def transportedOrbitMeanLocal (ty : HingeOrbitType) (p : Fin 24) : Fin 15 → ℝ :=
67 pushforwardClass (orbitMeanLocalKernel ty) p
68
69def slotOrbitMeanLocalKer (ty : HingeOrbitType) (s : Fin 24) (t : Fin 10) :
70 Fin 15 → ℝ :=
71 transportedOrbitMeanLocal ty (orbitCoveringPerm ty s t)
72
73theorem slotOrbitMeanLocalKer_eq_scaled (ty : HingeOrbitType)
74 (s : Fin 24) (t : Fin 10) (d : Fin 15) :
75 slotOrbitMeanLocalKer ty s t d =
76 (orbitStarSize ty)⁻¹ * slotOrbitDeficitKer ty s t d := by
77 unfold slotOrbitMeanLocalKer transportedOrbitMeanLocal
78 slotOrbitDeficitKer transportedOrbitDeficit pushforwardClass
79 orbitMeanLocalKernel
80 have h : ∀ d0 : Fin 15,
81 (if permClass (orbitCoveringPerm ty s t) d0 = d then
82 (orbitStarSize ty)⁻¹ * orbitSeedKernel ty d0 else 0) =
83 (orbitStarSize ty)⁻¹ *
84 (if permClass (orbitCoveringPerm ty s t) d0 = d then
85 orbitSeedKernel ty d0 else 0) := by
86 intro d0; split_ifs <;> ring
87 simp_rw [h, ← Finset.mul_sum]
88
89def meanLocalSlotTerm (ty : HingeOrbitType) (H : Mat4) (m : Fin 4 → ℝ)
90 (s : Fin 24) (t : Fin 10) : ℝ :=
91 if isOrbit ty s t then
92 phasedClassDot (slotOrbitAreaCov ty s t) H m (hingeBase s t) *
93 phasedClassDot (slotOrbitMeanLocalKer ty s t) H m (hingeBase s t)
94 else 0
95
96theorem meanLocalSlotTerm_eq_scaled (ty : HingeOrbitType) (H : Mat4)
97 (m : Fin 4 → ℝ) (s : Fin 24) (t : Fin 10) :
98 meanLocalSlotTerm ty H m s t =
99 (orbitStarSize ty)⁻¹ * transportedOrbitSlotTerm ty H m s t := by
100 unfold meanLocalSlotTerm transportedOrbitSlotTerm
101 by_cases h : isOrbit ty s t
102 · simp only [h, ite_true]
103 have hker :
104 phasedClassDot (slotOrbitMeanLocalKer ty s t) H m (hingeBase s t) =
105 (orbitStarSize ty)⁻¹ *
106 phasedClassDot (slotOrbitDeficitKer ty s t) H m
107 (hingeBase s t) := by
108 unfold phasedClassDot
109 have hpt : ∀ d : Fin 15,
110 slotOrbitMeanLocalKer ty s t d *
111 planeWaveClassPert H m (hingeBase s t) d =
112 (orbitStarSize ty)⁻¹ *
113 (slotOrbitDeficitKer ty s t d *
114 planeWaveClassPert H m (hingeBase s t) d) := by
115 intro d
116 rw [slotOrbitMeanLocalKer_eq_scaled]
117 ring
118 simp_rw [hpt, ← Finset.mul_sum]
119 rw [hker]
120 ring
121 · simp [h]
122
123def blochFoldOrbitMeanLocal (ty : HingeOrbitType) (H : Mat4)
124 (m : Fin 4 → ℝ) : ℝ :=
125 ∑ s : Fin 24, ∑ t : Fin 10, meanLocalSlotTerm ty H m s t
126
127theorem blochFoldOrbitMeanLocal_eq_scaled (ty : HingeOrbitType) (H : Mat4)
128 (m : Fin 4 → ℝ) :
129 blochFoldOrbitMeanLocal ty H m =
130 (orbitStarSize ty)⁻¹ * blochFoldOrbit ty H m := by
131 unfold blochFoldOrbitMeanLocal blochFoldOrbit
132 simp_rw [meanLocalSlotTerm_eq_scaled, ← Finset.mul_sum]
133
134/-- Vacuous Path B fold (= distinct-hinge). -/
135def blochFoldAllMeanLocal (H : Mat4) (m : Fin 4 → ℝ) : ℝ :=
136 ∑ ty : HingeOrbitType, blochFoldOrbitMeanLocal ty H m
137
138theorem blochFoldAllMeanLocal_eq_distinctHinge (H : Mat4) (m : Fin 4 → ℝ) :
139 blochFoldAllMeanLocal H m = blochFoldAllDistinctHinge H m := by
140 unfold blochFoldAllMeanLocal blochFoldAllDistinctHinge
141 refine Finset.sum_congr rfl fun ty _ =>
142 blochFoldOrbitMeanLocal_eq_scaled ty H m
143
144/-! ## §2. Mean-local m² -/
145
146def m2MeanLocalOrbitSlotCoeff (ty : HingeOrbitType) (H : Mat4)
147 (dir : Fin 4 → ℝ) (s : Fin 24) (t : Fin 10) : ℝ :=
148 if isOrbit ty s t then
149 (∑ d : Fin 15, slotOrbitAreaCov ty s t d * classCoeff H d) *
150 (-(1 / 2 : ℝ) *
151 ∑ d : Fin 15,
152 slotOrbitMeanLocalKer ty s t d * classCoeff H d *
153 (phaseScaleDir dir (hingeBase s t) d) ^ 2)
154 else 0
155
156theorem m2MeanLocalOrbitSlotCoeff_eq_scaled (ty : HingeOrbitType) (H : Mat4)
157 (dir : Fin 4 → ℝ) (s : Fin 24) (t : Fin 10) :
158 m2MeanLocalOrbitSlotCoeff ty H dir s t =
159 (orbitStarSize ty)⁻¹ * m2TransportedOrbitSlotCoeff ty H dir s t := by
160 change m2MeanLocalOrbitSlotCoeff ty H dir s t =
161 (orbitStarSize ty)⁻¹ * m2TransportedOrbitSlotCoeffTrunc ty H dir s t
162 unfold m2MeanLocalOrbitSlotCoeff m2TransportedOrbitSlotCoeffTrunc
163 by_cases h : isOrbit ty s t
164 · simp only [h, ↓reduceIte]
165 have hsum :
166 (∑ d : Fin 15,
167 slotOrbitMeanLocalKer ty s t d * classCoeff H d *
168 (phaseScaleDir dir (hingeBase s t) d) ^ 2) =
169 (orbitStarSize ty)⁻¹ *
170 ∑ d : Fin 15,
171 slotOrbitDeficitKer ty s t d * classCoeff H d *
172 (phaseScaleDir dir (hingeBase s t) d) ^ 2 := by
173 have hpt : ∀ d : Fin 15,
174 slotOrbitMeanLocalKer ty s t d * classCoeff H d *
175 (phaseScaleDir dir (hingeBase s t) d) ^ 2 =
176 (orbitStarSize ty)⁻¹ *
177 (slotOrbitDeficitKer ty s t d * classCoeff H d *
178 (phaseScaleDir dir (hingeBase s t) d) ^ 2) := by
179 intro d
180 rw [slotOrbitMeanLocalKer_eq_scaled]
181 ring
182 simp_rw [hpt, ← Finset.mul_sum]
183 rw [hsum]
184 ring
185 · simp only [h, ↓reduceIte, mul_zero]
186
187def m2MeanLocalOrbitMoment (ty : HingeOrbitType) (H : Mat4)
188 (dir : Fin 4 → ℝ) : ℝ :=
189 ∑ s : Fin 24, ∑ t : Fin 10, m2MeanLocalOrbitSlotCoeff ty H dir s t
190
191theorem m2MeanLocalOrbitMoment_eq_scaled (ty : HingeOrbitType) (H : Mat4)
192 (dir : Fin 4 → ℝ) :
193 m2MeanLocalOrbitMoment ty H dir =
194 (orbitStarSize ty)⁻¹ * m2TransportedOrbitMoment ty H dir := by
195 unfold m2MeanLocalOrbitMoment m2TransportedOrbitMoment
196 simp_rw [m2MeanLocalOrbitSlotCoeff_eq_scaled, ← Finset.mul_sum]
197
198def m2MeanLocalAllOrbitMoment (H : Mat4) (dir : Fin 4 → ℝ) : ℝ :=
199 ∑ ty : HingeOrbitType, m2MeanLocalOrbitMoment ty H dir
200
201theorem m2MeanLocalAllOrbitMoment_eq_distinctHinge (H : Mat4)
202 (dir : Fin 4 → ℝ) :
203 m2MeanLocalAllOrbitMoment H dir =
204 m2TransportedAllOrbitMomentDistinctHinge H dir := by
205 unfold m2MeanLocalAllOrbitMoment m2TransportedAllOrbitMomentDistinctHinge
206 refine Finset.sum_congr rfl fun ty _ =>
207 m2MeanLocalOrbitMoment_eq_scaled ty H dir
208
209theorem m2MeanLocalAllOrbitMoment_smul (c : ℝ) (H : Mat4) (dir : Fin 4 → ℝ) :
210 m2MeanLocalAllOrbitMoment (c • H) dir =
211 c ^ 2 * m2MeanLocalAllOrbitMoment H dir := by
212 rw [m2MeanLocalAllOrbitMoment_eq_distinctHinge,
213 m2TransportedAllOrbitMomentDistinctHinge_smul,
214 m2MeanLocalAllOrbitMoment_eq_distinctHinge]
215
216/-! ## §3. Position-resolved Path B (t11 seed geometry) -/
217
218/-- Cube translate of a `(1,1)` star member as an ℝ⁴ lattice offset. -/
219def cubeTranslateOffset : CubeTranslate → (Fin 4 → ℝ)
220 | .origin => fun _ => 0
221 | .minusE2 => fun i => if i = 2 then (-1 : ℝ) else 0
222 | .minusE3 => fun i => if i = 3 then (-1 : ℝ) else 0
223 | .minusE2E3 => fun i =>
224 if i = 2 then (-1 : ℝ) else if i = 3 then (-1 : ℝ) else 0
225
226/-- Seed-frame offsets for the six `(1,1)` star members, in
227`starMembers` / `assembleStarMember` order. -/
228def t11MemberOffset : Fin 6 → (Fin 4 → ℝ)
229 | 0 | 1 => cubeTranslateOffset .origin
230 | 2 => cubeTranslateOffset .minusE2
231 | 3 => cubeTranslateOffset .minusE3
232 | 4 | 5 => cubeTranslateOffset .minusE2E3
233
234def addBase (x δ : Fin 4 → ℝ) : Fin 4 → ℝ := fun i => x i + δ i
235
236/-- Pushforward of one `(1,1)` star-member local kernel. -/
237def transportedT11Member (m : Fin 6) (p : Fin 24) : Fin 15 → ℝ :=
238 pushforwardClass (ReggeHinge4DStarKernel.assembleStarMember m) p
239
240/-- Apply covering perm as an axis permutation of a seed-frame offset.
241`coordPermOf p` maps seed axis `i` to world axis `(coordPermOf p) i`. -/
242def permOffset (p : Fin 24) (δ : Fin 4 → ℝ) : Fin 4 → ℝ :=
243 fun j => ∑ i : Fin 4, if coordPermOf p i = j then δ i else 0
244
245/-- Position-resolved deficit phased class-dot for type `(1,1)`:
246`Σ_m K_m` at `base + perm(offset_m)`. -/
247def phasedT11PositionResolved (H : Mat4) (mvec : Fin 4 → ℝ)
248 (s : Fin 24) (t : Fin 10) : ℝ :=
249 let p := orbitCoveringPerm .t11 s t
250 let base := hingeBase s t
251 ∑ mem : Fin 6,
252 phasedClassDot (transportedT11Member mem p) H mvec
253 (addBase base (permOffset p (t11MemberOffset mem)))
254
255/-- Position-resolved t11 slot term (area at hinge base). -/
256def t11PositionResolvedSlotTerm (H : Mat4) (mvec : Fin 4 → ℝ)
257 (s : Fin 24) (t : Fin 10) : ℝ :=
258 if isOrbit .t11 s t then
259 phasedClassDot (slotOrbitAreaCov .t11 s t) H mvec (hingeBase s t) *
260 phasedT11PositionResolved H mvec s t
261 else 0
262
263/-- Star assembly identity: Σ_m assembleStarMember = fullStar. -/
264theorem t11_member_sum_eq_fullStar (d : Fin 15) :
265 (∑ mem : Fin 6, ReggeHinge4DStarKernel.assembleStarMember mem d) =
266 ReggeHinge4DStarKernel.fullStarClassKernel d := by
267 simpa [ReggeHinge4DStarKernel.fullStarClassKernelAssembled] using
268 ReggeHinge4DStarKernel.fullStarClassKernel_eq d
269
270/-! ## §4. Status / OPEN obligations -/
271
272/-- **OPEN**: all-orbit position-resolved Path B equals (or repairs) the
273distinct-hinge continuum TT symbol. MEASURED counterexample on t12
274cross (receipt): symbolDir plus/cross agreement breaks; EH face not hit. -/
275def Regge4DPathBPositionResolvedClosesEH : Prop :=
276 False
277
278theorem Regge4DPathBPositionResolvedClosesEH_status_open :
279 Regge4DPathBPositionResolvedClosesEH = False :=
280 rfl
281
282/-- Vacuous mean-local Path B cannot repair e0 anisotropy / factor 4,
283because it equals distinct-hinge. -/
284theorem meanLocal_inherits_distinctHinge_on_any (H : Mat4)
285 (dir : Fin 4 → ℝ) :
286 m2MeanLocalAllOrbitMoment H dir =
287 m2TransportedAllOrbitMomentDistinctHinge H dir :=
288 m2MeanLocalAllOrbitMoment_eq_distinctHinge H dir
289
290structure ReggeBlochLocalIncidence4DStatus where
291 meanLocalEqualsDistinctHinge : Bool
292 positionResolvedT11Defined : Bool
293 pathBClosesEH : Bool
294 gapActionRecovery : Bool
295
296def reggeBlochLocalIncidence4DStatus : ReggeBlochLocalIncidence4DStatus where
297 meanLocalEqualsDistinctHinge := true
298 positionResolvedT11Defined := true
299 pathBClosesEH := false
300 gapActionRecovery := false
301
302theorem reggeBlochLocalIncidence4DStatus_flags :
303 reggeBlochLocalIncidence4DStatus.meanLocalEqualsDistinctHinge = true ∧
304 reggeBlochLocalIncidence4DStatus.positionResolvedT11Defined = true ∧
305 reggeBlochLocalIncidence4DStatus.pathBClosesEH = false ∧
306 reggeBlochLocalIncidence4DStatus.gapActionRecovery = false := by
307 decide
308
309theorem does_not_flip_gap_action_recovery :
310 reggeBlochLocalIncidence4DStatus.gapActionRecovery = false :=
311 rfl
312
313end
314
315end ReggeBlochLocalIncidence4D
316end Analysis
317end Gravity
318end IndisputableMonolith
319