Encyclopedia Gravity Gravity Analysis Regge Exact Midpoint M2 Ttidentity4 Dm2 Num Assemble

ARTICLE 2 claims 2 theorems

Gravity Analysis Regge Exact Midpoint M2 Ttidentity4 Dm2 Num Assemble

A machine-checked proof that a 4096-term gravitational identity holds exactly, by splitting it into 16 tractable pieces.

Verify this page

The assembly lemma

The module is a piece of bookkeeping inside a larger proof. The larger proof concerns an identity that compares two ways of computing a quantity called m2Num, which appears in an analysis of gravity. The identity claims that m2Num always equals 8 times another quantity, explicitZ, for every choice of six indices, each running over four values. That is 4 to the 6th power, or 4096, separate cases in total.

Proving all 4096 cases at once would overwhelm the proof checker. The module therefore splits the work into 16 chunks, one for each fixed pair of the first two indices. Each chunk proves the identity for the remaining 256 combinations of the other four indices. The module states this as 16 separate theorems, one per chunk, and then combines them into a single theorem covering all cases.

In Recognition Science, the framework treats physical structure as derived from a discrete record of events, called a ledger. The identity here is part of a larger effort to show that a certain gravitational expression, built from the ledger's geometry, satisfies a required symmetry. The module itself does not interpret the physics; it certifies the algebra.

The final theorem, m2Num_eq_eight_explicitZ, states that for all indices a, b, c, d, i, and j, each in the set {0, 1, 2, 3}, the equation m2Num a b c d i j = 8 * explicitZ a b c d i j holds. The factor of 8 is not an approximation; it is exact. The proof is machine-checked, meaning no step is left to human judgment.

What this establishes in plain language is that a complicated sum, built from many terms, collapses to a simple multiple of a single reference quantity. The identity is a necessary step for the framework's gravitational analysis to proceed. It does not by itself prove any physical law; it removes a computational obstacle.

THEOREM m2Num_eq_eight_explicitZ · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumAssemble.lean
m2Num_eq_eight_explicitZ · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumAssemble.lean:4242 
theorem m2Num_eq_eight_explicitZ :
    ∀ (a b c d i j : Fin 4),
      m2Num a b c d i j = 8 * explicitZ a b c d i j := by
  intro a b c d i j
  fin_cases a <;> fin_cases b
  · exact m2Num_eq_eight_explicitZ_00 c d i j
  · exact m2Num_eq_eight_explicitZ_01 c d i j
  · exact m2Num_eq_eight_explicitZ_02 c d i j
  · exact m2Num_eq_eight_explicitZ_03 c d i j
  · exact m2Num_eq_eight_explicitZ_10 c d i j
  · exact m2Num_eq_eight_explicitZ_11 c d i j
  · exact m2Num_eq_eight_explicitZ_12 c d i j
  · exact m2Num_eq_eight_explicitZ_13 c d i j
  · exact m2Num_eq_eight_explicitZ_20 c d i j
  · exact m2Num_eq_eight_explicitZ_21 c d i j
  · exact m2Num_eq_eight_explicitZ_22 c d i j
  · exact m2Num_eq_eight_explicitZ_23 c d i j
  · exact m2Num_eq_eight_explicitZ_30 c d i j
  · exact m2Num_eq_eight_explicitZ_31 c d i j
  · exact m2Num_eq_eight_explicitZ_32 c d i j
  · exact m2Num_eq_eight_explicitZ_33 c d i j
