Encyclopedia Gravity Gravity Analysis Regge Exact Midpoint M2 Ttidentity4 Dkernel Cert Coupling Zlist
ARTICLE 5 claims 4 theorems 1 model
Gravity Analysis Regge Exact Midpoint M2 Ttidentity4 Dkernel Cert Coupling Zlist
A formal proof that two ways of writing the same gravitational calculation agree exactly, checked step by step by a machine.
A machine-checked bridge
In numerical work, a calculation can be written two ways: one that is easy to read, and one that is fast for a computer to run. The declaration couplingZList_bridge is a machine-checked guarantee that these two versions of a particular gravitational expression produce identical results. The expression lives in a four-dimensional model of gravity, where the calculation concerns a quantity called the midpoint m² TT identity. The proof is a bridge: it connects the readable form, called couplingChunk, to a compact form, called czChunk, and shows that every entry in one matches the corresponding entry in the other.
The check is exhaustive. The calculation is split into sixteen chunks, numbered from zero to fifteen. For each chunk, a separate theorem states that the readable list, after a conversion step, equals the compact list. Each of these sixteen theorems is proved by a command called decide, which asks the machine to evaluate both sides and confirm they match. The proof does not rely on a fast but untrusted evaluator; it uses only the kernel's own decision procedure. The declaration explicitZ provides the full expression in six indices, and a further theorem, symFullZ_explicit_eq_closed, confirms that this explicit form agrees with a closed form under a symmetry operation.
In Recognition Science, this certificate is part of a larger pattern. The framework's machine-checked library of formal theorems treats numerical identities as objects that can be verified rather than assumed. This particular certificate does not derive any new physics. It does not prove that the midpoint m² TT identity is true; it proves that two implementations of it agree. The identity itself, and the physical meaning of the coupling, are separate matters. What the bridge establishes is a precise, mechanical fact: the readable and compact forms are the same list of integers, chunk by chunk.
The practical consequence is trust. When a calculation is translated into a faster form, errors can creep in. A machine-checked bridge removes that class of error. It means the compact version can be used with confidence wherever the readable version would be correct. This is a narrow but solid result: it does not extend to other identities, other dimensions, or other models. It covers exactly the sixteen chunks and the explicit-to-closed symmetry statement, and it covers them completely.
THEOREM czChunk0_bridge · czChunk1_bridge · czChunk2_bridge · czChunk3_bridge · czChunk4_bridge · czChunk5_bridge · czChunk6_bridge · czChunk7_bridge · czChunk8_bridge · czChunk9_bridge · czChunk10_bridge · czChunk11_bridge · czChunk12_bridge · czChunk13_bridge · czChunk14_bridge · czChunk15_bridge · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.lean
theorem czChunk0_bridge :
couplingChunk0.toList.map toCZ = czChunk0 := by
decide
theorem czChunk1_bridge :
couplingChunk1.toList.map toCZ = czChunk1 := by
decide
theorem czChunk2_bridge :
couplingChunk2.toList.map toCZ = czChunk2 := by
decide
theorem czChunk3_bridge :
couplingChunk3.toList.map toCZ = czChunk3 := by
decide
theorem czChunk4_bridge :
couplingChunk4.toList.map toCZ = czChunk4 := by
decide
theorem czChunk5_bridge :
couplingChunk5.toList.map toCZ = czChunk5 := by
decide
theorem czChunk6_bridge :
couplingChunk6.toList.map toCZ = czChunk6 := by
decide
theorem czChunk7_bridge :
couplingChunk7.toList.map toCZ = czChunk7 := by
decide
theorem czChunk8_bridge :
couplingChunk8.toList.map toCZ = czChunk8 := by
decide
theorem czChunk9_bridge :
couplingChunk9.toList.map toCZ = czChunk9 := by
decide
theorem czChunk10_bridge :
couplingChunk10.toList.map toCZ = czChunk10 := by
decide
theorem czChunk11_bridge :
couplingChunk11.toList.map toCZ = czChunk11 := by
decide
theorem czChunk12_bridge :
couplingChunk12.toList.map toCZ = czChunk12 := by
decide
theorem czChunk13_bridge :
couplingChunk13.toList.map toCZ = czChunk13 := by
decide
theorem czChunk14_bridge :
couplingChunk14.toList.map toCZ = czChunk14 := by
decide
theorem czChunk15_bridge :
couplingChunk15.toList.map toCZ = czChunk15 := by
decide
THEOREM czChunk0_bridge · czChunk1_bridge · czChunk2_bridge · czChunk3_bridge · czChunk4_bridge · czChunk5_bridge · czChunk6_bridge · czChunk7_bridge · czChunk8_bridge · czChunk9_bridge · czChunk10_bridge · czChunk11_bridge · czChunk12_bridge · czChunk13_bridge · czChunk14_bridge · czChunk15_bridge · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.lean
theorem czChunk0_bridge :
couplingChunk0.toList.map toCZ = czChunk0 := by
decide
theorem czChunk1_bridge :
couplingChunk1.toList.map toCZ = czChunk1 := by
decide
theorem czChunk2_bridge :
couplingChunk2.toList.map toCZ = czChunk2 := by
decide
theorem czChunk3_bridge :
couplingChunk3.toList.map toCZ = czChunk3 := by
decide
theorem czChunk4_bridge :
couplingChunk4.toList.map toCZ = czChunk4 := by
decide
theorem czChunk5_bridge :
couplingChunk5.toList.map toCZ = czChunk5 := by
decide
theorem czChunk6_bridge :
couplingChunk6.toList.map toCZ = czChunk6 := by
decide
theorem czChunk7_bridge :
couplingChunk7.toList.map toCZ = czChunk7 := by
decide
theorem czChunk8_bridge :
couplingChunk8.toList.map toCZ = czChunk8 := by
decide
theorem czChunk9_bridge :
couplingChunk9.toList.map toCZ = czChunk9 := by
decide
theorem czChunk10_bridge :
couplingChunk10.toList.map toCZ = czChunk10 := by
decide
theorem czChunk11_bridge :
couplingChunk11.toList.map toCZ = czChunk11 := by
decide
theorem czChunk12_bridge :
couplingChunk12.toList.map toCZ = czChunk12 := by
decide
theorem czChunk13_bridge :
couplingChunk13.toList.map toCZ = czChunk13 := by
decide
theorem czChunk14_bridge :
couplingChunk14.toList.map toCZ = czChunk14 := by
decide
theorem czChunk15_bridge :
couplingChunk15.toList.map toCZ = czChunk15 := by
decide
THEOREM czChunk0_bridge · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.lean
theorem czChunk0_bridge :
couplingChunk0.toList.map toCZ = czChunk0 := by
decide
THEOREM symFullZ_explicit_eq_closed · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.lean
theorem symFullZ_explicit_eq_closed :
∀ a b c d i j : Fin 4,
symFullZ explicitZ a b c d i j = symFullZ closedZ a b c d i j := by
decide
MODEL explicitZ · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.lean
def explicitZ : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Int
| 0, 0, 1, 1, 2, 2 => (4 : Int)
| 0, 0, 1, 1, 3, 3 => (4 : Int)
| 0, 0, 1, 2, 1, 2 => (-2 : Int)
| 0, 0, 1, 2, 2, 1 => (-2 : Int)
| 0, 0, 1, 3, 1, 3 => (-2 : Int)
| 0, 0, 1, 3, 3, 1 => (-2 : Int)
| 0, 0, 2, 1, 1, 2 => (-2 : Int)
| 0, 0, 2, 1, 2, 1 => (-2 : Int)
| 0, 0, 2, 2, 1, 1 => (4 : Int)
| 0, 0, 2, 2, 3, 3 => (4 : Int)
| 0, 0, 2, 3, 2, 3 => (-2 : Int)
| 0, 0, 2, 3, 3, 2 => (-2 : Int)
| 0, 0, 3, 1, 1, 3 => (-2 : Int)
| 0, 0, 3, 1, 3, 1 => (-2 : Int)
| 0, 0, 3, 2, 2, 3 => (-2 : Int)
| 0, 0, 3, 2, 3, 2 => (-2 : Int)
| 0, 0, 3, 3, 1, 1 => (4 : Int)
| 0, 0, 3, 3, 2, 2 => (4 : Int)
| 0, 1, 0, 1, 2, 2 => (-2 : Int)
| 0, 1, 0, 1, 3, 3 => (-2 : Int)
| 0, 1, 0, 2, 1, 2 => (1 : Int)
| 0, 1, 0, 2, 2, 1 => (1 : Int)
| 0, 1, 0, 3, 1, 3 => (1 : Int)
| 0, 1, 0, 3, 3, 1 => (1 : Int)
| 0, 1, 1, 0, 2, 2 => (-2 : Int)
| 0, 1, 1, 0, 3, 3 => (-2 : Int)
| 0, 1, 1, 2, 0, 2 => (1 : Int)
| 0, 1, 1, 2, 2, 0 => (1 : Int)
| 0, 1, 1, 3, 0, 3 => (1 : Int)
| 0, 1, 1, 3, 3, 0 => (1 : Int)
| 0, 1, 2, 0, 1, 2 => (1 : Int)
| 0, 1, 2, 0, 2, 1 => (1 : Int)
| 0, 1, 2, 1, 0, 2 => (1 : Int)
| 0, 1, 2, 1, 2, 0 => (1 : Int)
| 0, 1, 2, 2, 0, 1 => (-2 : Int)
| 0, 1, 2, 2, 1, 0 => (-2 : Int)
| 0, 1, 3, 0, 1, 3 => (1 : Int)
| 0, 1, 3, 0, 3, 1 => (1 : Int)
| 0, 1, 3, 1, 0, 3 => (1 : Int)
| 0, 1, 3, 1, 3, 0 => (1 : Int)
| 0, 1, 3, 3, 0, 1 => (-2 : Int)
| 0, 1, 3, 3, 1, 0 => (-2 : Int)
| 0, 2, 0, 1, 1, 2 => (1 : Int)
| 0, 2, 0, 1, 2, 1 => (1 : Int)
| 0, 2, 0, 2, 1, 1 => (-2 : Int)
| 0, 2, 0, 2, 3, 3 => (-2 : Int)
| 0, 2, 0, 3, 2, 3 => (1 : Int)
| 0, 2, 0, 3, 3, 2 => (1 : Int)
| 0, 2, 1, 0, 1, 2 => (1 : Int)
| 0, 2, 1, 0, 2, 1 => (1 : Int)
| 0, 2, 1, 1, 0, 2 => (-2 : Int)
| 0, 2, 1, 1, 2, 0 => (-2 : Int)
| 0, 2, 1, 2, 0, 1 => (1 : Int)
| 0, 2, 1, 2, 1, 0 => (1 : Int)
| 0, 2, 2, 0, 1, 1 => (-2 : Int)
| 0, 2, 2, 0, 3, 3 => (-2 : Int)
| 0, 2, 2, 1, 0, 1 => (1 : Int)
| 0, 2, 2, 1, 1, 0 => (1 : Int)
| 0, 2, 2, 3, 0, 3 => (1 : Int)
| 0, 2, 2, 3, 3, 0 => (1 : Int)
| 0, 2, 3, 0, 2, 3 => (1 : Int)
| 0, 2, 3, 0, 3, 2 => (1 : Int)
| 0, 2, 3, 2, 0, 3 => (1 : Int)
| 0, 2, 3, 2, 3, 0 => (1 : Int)
| 0, 2, 3, 3, 0, 2 => (-2 : Int)
| 0, 2, 3, 3, 2, 0 => (-2 : Int)
| 0, 3, 0, 1, 1, 3 => (1 : Int)
| 0, 3, 0, 1, 3, 1 => (1 : Int)
| 0, 3, 0, 2, 2, 3 => (1 : Int)
| 0, 3, 0, 2, 3, 2 => (1 : Int)
| 0, 3, 0, 3, 1, 1 => (-2 : Int)
| 0, 3, 0, 3, 2, 2 => (-2 : Int)
| 0, 3, 1, 0, 1, 3 => (1 : Int)
| 0, 3, 1, 0, 3, 1 => (1 : Int)
| 0, 3, 1, 1, 0, 3 => (-2 : Int)
| 0, 3, 1, 1, 3, 0 => (-2 : Int)
| 0, 3, 1, 3, 0, 1 => (1 : Int)
| 0, 3, 1, 3, 1, 0 => (1 : Int)
| 0, 3, 2, 0, 2, 3 => (1 : Int)
| 0, 3, 2, 0, 3, 2 => (1 : Int)
| 0, 3, 2, 2, 0, 3 => (-2 : Int)
| 0, 3, 2, 2, 3, 0 => (-2 : Int)
| 0, 3, 2, 3, 0, 2 => (1 : Int)
| 0, 3, 2, 3, 2, 0 => (1 : Int)
| 0, 3, 3, 0, 1, 1 => (-2 : Int)
| 0, 3, 3, 0, 2, 2 => (-2 : Int)
| 0, 3, 3, 1, 0, 1 => (1 : Int)
| 0, 3, 3, 1, 1, 0 => (1 : Int)
| 0, 3, 3, 2, 0, 2 => (1 : Int)
| 0, 3, 3, 2, 2, 0 => (1 : Int)
| 1, 0, 0, 1, 2, 2 => (-2 : Int)
| 1, 0, 0, 1, 3, 3 => (-2 : Int)
| 1, 0, 0, 2, 1, 2 => (1 : Int)
| 1, 0, 0, 2, 2, 1 => (1 : Int)
| 1, 0, 0, 3, 1, 3 => (1 : Int)
| 1, 0, 0, 3, 3, 1 => (1 : Int)
| 1, 0, 1, 0, 2, 2 => (-2 : Int)
| 1, 0, 1, 0, 3, 3 => (-2 : Int)
| 1, 0, 1, 2, 0, 2 => (1 : Int)
| 1, 0, 1, 2, 2, 0 => (1 : Int)
| 1, 0, 1, 3, 0, 3 => (1 : Int)
| 1, 0, 1, 3, 3, 0 => (1 : Int)
| 1, 0, 2, 0, 1, 2 => (1 : Int)
| 1, 0, 2, 0, 2, 1 => (1 : Int)
| 1, 0, 2, 1, 0, 2 => (1 : Int)
| 1, 0, 2, 1, 2, 0 => (1 : Int)
| 1, 0, 2, 2, 0, 1 => (-2 : Int)
| 1, 0, 2, 2, 1, 0 => (-2 : Int)
| 1, 0, 3, 0, 1, 3 => (1 : Int)
| 1, 0, 3, 0, 3, 1 => (1 : Int)
| 1, 0, 3, 1, 0, 3 => (1 : Int)
| 1, 0, 3, 1, 3, 0 => (1 : Int)
| 1, 0, 3, 3, 0, 1 => (-2 : Int)
| 1, 0, 3, 3, 1, 0 => (-2 : Int)
| 1, 1, 0, 0, 2, 2 => (4 : Int)
| 1, 1, 0, 0, 3, 3 => (4 : Int)
| 1, 1, 0, 2, 0, 2 => (-2 : Int)
| 1, 1, 0, 2, 2, 0 => (-2 : Int)
| 1, 1, 0, 3, 0, 3 => (-2 : Int)
| 1, 1, 0, 3, 3, 0 => (-2 : Int)
| 1, 1, 2, 0, 0, 2 => (-2 : Int)
| 1, 1, 2, 0, 2, 0 => (-2 : Int)
| 1, 1, 2, 2, 0, 0 => (4 : Int)
| 1, 1, 2, 2, 3, 3 => (4 : Int)
| 1, 1, 2, 3, 2, 3 => (-2 : Int)
| 1, 1, 2, 3, 3, 2 => (-2 : Int)
| 1, 1, 3, 0, 0, 3 => (-2 : Int)
| 1, 1, 3, 0, 3, 0 => (-2 : Int)
| 1, 1, 3, 2, 2, 3 => (-2 : Int)
| 1, 1, 3, 2, 3, 2 => (-2 : Int)
| 1, 1, 3, 3, 0, 0 => (4 : Int)
| 1, 1, 3, 3, 2, 2 => (4 : Int)
| 1, 2, 0, 0, 1, 2 => (-2 : Int)
| 1, 2, 0, 0, 2, 1 => (-2 : Int)
| 1, 2, 0, 1, 0, 2 => (1 : Int)
| 1, 2, 0, 1, 2, 0 => (1 : Int)
| 1, 2, 0, 2, 0, 1 => (1 : Int)
| 1, 2, 0, 2, 1, 0 => (1 : Int)
| 1, 2, 1, 0, 0, 2 => (1 : Int)
| 1, 2, 1, 0, 2, 0 => (1 : Int)
| 1, 2, 1, 2, 0, 0 => (-2 : Int)
| 1, 2, 1, 2, 3, 3 => (-2 : Int)
| 1, 2, 1, 3, 2, 3 => (1 : Int)
| 1, 2, 1, 3, 3, 2 => (1 : Int)
| 1, 2, 2, 0, 0, 1 => (1 : Int)
| 1, 2, 2, 0, 1, 0 => (1 : Int)
| 1, 2, 2, 1, 0, 0 => (-2 : Int)
| 1, 2, 2, 1, 3, 3 => (-2 : Int)
| 1, 2, 2, 3, 1, 3 => (1 : Int)
| 1, 2, 2, 3, 3, 1 => (1 : Int)
| 1, 2, 3, 1, 2, 3 => (1 : Int)
| 1, 2, 3, 1, 3, 2 => (1 : Int)
| 1, 2, 3, 2, 1, 3 => (1 : Int)
| 1, 2, 3, 2, 3, 1 => (1 : Int)
| 1, 2, 3, 3, 1, 2 => (-2 : Int)
| 1, 2, 3, 3, 2, 1 => (-2 : Int)
| 1, 3, 0, 0, 1, 3 => (-2 : Int)
| 1, 3, 0, 0, 3, 1 => (-2 : Int)
| 1, 3, 0, 1, 0, 3 => (1 : Int)
| 1, 3, 0, 1, 3, 0 => (1 : Int)
| 1, 3, 0, 3, 0, 1 => (1 : Int)
| 1, 3, 0, 3, 1, 0 => (1 : Int)
| 1, 3, 1, 0, 0, 3 => (1 : Int)
| 1, 3, 1, 0, 3, 0 => (1 : Int)
| 1, 3, 1, 2, 2, 3 => (1 : Int)
| 1, 3, 1, 2, 3, 2 => (1 : Int)
| 1, 3, 1, 3, 0, 0 => (-2 : Int)
| 1, 3, 1, 3, 2, 2 => (-2 : Int)
| 1, 3, 2, 1, 2, 3 => (1 : Int)
| 1, 3, 2, 1, 3, 2 => (1 : Int)
| 1, 3, 2, 2, 1, 3 => (-2 : Int)
| 1, 3, 2, 2, 3, 1 => (-2 : Int)
| 1, 3, 2, 3, 1, 2 => (1 : Int)
| 1, 3, 2, 3, 2, 1 => (1 : Int)
| 1, 3, 3, 0, 0, 1 => (1 : Int)
| 1, 3, 3, 0, 1, 0 => (1 : Int)
| 1, 3, 3, 1, 0, 0 => (-2 : Int)
| 1, 3, 3, 1, 2, 2 => (-2 : Int)
| 1, 3, 3, 2, 1, 2 => (1 : Int)
| 1, 3, 3, 2, 2, 1 => (1 : Int)
| 2, 0, 0, 1, 1, 2 => (1 : Int)
| 2, 0, 0, 1, 2, 1 => (1 : Int)
| 2, 0, 0, 2, 1, 1 => (-2 : Int)
| 2, 0, 0, 2, 3, 3 => (-2 : Int)
| 2, 0, 0, 3, 2, 3 => (1 : Int)
| 2, 0, 0, 3, 3, 2 => (1 : Int)
| 2, 0, 1, 0, 1, 2 => (1 : Int)
| 2, 0, 1, 0, 2, 1 => (1 : Int)
| 2, 0, 1, 1, 0, 2 => (-2 : Int)
| 2, 0, 1, 1, 2, 0 => (-2 : Int)
| 2, 0, 1, 2, 0, 1 => (1 : Int)
| 2, 0, 1, 2, 1, 0 => (1 : Int)
| 2, 0, 2, 0, 1, 1 => (-2 : Int)
| 2, 0, 2, 0, 3, 3 => (-2 : Int)
| 2, 0, 2, 1, 0, 1 => (1 : Int)
| 2, 0, 2, 1, 1, 0 => (1 : Int)
| 2, 0, 2, 3, 0, 3 => (1 : Int)
| 2, 0, 2, 3, 3, 0 => (1 : Int)
| 2, 0, 3, 0, 2, 3 => (1 : Int)
| 2, 0, 3, 0, 3, 2 => (1 : Int)
| 2, 0, 3, 2, 0, 3 => (1 : Int)
| 2, 0, 3, 2, 3, 0 => (1 : Int)
| 2, 0, 3, 3, 0, 2 => (-2 : Int)
| 2, 0, 3, 3, 2, 0 => (-2 : Int)
| 2, 1, 0, 0, 1, 2 => (-2 : Int)
| 2, 1, 0, 0, 2, 1 => (-2 : Int)
| 2, 1, 0, 1, 0, 2 => (1 : Int)
| 2, 1, 0, 1, 2, 0 => (1 : Int)
| 2, 1, 0, 2, 0, 1 => (1 : Int)
| 2, 1, 0, 2, 1, 0 => (1 : Int)
| 2, 1, 1, 0, 0, 2 => (1 : Int)
| 2, 1, 1, 0, 2, 0 => (1 : Int)
| 2, 1, 1, 2, 0, 0 => (-2 : Int)
| 2, 1, 1, 2, 3, 3 => (-2 : Int)
| 2, 1, 1, 3, 2, 3 => (1 : Int)
| 2, 1, 1, 3, 3, 2 => (1 : Int)
| 2, 1, 2, 0, 0, 1 => (1 : Int)
| 2, 1, 2, 0, 1, 0 => (1 : Int)
| 2, 1, 2, 1, 0, 0 => (-2 : Int)
| 2, 1, 2, 1, 3, 3 => (-2 : Int)
| 2, 1, 2, 3, 1, 3 => (1 : Int)
| 2, 1, 2, 3, 3, 1 => (1 : Int)
| 2, 1, 3, 1, 2, 3 => (1 : Int)
| 2, 1, 3, 1, 3, 2 => (1 : Int)
| 2, 1, 3, 2, 1, 3 => (1 : Int)
| 2, 1, 3, 2, 3, 1 => (1 : Int)
| 2, 1, 3, 3, 1, 2 => (-2 : Int)
| 2, 1, 3, 3, 2, 1 => (-2 : Int)
| 2, 2, 0, 0, 1, 1 => (4 : Int)
| 2, 2, 0, 0, 3, 3 => (4 : Int)
| 2, 2, 0, 1, 0, 1 => (-2 : Int)
| 2, 2, 0, 1, 1, 0 => (-2 : Int)
| 2, 2, 0, 3, 0, 3 => (-2 : Int)
| 2, 2, 0, 3, 3, 0 => (-2 : Int)
| 2, 2, 1, 0, 0, 1 => (-2 : Int)
| 2, 2, 1, 0, 1, 0 => (-2 : Int)
| 2, 2, 1, 1, 0, 0 => (4 : Int)
| 2, 2, 1, 1, 3, 3 => (4 : Int)
| 2, 2, 1, 3, 1, 3 => (-2 : Int)
| 2, 2, 1, 3, 3, 1 => (-2 : Int)
| 2, 2, 3, 0, 0, 3 => (-2 : Int)
| 2, 2, 3, 0, 3, 0 => (-2 : Int)
| 2, 2, 3, 1, 1, 3 => (-2 : Int)
| 2, 2, 3, 1, 3, 1 => (-2 : Int)
| 2, 2, 3, 3, 0, 0 => (4 : Int)
| 2, 2, 3, 3, 1, 1 => (4 : Int)
| 2, 3, 0, 0, 2, 3 => (-2 : Int)
| 2, 3, 0, 0, 3, 2 => (-2 : Int)
| 2, 3, 0, 2, 0, 3 => (1 : Int)
| 2, 3, 0, 2, 3, 0 => (1 : Int)
| 2, 3, 0, 3, 0, 2 => (1 : Int)
| 2, 3, 0, 3, 2, 0 => (1 : Int)
| 2, 3, 1, 1, 2, 3 => (-2 : Int)
| 2, 3, 1, 1, 3, 2 => (-2 : Int)
| 2, 3, 1, 2, 1, 3 => (1 : Int)
| 2, 3, 1, 2, 3, 1 => (1 : Int)
| 2, 3, 1, 3, 1, 2 => (1 : Int)
| 2, 3, 1, 3, 2, 1 => (1 : Int)
| 2, 3, 2, 0, 0, 3 => (1 : Int)
| 2, 3, 2, 0, 3, 0 => (1 : Int)
| 2, 3, 2, 1, 1, 3 => (1 : Int)
| 2, 3, 2, 1, 3, 1 => (1 : Int)
| 2, 3, 2, 3, 0, 0 => (-2 : Int)
| 2, 3, 2, 3, 1, 1 => (-2 : Int)
| 2, 3, 3, 0, 0, 2 => (1 : Int)
| 2, 3, 3, 0, 2, 0 => (1 : Int)
| 2, 3, 3, 1, 1, 2 => (1 : Int)
| 2, 3, 3, 1, 2, 1 => (1 : Int)
| 2, 3, 3, 2, 0, 0 => (-2 : Int)
| 2, 3, 3, 2, 1, 1 => (-2 : Int)
| 3, 0, 0, 1, 1, 3 => (1 : Int)
| 3, 0, 0, 1, 3, 1 => (1 : Int)
| 3, 0, 0, 2, 2, 3 => (1 : Int)
| 3, 0, 0, 2, 3, 2 => (1 : Int)
| 3, 0, 0, 3, 1, 1 => (-2 : Int)
| 3, 0, 0, 3, 2, 2 => (-2 : Int)
| 3, 0, 1, 0, 1, 3 => (1 : Int)
| 3, 0, 1, 0, 3, 1 => (1 : Int)
| 3, 0, 1, 1, 0, 3 => (-2 : Int)
| 3, 0, 1, 1, 3, 0 => (-2 : Int)
| 3, 0, 1, 3, 0, 1 => (1 : Int)
| 3, 0, 1, 3, 1, 0 => (1 : Int)
| 3, 0, 2, 0, 2, 3 => (1 : Int)
| 3, 0, 2, 0, 3, 2 => (1 : Int)
| 3, 0, 2, 2, 0, 3 => (-2 : Int)
| 3, 0, 2, 2, 3, 0 => (-2 : Int)
| 3, 0, 2, 3, 0, 2 => (1 : Int)
| 3, 0, 2, 3, 2, 0 => (1 : Int)
| 3, 0, 3, 0, 1, 1 => (-2 : Int)
| 3, 0, 3, 0, 2, 2 => (-2 : Int)
| 3, 0, 3, 1, 0, 1 => (1 : Int)
| 3, 0, 3, 1, 1, 0 => (1 : Int)
| 3, 0, 3, 2, 0, 2 => (1 : Int)
| 3, 0, 3, 2, 2, 0 => (1 : Int)
| 3, 1, 0, 0, 1, 3 => (-2 : Int)
| 3, 1, 0, 0, 3, 1 => (-2 : Int)
| 3, 1, 0, 1, 0, 3 => (1 : Int)
| 3, 1, 0, 1, 3, 0 => (1 : Int)
| 3, 1, 0, 3, 0, 1 => (1 : Int)
| 3, 1, 0, 3, 1, 0 => (1 : Int)
| 3, 1, 1, 0, 0, 3 => (1 : Int)
| 3, 1, 1, 0, 3, 0 => (1 : Int)
| 3, 1, 1, 2, 2, 3 => (1 : Int)
| 3, 1, 1, 2, 3, 2 => (1 : Int)
| 3, 1, 1, 3, 0, 0 => (-2 : Int)
| 3, 1, 1, 3, 2, 2 => (-2 : Int)
| 3, 1, 2, 1, 2, 3 => (1 : Int)
| 3, 1, 2, 1, 3, 2 => (1 : Int)
| 3, 1, 2, 2, 1, 3 => (-2 : Int)
| 3, 1, 2, 2, 3, 1 => (-2 : Int)
| 3, 1, 2, 3, 1, 2 => (1 : Int)
| 3, 1, 2, 3, 2, 1 => (1 : Int)
| 3, 1, 3, 0, 0, 1 => (1 : Int)
| 3, 1, 3, 0, 1, 0 => (1 : Int)
| 3, 1, 3, 1, 0, 0 => (-2 : Int)
| 3, 1, 3, 1, 2, 2 => (-2 : Int)
| 3, 1, 3, 2, 1, 2 => (1 : Int)
| 3, 1, 3, 2, 2, 1 => (1 : Int)
| 3, 2, 0, 0, 2, 3 => (-2 : Int)
| 3, 2, 0, 0, 3, 2 => (-2 : Int)
| 3, 2, 0, 2, 0, 3 => (1 : Int)
| 3, 2, 0, 2, 3, 0 => (1 : Int)
| 3, 2, 0, 3, 0, 2 => (1 : Int)
| 3, 2, 0, 3, 2, 0 => (1 : Int)
| 3, 2, 1, 1, 2, 3 => (-2 : Int)
| 3, 2, 1, 1, 3, 2 => (-2 : Int)
| 3, 2, 1, 2, 1, 3 => (1 : Int)
| 3, 2, 1, 2, 3, 1 => (1 : Int)
| 3, 2, 1, 3, 1, 2 => (1 : Int)
| 3, 2, 1, 3, 2, 1 => (1 : Int)
| 3, 2, 2, 0, 0, 3 => (1 : Int)
| 3, 2, 2, 0, 3, 0 => (1 : Int)
| 3, 2, 2, 1, 1, 3 => (1 : Int)
| 3, 2, 2, 1, 3, 1 => (1 : Int)
| 3, 2, 2, 3, 0, 0 => (-2 : Int)
| 3, 2, 2, 3, 1, 1 => (-2 : Int)
| 3, 2, 3, 0, 0, 2 => (1 : Int)
| 3, 2, 3, 0, 2, 0 => (1 : Int)
| 3, 2, 3, 1, 1, 2 => (1 : Int)
| 3, 2, 3, 1, 2, 1 => (1 : Int)
| 3, 2, 3, 2, 0, 0 => (-2 : Int)
| 3, 2, 3, 2, 1, 1 => (-2 : Int)
| 3, 3, 0, 0, 1, 1 => (4 : Int)
| 3, 3, 0, 0, 2, 2 => (4 : Int)
| 3, 3, 0, 1, 0, 1 => (-2 : Int)
| 3, 3, 0, 1, 1, 0 => (-2 : Int)
| 3, 3, 0, 2, 0, 2 => (-2 : Int)
-- … truncated for the page; open the module for the rest.
What this page does not claim
No claim that the midpoint m² TT identity itself is physically true or derived from the framework's axioms. No claim that the bridge extends to identities outside the sixteen chunks listed. No claim that the compact form is faster or more efficient than the readable form.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What physical content does the midpoint m² TT identity carry in the four-dimensional gravity model?
- How does the compact czChunk representation relate to the readable couplingChunk form beyond the integer lists?
- What role does the symmetry operation in symFullZ play in the wider gravitational analysis?
- How are the sixteen chunks assembled into the full couplingZList used by m2Num?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM czChunk0_bridge · czChunk1_bridge · czChunk2_bridge · czChunk3_bridge · czChunk4_bridge · czChunk5_bridge · czChunk6_bridge · czChunk7_bridge · czChunk8_bridge · czChunk9_bridge · czChunk10_bridge · czChunk11_bridge · czChunk12_bridge · czChunk13_bridge · czChunk14_bridge · czChunk15_bridge · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.lean
theorem czChunk0_bridge : couplingChunk0.toList.map toCZ = czChunk0 := by decidetheorem czChunk1_bridge : couplingChunk1.toList.map toCZ = czChunk1 := by decidetheorem czChunk2_bridge : couplingChunk2.toList.map toCZ = czChunk2 := by decidetheorem czChunk3_bridge : couplingChunk3.toList.map toCZ = czChunk3 := by decidetheorem czChunk4_bridge : couplingChunk4.toList.map toCZ = czChunk4 := by decidetheorem czChunk5_bridge : couplingChunk5.toList.map toCZ = czChunk5 := by decidetheorem czChunk6_bridge : couplingChunk6.toList.map toCZ = czChunk6 := by decidetheorem czChunk7_bridge : couplingChunk7.toList.map toCZ = czChunk7 := by decidetheorem czChunk8_bridge : couplingChunk8.toList.map toCZ = czChunk8 := by decidetheorem czChunk9_bridge : couplingChunk9.toList.map toCZ = czChunk9 := by decidetheorem czChunk10_bridge : couplingChunk10.toList.map toCZ = czChunk10 := by decidetheorem czChunk11_bridge : couplingChunk11.toList.map toCZ = czChunk11 := by decidetheorem czChunk12_bridge : couplingChunk12.toList.map toCZ = czChunk12 := by decidetheorem czChunk13_bridge : couplingChunk13.toList.map toCZ = czChunk13 := by decidetheorem czChunk14_bridge : couplingChunk14.toList.map toCZ = czChunk14 := by decidetheorem czChunk15_bridge : couplingChunk15.toList.map toCZ = czChunk15 := by decideThe declaration couplingZList_bridge is a machine-checked guarantee that two versions of a particular gravitational expression produce identical results. czChunk0_bridge · czChunk1_bridge · czChunk2_bridge · czChunk3_bridge · czChunk4_bridge · czChunk5_bridge · czChunk6_bridge · czChunk7_bridge · czChunk8_bridge · czChunk9_bridge · czChunk10_bridge · czChunk11_bridge · czChunk12_bridge · czChunk13_bridge · czChunk14_bridge · czChunk15_bridge · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.leanTHEOREM czChunk0_bridge · czChunk1_bridge · czChunk2_bridge · czChunk3_bridge · czChunk4_bridge · czChunk5_bridge · czChunk6_bridge · czChunk7_bridge · czChunk8_bridge · czChunk9_bridge · czChunk10_bridge · czChunk11_bridge · czChunk12_bridge · czChunk13_bridge · czChunk14_bridge · czChunk15_bridge · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.lean
theorem czChunk0_bridge : couplingChunk0.toList.map toCZ = czChunk0 := by decidetheorem czChunk1_bridge : couplingChunk1.toList.map toCZ = czChunk1 := by decidetheorem czChunk2_bridge : couplingChunk2.toList.map toCZ = czChunk2 := by decidetheorem czChunk3_bridge : couplingChunk3.toList.map toCZ = czChunk3 := by decidetheorem czChunk4_bridge : couplingChunk4.toList.map toCZ = czChunk4 := by decidetheorem czChunk5_bridge : couplingChunk5.toList.map toCZ = czChunk5 := by decidetheorem czChunk6_bridge : couplingChunk6.toList.map toCZ = czChunk6 := by decidetheorem czChunk7_bridge : couplingChunk7.toList.map toCZ = czChunk7 := by decidetheorem czChunk8_bridge : couplingChunk8.toList.map toCZ = czChunk8 := by decidetheorem czChunk9_bridge : couplingChunk9.toList.map toCZ = czChunk9 := by decidetheorem czChunk10_bridge : couplingChunk10.toList.map toCZ = czChunk10 := by decidetheorem czChunk11_bridge : couplingChunk11.toList.map toCZ = czChunk11 := by decidetheorem czChunk12_bridge : couplingChunk12.toList.map toCZ = czChunk12 := by decidetheorem czChunk13_bridge : couplingChunk13.toList.map toCZ = czChunk13 := by decidetheorem czChunk14_bridge : couplingChunk14.toList.map toCZ = czChunk14 := by decidetheorem czChunk15_bridge : couplingChunk15.toList.map toCZ = czChunk15 := by decideThe check is exhaustive. czChunk0_bridge · czChunk1_bridge · czChunk2_bridge · czChunk3_bridge · czChunk4_bridge · czChunk5_bridge · czChunk6_bridge · czChunk7_bridge · czChunk8_bridge · czChunk9_bridge · czChunk10_bridge · czChunk11_bridge · czChunk12_bridge · czChunk13_bridge · czChunk14_bridge · czChunk15_bridge · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.leanTHEOREM czChunk0_bridge · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.lean
theorem czChunk0_bridge : couplingChunk0.toList.map toCZ = czChunk0 := by decideThe proof does not rely on a fast but untrusted evaluator; it uses only the kernel's own decision procedure. czChunk0_bridge · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.leanTHEOREM symFullZ_explicit_eq_closed · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.lean
theorem symFullZ_explicit_eq_closed : ∀ a b c d i j : Fin 4, symFullZ explicitZ a b c d i j = symFullZ closedZ a b c d i j := by decideA further theorem, symFullZ_explicit_eq_closed, confirms that this explicit form agrees with a closed form under a symmetry operation. symFullZ_explicit_eq_closed · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.leanMODEL explicitZ · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.lean
def explicitZ : Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Fin 4 → Int | 0, 0, 1, 1, 2, 2 => (4 : Int) | 0, 0, 1, 1, 3, 3 => (4 : Int) | 0, 0, 1, 2, 1, 2 => (-2 : Int) | 0, 0, 1, 2, 2, 1 => (-2 : Int) | 0, 0, 1, 3, 1, 3 => (-2 : Int) | 0, 0, 1, 3, 3, 1 => (-2 : Int) | 0, 0, 2, 1, 1, 2 => (-2 : Int) | 0, 0, 2, 1, 2, 1 => (-2 : Int) | 0, 0, 2, 2, 1, 1 => (4 : Int) | 0, 0, 2, 2, 3, 3 => (4 : Int) | 0, 0, 2, 3, 2, 3 => (-2 : Int) | 0, 0, 2, 3, 3, 2 => (-2 : Int) | 0, 0, 3, 1, 1, 3 => (-2 : Int) | 0, 0, 3, 1, 3, 1 => (-2 : Int) | 0, 0, 3, 2, 2, 3 => (-2 : Int) | 0, 0, 3, 2, 3, 2 => (-2 : Int) | 0, 0, 3, 3, 1, 1 => (4 : Int) | 0, 0, 3, 3, 2, 2 => (4 : Int) | 0, 1, 0, 1, 2, 2 => (-2 : Int) | 0, 1, 0, 1, 3, 3 => (-2 : Int) | 0, 1, 0, 2, 1, 2 => (1 : Int) | 0, 1, 0, 2, 2, 1 => (1 : Int) | 0, 1, 0, 3, 1, 3 => (1 : Int) | 0, 1, 0, 3, 3, 1 => (1 : Int) | 0, 1, 1, 0, 2, 2 => (-2 : Int) | 0, 1, 1, 0, 3, 3 => (-2 : Int) | 0, 1, 1, 2, 0, 2 => (1 : Int) | 0, 1, 1, 2, 2, 0 => (1 : Int) | 0, 1, 1, 3, 0, 3 => (1 : Int) | 0, 1, 1, 3, 3, 0 => (1 : Int) | 0, 1, 2, 0, 1, 2 => (1 : Int) | 0, 1, 2, 0, 2, 1 => (1 : Int) | 0, 1, 2, 1, 0, 2 => (1 : Int) | 0, 1, 2, 1, 2, 0 => (1 : Int) | 0, 1, 2, 2, 0, 1 => (-2 : Int) | 0, 1, 2, 2, 1, 0 => (-2 : Int) | 0, 1, 3, 0, 1, 3 => (1 : Int) | 0, 1, 3, 0, 3, 1 => (1 : Int) | 0, 1, 3, 1, 0, 3 => (1 : Int) | 0, 1, 3, 1, 3, 0 => (1 : Int) | 0, 1, 3, 3, 0, 1 => (-2 : Int) | 0, 1, 3, 3, 1, 0 => (-2 : Int) | 0, 2, 0, 1, 1, 2 => (1 : Int) | 0, 2, 0, 1, 2, 1 => (1 : Int) | 0, 2, 0, 2, 1, 1 => (-2 : Int) | 0, 2, 0, 2, 3, 3 => (-2 : Int) | 0, 2, 0, 3, 2, 3 => (1 : Int) | 0, 2, 0, 3, 3, 2 => (1 : Int) | 0, 2, 1, 0, 1, 2 => (1 : Int) | 0, 2, 1, 0, 2, 1 => (1 : Int) | 0, 2, 1, 1, 0, 2 => (-2 : Int) | 0, 2, 1, 1, 2, 0 => (-2 : Int) | 0, 2, 1, 2, 0, 1 => (1 : Int) | 0, 2, 1, 2, 1, 0 => (1 : Int) | 0, 2, 2, 0, 1, 1 => (-2 : Int) | 0, 2, 2, 0, 3, 3 => (-2 : Int) | 0, 2, 2, 1, 0, 1 => (1 : Int) | 0, 2, 2, 1, 1, 0 => (1 : Int) | 0, 2, 2, 3, 0, 3 => (1 : Int) | 0, 2, 2, 3, 3, 0 => (1 : Int) | 0, 2, 3, 0, 2, 3 => (1 : Int) | 0, 2, 3, 0, 3, 2 => (1 : Int) | 0, 2, 3, 2, 0, 3 => (1 : Int) | 0, 2, 3, 2, 3, 0 => (1 : Int) | 0, 2, 3, 3, 0, 2 => (-2 : Int) | 0, 2, 3, 3, 2, 0 => (-2 : Int) | 0, 3, 0, 1, 1, 3 => (1 : Int) | 0, 3, 0, 1, 3, 1 => (1 : Int) | 0, 3, 0, 2, 2, 3 => (1 : Int) | 0, 3, 0, 2, 3, 2 => (1 : Int) | 0, 3, 0, 3, 1, 1 => (-2 : Int) | 0, 3, 0, 3, 2, 2 => (-2 : Int) | 0, 3, 1, 0, 1, 3 => (1 : Int) | 0, 3, 1, 0, 3, 1 => (1 : Int) | 0, 3, 1, 1, 0, 3 => (-2 : Int) | 0, 3, 1, 1, 3, 0 => (-2 : Int) | 0, 3, 1, 3, 0, 1 => (1 : Int) | 0, 3, 1, 3, 1, 0 => (1 : Int) | 0, 3, 2, 0, 2, 3 => (1 : Int) | 0, 3, 2, 0, 3, 2 => (1 : Int) | 0, 3, 2, 2, 0, 3 => (-2 : Int) | 0, 3, 2, 2, 3, 0 => (-2 : Int) | 0, 3, 2, 3, 0, 2 => (1 : Int) | 0, 3, 2, 3, 2, 0 => (1 : Int) | 0, 3, 3, 0, 1, 1 => (-2 : Int) | 0, 3, 3, 0, 2, 2 => (-2 : Int) | 0, 3, 3, 1, 0, 1 => (1 : Int) | 0, 3, 3, 1, 1, 0 => (1 : Int) | 0, 3, 3, 2, 0, 2 => (1 : Int) | 0, 3, 3, 2, 2, 0 => (1 : Int) | 1, 0, 0, 1, 2, 2 => (-2 : Int) | 1, 0, 0, 1, 3, 3 => (-2 : Int) | 1, 0, 0, 2, 1, 2 => (1 : Int) | 1, 0, 0, 2, 2, 1 => (1 : Int) | 1, 0, 0, 3, 1, 3 => (1 : Int) | 1, 0, 0, 3, 3, 1 => (1 : Int) | 1, 0, 1, 0, 2, 2 => (-2 : Int) | 1, 0, 1, 0, 3, 3 => (-2 : Int) | 1, 0, 1, 2, 0, 2 => (1 : Int) | 1, 0, 1, 2, 2, 0 => (1 : Int) | 1, 0, 1, 3, 0, 3 => (1 : Int) | 1, 0, 1, 3, 3, 0 => (1 : Int) | 1, 0, 2, 0, 1, 2 => (1 : Int) | 1, 0, 2, 0, 2, 1 => (1 : Int) | 1, 0, 2, 1, 0, 2 => (1 : Int) | 1, 0, 2, 1, 2, 0 => (1 : Int) | 1, 0, 2, 2, 0, 1 => (-2 : Int) | 1, 0, 2, 2, 1, 0 => (-2 : Int) | 1, 0, 3, 0, 1, 3 => (1 : Int) | 1, 0, 3, 0, 3, 1 => (1 : Int) | 1, 0, 3, 1, 0, 3 => (1 : Int) | 1, 0, 3, 1, 3, 0 => (1 : Int) | 1, 0, 3, 3, 0, 1 => (-2 : Int) | 1, 0, 3, 3, 1, 0 => (-2 : Int) | 1, 1, 0, 0, 2, 2 => (4 : Int) | 1, 1, 0, 0, 3, 3 => (4 : Int) | 1, 1, 0, 2, 0, 2 => (-2 : Int) | 1, 1, 0, 2, 2, 0 => (-2 : Int) | 1, 1, 0, 3, 0, 3 => (-2 : Int) | 1, 1, 0, 3, 3, 0 => (-2 : Int) | 1, 1, 2, 0, 0, 2 => (-2 : Int) | 1, 1, 2, 0, 2, 0 => (-2 : Int) | 1, 1, 2, 2, 0, 0 => (4 : Int) | 1, 1, 2, 2, 3, 3 => (4 : Int) | 1, 1, 2, 3, 2, 3 => (-2 : Int) | 1, 1, 2, 3, 3, 2 => (-2 : Int) | 1, 1, 3, 0, 0, 3 => (-2 : Int) | 1, 1, 3, 0, 3, 0 => (-2 : Int) | 1, 1, 3, 2, 2, 3 => (-2 : Int) | 1, 1, 3, 2, 3, 2 => (-2 : Int) | 1, 1, 3, 3, 0, 0 => (4 : Int) | 1, 1, 3, 3, 2, 2 => (4 : Int) | 1, 2, 0, 0, 1, 2 => (-2 : Int) | 1, 2, 0, 0, 2, 1 => (-2 : Int) | 1, 2, 0, 1, 0, 2 => (1 : Int) | 1, 2, 0, 1, 2, 0 => (1 : Int) | 1, 2, 0, 2, 0, 1 => (1 : Int) | 1, 2, 0, 2, 1, 0 => (1 : Int) | 1, 2, 1, 0, 0, 2 => (1 : Int) | 1, 2, 1, 0, 2, 0 => (1 : Int) | 1, 2, 1, 2, 0, 0 => (-2 : Int) | 1, 2, 1, 2, 3, 3 => (-2 : Int) | 1, 2, 1, 3, 2, 3 => (1 : Int) | 1, 2, 1, 3, 3, 2 => (1 : Int) | 1, 2, 2, 0, 0, 1 => (1 : Int) | 1, 2, 2, 0, 1, 0 => (1 : Int) | 1, 2, 2, 1, 0, 0 => (-2 : Int) | 1, 2, 2, 1, 3, 3 => (-2 : Int) | 1, 2, 2, 3, 1, 3 => (1 : Int) | 1, 2, 2, 3, 3, 1 => (1 : Int) | 1, 2, 3, 1, 2, 3 => (1 : Int) | 1, 2, 3, 1, 3, 2 => (1 : Int) | 1, 2, 3, 2, 1, 3 => (1 : Int) | 1, 2, 3, 2, 3, 1 => (1 : Int) | 1, 2, 3, 3, 1, 2 => (-2 : Int) | 1, 2, 3, 3, 2, 1 => (-2 : Int) | 1, 3, 0, 0, 1, 3 => (-2 : Int) | 1, 3, 0, 0, 3, 1 => (-2 : Int) | 1, 3, 0, 1, 0, 3 => (1 : Int) | 1, 3, 0, 1, 3, 0 => (1 : Int) | 1, 3, 0, 3, 0, 1 => (1 : Int) | 1, 3, 0, 3, 1, 0 => (1 : Int) | 1, 3, 1, 0, 0, 3 => (1 : Int) | 1, 3, 1, 0, 3, 0 => (1 : Int) | 1, 3, 1, 2, 2, 3 => (1 : Int) | 1, 3, 1, 2, 3, 2 => (1 : Int) | 1, 3, 1, 3, 0, 0 => (-2 : Int) | 1, 3, 1, 3, 2, 2 => (-2 : Int) | 1, 3, 2, 1, 2, 3 => (1 : Int) | 1, 3, 2, 1, 3, 2 => (1 : Int) | 1, 3, 2, 2, 1, 3 => (-2 : Int) | 1, 3, 2, 2, 3, 1 => (-2 : Int) | 1, 3, 2, 3, 1, 2 => (1 : Int) | 1, 3, 2, 3, 2, 1 => (1 : Int) | 1, 3, 3, 0, 0, 1 => (1 : Int) | 1, 3, 3, 0, 1, 0 => (1 : Int) | 1, 3, 3, 1, 0, 0 => (-2 : Int) | 1, 3, 3, 1, 2, 2 => (-2 : Int) | 1, 3, 3, 2, 1, 2 => (1 : Int) | 1, 3, 3, 2, 2, 1 => (1 : Int) | 2, 0, 0, 1, 1, 2 => (1 : Int) | 2, 0, 0, 1, 2, 1 => (1 : Int) | 2, 0, 0, 2, 1, 1 => (-2 : Int) | 2, 0, 0, 2, 3, 3 => (-2 : Int) | 2, 0, 0, 3, 2, 3 => (1 : Int) | 2, 0, 0, 3, 3, 2 => (1 : Int) | 2, 0, 1, 0, 1, 2 => (1 : Int) | 2, 0, 1, 0, 2, 1 => (1 : Int) | 2, 0, 1, 1, 0, 2 => (-2 : Int) | 2, 0, 1, 1, 2, 0 => (-2 : Int) | 2, 0, 1, 2, 0, 1 => (1 : Int) | 2, 0, 1, 2, 1, 0 => (1 : Int) | 2, 0, 2, 0, 1, 1 => (-2 : Int) | 2, 0, 2, 0, 3, 3 => (-2 : Int) | 2, 0, 2, 1, 0, 1 => (1 : Int) | 2, 0, 2, 1, 1, 0 => (1 : Int) | 2, 0, 2, 3, 0, 3 => (1 : Int) | 2, 0, 2, 3, 3, 0 => (1 : Int) | 2, 0, 3, 0, 2, 3 => (1 : Int) | 2, 0, 3, 0, 3, 2 => (1 : Int) | 2, 0, 3, 2, 0, 3 => (1 : Int) | 2, 0, 3, 2, 3, 0 => (1 : Int) | 2, 0, 3, 3, 0, 2 => (-2 : Int) | 2, 0, 3, 3, 2, 0 => (-2 : Int) | 2, 1, 0, 0, 1, 2 => (-2 : Int) | 2, 1, 0, 0, 2, 1 => (-2 : Int) | 2, 1, 0, 1, 0, 2 => (1 : Int) | 2, 1, 0, 1, 2, 0 => (1 : Int) | 2, 1, 0, 2, 0, 1 => (1 : Int) | 2, 1, 0, 2, 1, 0 => (1 : Int) | 2, 1, 1, 0, 0, 2 => (1 : Int) | 2, 1, 1, 0, 2, 0 => (1 : Int) | 2, 1, 1, 2, 0, 0 => (-2 : Int) | 2, 1, 1, 2, 3, 3 => (-2 : Int) | 2, 1, 1, 3, 2, 3 => (1 : Int) | 2, 1, 1, 3, 3, 2 => (1 : Int) | 2, 1, 2, 0, 0, 1 => (1 : Int) | 2, 1, 2, 0, 1, 0 => (1 : Int) | 2, 1, 2, 1, 0, 0 => (-2 : Int) | 2, 1, 2, 1, 3, 3 => (-2 : Int) | 2, 1, 2, 3, 1, 3 => (1 : Int) | 2, 1, 2, 3, 3, 1 => (1 : Int) | 2, 1, 3, 1, 2, 3 => (1 : Int) | 2, 1, 3, 1, 3, 2 => (1 : Int) | 2, 1, 3, 2, 1, 3 => (1 : Int) | 2, 1, 3, 2, 3, 1 => (1 : Int) | 2, 1, 3, 3, 1, 2 => (-2 : Int) | 2, 1, 3, 3, 2, 1 => (-2 : Int) | 2, 2, 0, 0, 1, 1 => (4 : Int) | 2, 2, 0, 0, 3, 3 => (4 : Int) | 2, 2, 0, 1, 0, 1 => (-2 : Int) | 2, 2, 0, 1, 1, 0 => (-2 : Int) | 2, 2, 0, 3, 0, 3 => (-2 : Int) | 2, 2, 0, 3, 3, 0 => (-2 : Int) | 2, 2, 1, 0, 0, 1 => (-2 : Int) | 2, 2, 1, 0, 1, 0 => (-2 : Int) | 2, 2, 1, 1, 0, 0 => (4 : Int) | 2, 2, 1, 1, 3, 3 => (4 : Int) | 2, 2, 1, 3, 1, 3 => (-2 : Int) | 2, 2, 1, 3, 3, 1 => (-2 : Int) | 2, 2, 3, 0, 0, 3 => (-2 : Int) | 2, 2, 3, 0, 3, 0 => (-2 : Int) | 2, 2, 3, 1, 1, 3 => (-2 : Int) | 2, 2, 3, 1, 3, 1 => (-2 : Int) | 2, 2, 3, 3, 0, 0 => (4 : Int) | 2, 2, 3, 3, 1, 1 => (4 : Int) | 2, 3, 0, 0, 2, 3 => (-2 : Int) | 2, 3, 0, 0, 3, 2 => (-2 : Int) | 2, 3, 0, 2, 0, 3 => (1 : Int) | 2, 3, 0, 2, 3, 0 => (1 : Int) | 2, 3, 0, 3, 0, 2 => (1 : Int) | 2, 3, 0, 3, 2, 0 => (1 : Int) | 2, 3, 1, 1, 2, 3 => (-2 : Int) | 2, 3, 1, 1, 3, 2 => (-2 : Int) | 2, 3, 1, 2, 1, 3 => (1 : Int) | 2, 3, 1, 2, 3, 1 => (1 : Int) | 2, 3, 1, 3, 1, 2 => (1 : Int) | 2, 3, 1, 3, 2, 1 => (1 : Int) | 2, 3, 2, 0, 0, 3 => (1 : Int) | 2, 3, 2, 0, 3, 0 => (1 : Int) | 2, 3, 2, 1, 1, 3 => (1 : Int) | 2, 3, 2, 1, 3, 1 => (1 : Int) | 2, 3, 2, 3, 0, 0 => (-2 : Int) | 2, 3, 2, 3, 1, 1 => (-2 : Int) | 2, 3, 3, 0, 0, 2 => (1 : Int) | 2, 3, 3, 0, 2, 0 => (1 : Int) | 2, 3, 3, 1, 1, 2 => (1 : Int) | 2, 3, 3, 1, 2, 1 => (1 : Int) | 2, 3, 3, 2, 0, 0 => (-2 : Int) | 2, 3, 3, 2, 1, 1 => (-2 : Int) | 3, 0, 0, 1, 1, 3 => (1 : Int) | 3, 0, 0, 1, 3, 1 => (1 : Int) | 3, 0, 0, 2, 2, 3 => (1 : Int) | 3, 0, 0, 2, 3, 2 => (1 : Int) | 3, 0, 0, 3, 1, 1 => (-2 : Int) | 3, 0, 0, 3, 2, 2 => (-2 : Int) | 3, 0, 1, 0, 1, 3 => (1 : Int) | 3, 0, 1, 0, 3, 1 => (1 : Int) | 3, 0, 1, 1, 0, 3 => (-2 : Int) | 3, 0, 1, 1, 3, 0 => (-2 : Int) | 3, 0, 1, 3, 0, 1 => (1 : Int) | 3, 0, 1, 3, 1, 0 => (1 : Int) | 3, 0, 2, 0, 2, 3 => (1 : Int) | 3, 0, 2, 0, 3, 2 => (1 : Int) | 3, 0, 2, 2, 0, 3 => (-2 : Int) | 3, 0, 2, 2, 3, 0 => (-2 : Int) | 3, 0, 2, 3, 0, 2 => (1 : Int) | 3, 0, 2, 3, 2, 0 => (1 : Int) | 3, 0, 3, 0, 1, 1 => (-2 : Int) | 3, 0, 3, 0, 2, 2 => (-2 : Int) | 3, 0, 3, 1, 0, 1 => (1 : Int) | 3, 0, 3, 1, 1, 0 => (1 : Int) | 3, 0, 3, 2, 0, 2 => (1 : Int) | 3, 0, 3, 2, 2, 0 => (1 : Int) | 3, 1, 0, 0, 1, 3 => (-2 : Int) | 3, 1, 0, 0, 3, 1 => (-2 : Int) | 3, 1, 0, 1, 0, 3 => (1 : Int) | 3, 1, 0, 1, 3, 0 => (1 : Int) | 3, 1, 0, 3, 0, 1 => (1 : Int) | 3, 1, 0, 3, 1, 0 => (1 : Int) | 3, 1, 1, 0, 0, 3 => (1 : Int) | 3, 1, 1, 0, 3, 0 => (1 : Int) | 3, 1, 1, 2, 2, 3 => (1 : Int) | 3, 1, 1, 2, 3, 2 => (1 : Int) | 3, 1, 1, 3, 0, 0 => (-2 : Int) | 3, 1, 1, 3, 2, 2 => (-2 : Int) | 3, 1, 2, 1, 2, 3 => (1 : Int) | 3, 1, 2, 1, 3, 2 => (1 : Int) | 3, 1, 2, 2, 1, 3 => (-2 : Int) | 3, 1, 2, 2, 3, 1 => (-2 : Int) | 3, 1, 2, 3, 1, 2 => (1 : Int) | 3, 1, 2, 3, 2, 1 => (1 : Int) | 3, 1, 3, 0, 0, 1 => (1 : Int) | 3, 1, 3, 0, 1, 0 => (1 : Int) | 3, 1, 3, 1, 0, 0 => (-2 : Int) | 3, 1, 3, 1, 2, 2 => (-2 : Int) | 3, 1, 3, 2, 1, 2 => (1 : Int) | 3, 1, 3, 2, 2, 1 => (1 : Int) | 3, 2, 0, 0, 2, 3 => (-2 : Int) | 3, 2, 0, 0, 3, 2 => (-2 : Int) | 3, 2, 0, 2, 0, 3 => (1 : Int) | 3, 2, 0, 2, 3, 0 => (1 : Int) | 3, 2, 0, 3, 0, 2 => (1 : Int) | 3, 2, 0, 3, 2, 0 => (1 : Int) | 3, 2, 1, 1, 2, 3 => (-2 : Int) | 3, 2, 1, 1, 3, 2 => (-2 : Int) | 3, 2, 1, 2, 1, 3 => (1 : Int) | 3, 2, 1, 2, 3, 1 => (1 : Int) | 3, 2, 1, 3, 1, 2 => (1 : Int) | 3, 2, 1, 3, 2, 1 => (1 : Int) | 3, 2, 2, 0, 0, 3 => (1 : Int) | 3, 2, 2, 0, 3, 0 => (1 : Int) | 3, 2, 2, 1, 1, 3 => (1 : Int) | 3, 2, 2, 1, 3, 1 => (1 : Int) | 3, 2, 2, 3, 0, 0 => (-2 : Int) | 3, 2, 2, 3, 1, 1 => (-2 : Int) | 3, 2, 3, 0, 0, 2 => (1 : Int) | 3, 2, 3, 0, 2, 0 => (1 : Int) | 3, 2, 3, 1, 1, 2 => (1 : Int) | 3, 2, 3, 1, 2, 1 => (1 : Int) | 3, 2, 3, 2, 0, 0 => (-2 : Int) | 3, 2, 3, 2, 1, 1 => (-2 : Int) | 3, 3, 0, 0, 1, 1 => (4 : Int) | 3, 3, 0, 0, 2, 2 => (4 : Int) | 3, 3, 0, 1, 0, 1 => (-2 : Int) | 3, 3, 0, 1, 1, 0 => (-2 : Int) | 3, 3, 0, 2, 0, 2 => (-2 : Int) -- … truncated for the page; open the module for the rest.This particular certificate does not derive any new physics. explicitZ · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DKernelCert.lean