THEOREM m2Num_eq_eight_explicitZ_00 · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumAssemble.lean
m2Num_eq_eight_explicitZ_00 · IndisputableMonolith/Gravity/Analysis/ReggeExactMidpointM2TTIdentity4DM2NumAssemble.lean:34 
/-- Fixed `(a,b)=(0,0)` packer (chunk 00). -/
theorem m2Num_eq_eight_explicitZ_00 :
    ∀ (c d i j : Fin 4),
      m2Num 0 0 c d i j = 8 * explicitZ 0 0 c d i j := by
  intro c d i j
  fin_cases c <;> fin_cases d <;> fin_cases i <;> fin_cases j
  · exact M2NumChunk00.e_000000
  · exact M2NumChunk00.e_000001
  · exact M2NumChunk00.e_000002
  · exact M2NumChunk00.e_000003
  · exact M2NumChunk00.e_000010
  · exact M2NumChunk00.e_000011
  · exact M2NumChunk00.e_000012
  · exact M2NumChunk00.e_000013
  · exact M2NumChunk00.e_000020
  · exact M2NumChunk00.e_000021
  · exact M2NumChunk00.e_000022
  · exact M2NumChunk00.e_000023
  · exact M2NumChunk00.e_000030
  · exact M2NumChunk00.e_000031
  · exact M2NumChunk00.e_000032
  · exact M2NumChunk00.e_000033
  · exact M2NumChunk00.e_000100
  · exact M2NumChunk00.e_000101
  · exact M2NumChunk00.e_000102
  · exact M2NumChunk00.e_000103
  · exact M2NumChunk00.e_000110
  · exact M2NumChunk00.e_000111
  · exact M2NumChunk00.e_000112
  · exact M2NumChunk00.e_000113
  · exact M2NumChunk00.e_000120
  · exact M2NumChunk00.e_000121
  · exact M2NumChunk00.e_000122
  · exact M2NumChunk00.e_000123
  · exact M2NumChunk00.e_000130
  · exact M2NumChunk00.e_000131
  · exact M2NumChunk00.e_000132
  · exact M2NumChunk00.e_000133
  · exact M2NumChunk00.e_000200
  · exact M2NumChunk00.e_000201
  · exact M2NumChunk00.e_000202
  · exact M2NumChunk00.e_000203
  · exact M2NumChunk00.e_000210
  · exact M2NumChunk00.e_000211
  · exact M2NumChunk00.e_000212
  · exact M2NumChunk00.e_000213
  · exact M2NumChunk00.e_000220
  · exact M2NumChunk00.e_000221
  · exact M2NumChunk00.e_000222
  · exact M2NumChunk00.e_000223
  · exact M2NumChunk00.e_000230
  · exact M2NumChunk00.e_000231
  · exact M2NumChunk00.e_000232
  · exact M2NumChunk00.e_000233
  · exact M2NumChunk00.e_000300
  · exact M2NumChunk00.e_000301
  · exact M2NumChunk00.e_000302
  · exact M2NumChunk00.e_000303
  · exact M2NumChunk00.e_000310
  · exact M2NumChunk00.e_000311
  · exact M2NumChunk00.e_000312
  · exact M2NumChunk00.e_000313
  · exact M2NumChunk00.e_000320
  · exact M2NumChunk00.e_000321
  · exact M2NumChunk00.e_000322
  · exact M2NumChunk00.e_000323
  · exact M2NumChunk00.e_000330
  · exact M2NumChunk00.e_000331
  · exact M2NumChunk00.e_000332
  · exact M2NumChunk00.e_000333
  · exact M2NumChunk00.e_001000
  · exact M2NumChunk00.e_001001
  · exact M2NumChunk00.e_001002
  · exact M2NumChunk00.e_001003
  · exact M2NumChunk00.e_001010
  · exact M2NumChunk00.e_001011
  · exact M2NumChunk00.e_001012
  · exact M2NumChunk00.e_001013
  · exact M2NumChunk00.e_001020
  · exact M2NumChunk00.e_001021
  · exact M2NumChunk00.e_001022
  · exact M2NumChunk00.e_001023
  · exact M2NumChunk00.e_001030
  · exact M2NumChunk00.e_001031
  · exact M2NumChunk00.e_001032
  · exact M2NumChunk00.e_001033
  · exact M2NumChunk00.e_001100
  · exact M2NumChunk00.e_001101
  · exact M2NumChunk00.e_001102
  · exact M2NumChunk00.e_001103
  · exact M2NumChunk00.e_001110
  · exact M2NumChunk00.e_001111
  · exact M2NumChunk00.e_001112
  · exact M2NumChunk00.e_001113
  · exact M2NumChunk00.e_001120
  · exact M2NumChunk00.e_001121
  · exact M2NumChunk00.e_001122
  · exact M2NumChunk00.e_001123
  · exact M2NumChunk00.e_001130
  · exact M2NumChunk00.e_001131
  · exact M2NumChunk00.e_001132
  · exact M2NumChunk00.e_001133
  · exact M2NumChunk00.e_001200
  · exact M2NumChunk00.e_001201
  · exact M2NumChunk00.e_001202
  · exact M2NumChunk00.e_001203
  · exact M2NumChunk00.e_001210
  · exact M2NumChunk00.e_001211
  · exact M2NumChunk00.e_001212
  · exact M2NumChunk00.e_001213
  · exact M2NumChunk00.e_001220
  · exact M2NumChunk00.e_001221
  · exact M2NumChunk00.e_001222
  · exact M2NumChunk00.e_001223
  · exact M2NumChunk00.e_001230
  · exact M2NumChunk00.e_001231
  · exact M2NumChunk00.e_001232
  · exact M2NumChunk00.e_001233
  · exact M2NumChunk00.e_001300
  · exact M2NumChunk00.e_001301
  · exact M2NumChunk00.e_001302
  · exact M2NumChunk00.e_001303
  · exact M2NumChunk00.e_001310
  · exact M2NumChunk00.e_001311
  · exact M2NumChunk00.e_001312
  · exact M2NumChunk00.e_001313
  · exact M2NumChunk00.e_001320
  · exact M2NumChunk00.e_001321
  · exact M2NumChunk00.e_001322
  · exact M2NumChunk00.e_001323
  · exact M2NumChunk00.e_001330
  · exact M2NumChunk00.e_001331
  · exact M2NumChunk00.e_001332
  · exact M2NumChunk00.e_001333
  · exact M2NumChunk00.e_002000
  · exact M2NumChunk00.e_002001
  · exact M2NumChunk00.e_002002
  · exact M2NumChunk00.e_002003
  · exact M2NumChunk00.e_002010
  · exact M2NumChunk00.e_002011
  · exact M2NumChunk00.e_002012
  · exact M2NumChunk00.e_002013
  · exact M2NumChunk00.e_002020
  · exact M2NumChunk00.e_002021
  · exact M2NumChunk00.e_002022
  · exact M2NumChunk00.e_002023
  · exact M2NumChunk00.e_002030
  · exact M2NumChunk00.e_002031
  · exact M2NumChunk00.e_002032
  · exact M2NumChunk00.e_002033
  · exact M2NumChunk00.e_002100
  · exact M2NumChunk00.e_002101
  · exact M2NumChunk00.e_002102
  · exact M2NumChunk00.e_002103
  · exact M2NumChunk00.e_002110
  · exact M2NumChunk00.e_002111
  · exact M2NumChunk00.e_002112
  · exact M2NumChunk00.e_002113
  · exact M2NumChunk00.e_002120
  · exact M2NumChunk00.e_002121
  · exact M2NumChunk00.e_002122
  · exact M2NumChunk00.e_002123
  · exact M2NumChunk00.e_002130
  · exact M2NumChunk00.e_002131
  · exact M2NumChunk00.e_002132
  · exact M2NumChunk00.e_002133
  · exact M2NumChunk00.e_002200
  · exact M2NumChunk00.e_002201
  · exact M2NumChunk00.e_002202
  · exact M2NumChunk00.e_002203
  · exact M2NumChunk00.e_002210
  · exact M2NumChunk00.e_002211
  · exact M2NumChunk00.e_002212
  · exact M2NumChunk00.e_002213
  · exact M2NumChunk00.e_002220
  · exact M2NumChunk00.e_002221
  · exact M2NumChunk00.e_002222
  · exact M2NumChunk00.e_002223
  · exact M2NumChunk00.e_002230
  · exact M2NumChunk00.e_002231
  · exact M2NumChunk00.e_002232
  · exact M2NumChunk00.e_002233
  · exact M2NumChunk00.e_002300
  · exact M2NumChunk00.e_002301
  · exact M2NumChunk00.e_002302
  · exact M2NumChunk00.e_002303
  · exact M2NumChunk00.e_002310
  · exact M2NumChunk00.e_002311
  · exact M2NumChunk00.e_002312
  · exact M2NumChunk00.e_002313
  · exact M2NumChunk00.e_002320
  · exact M2NumChunk00.e_002321
  · exact M2NumChunk00.e_002322
  · exact M2NumChunk00.e_002323
  · exact M2NumChunk00.e_002330
  · exact M2NumChunk00.e_002331
  · exact M2NumChunk00.e_002332
  · exact M2NumChunk00.e_002333
  · exact M2NumChunk00.e_003000
  · exact M2NumChunk00.e_003001
  · exact M2NumChunk00.e_003002
  · exact M2NumChunk00.e_003003
  · exact M2NumChunk00.e_003010
  · exact M2NumChunk00.e_003011
  · exact M2NumChunk00.e_003012
  · exact M2NumChunk00.e_003013
  · exact M2NumChunk00.e_003020
  · exact M2NumChunk00.e_003021
  · exact M2NumChunk00.e_003022
  · exact M2NumChunk00.e_003023
  · exact M2NumChunk00.e_003030
  · exact M2NumChunk00.e_003031
  · exact M2NumChunk00.e_003032
  · exact M2NumChunk00.e_003033
  · exact M2NumChunk00.e_003100
  · exact M2NumChunk00.e_003101
  · exact M2NumChunk00.e_003102
  · exact M2NumChunk00.e_003103
  · exact M2NumChunk00.e_003110
  · exact M2NumChunk00.e_003111
  · exact M2NumChunk00.e_003112
  · exact M2NumChunk00.e_003113
  · exact M2NumChunk00.e_003120
  · exact M2NumChunk00.e_003121
  · exact M2NumChunk00.e_003122
  · exact M2NumChunk00.e_003123
  · exact M2NumChunk00.e_003130
  · exact M2NumChunk00.e_003131
  · exact M2NumChunk00.e_003132
  · exact M2NumChunk00.e_003133
  · exact M2NumChunk00.e_003200
  · exact M2NumChunk00.e_003201
  · exact M2NumChunk00.e_003202
  · exact M2NumChunk00.e_003203
  · exact M2NumChunk00.e_003210
  · exact M2NumChunk00.e_003211
  · exact M2NumChunk00.e_003212
  · exact M2NumChunk00.e_003213
  · exact M2NumChunk00.e_003220
  · exact M2NumChunk00.e_003221
  · exact M2NumChunk00.e_003222
  · exact M2NumChunk00.e_003223
  · exact M2NumChunk00.e_003230
  · exact M2NumChunk00.e_003231
  · exact M2NumChunk00.e_003232
  · exact M2NumChunk00.e_003233
  · exact M2NumChunk00.e_003300
  · exact M2NumChunk00.e_003301
  · exact M2NumChunk00.e_003302
  · exact M2NumChunk00.e_003303
  · exact M2NumChunk00.e_003310
  · exact M2NumChunk00.e_003311
  · exact M2NumChunk00.e_003312
  · exact M2NumChunk00.e_003313
  · exact M2NumChunk00.e_003320
  · exact M2NumChunk00.e_003321
  · exact M2NumChunk00.e_003322
  · exact M2NumChunk00.e_003323
  · exact M2NumChunk00.e_003330
  · exact M2NumChunk00.e_003331
  · exact M2NumChunk00.e_003332
  · exact M2NumChunk00.e_003333

What this page does not claim

This module does not establish any physical law or interpretation of gravity. The identity does not prove that the framework's gravitational analysis is correct; it only certifies an algebraic step.

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/ReggeExactMidpointM2TTIdentity4DM2NumAssemble.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND