Gravity Analysis Regge Exact Midpoint M2 Ttidentity4 Dkernel Cert Cz Chunk11 Bri

The bridge theorem

In numerical work, the same mathematical object can be represented in two different ways: once as a compact symbolic formula, and once as a long explicit table of numbers. When the two disagree, the error is almost always in the translation between them. The declaration czChunk11_bridge is a machine-checked proof that, for the eleventh of sixteen blocks of a four-dimensional gravitational calculation, the two representations are exactly equal.

The calculation concerns the Regge exact midpoint m² TT identity, a relation in discrete gravity. The framework's machine-checked library of formal theorems proves, block by block, that a symbolic expression called the coupling list, when converted into the explicit table format, matches the precomputed table called czChunk11. The proof method is decide, meaning the computer checks the equality by direct computation over the finite list of entries, not by a general argument. This is a brute-force verification, but a complete one: every entry in the block is checked, and the check is recorded as a formal theorem.

The theorem is one of sixteen such bridge proofs, one for each chunk. Together they establish that the full conversion from the symbolic coupling list to the explicit table is correct. The value of this is practical: when a later proof uses the explicit table, it can rely on the table being exactly the same object as the symbolic formula, with no transcription error. The bridge is what lets the framework treat the table as a trustworthy substitute for the formula.

What the theorem does not claim is just as important. It does not prove that the Regge identity itself is physically correct, nor that the midpoint m² TT identity holds in general. It only proves that two specific finite lists are equal after conversion. The physical meaning of the identity, its derivation from the framework's axioms, and its connection to measured gravity are all separate questions, not settled by this declaration.

theorem czChunk11_bridge :
    couplingChunk11.toList.map toCZ = czChunk11 := by
  decide

theorem czChunk11_bridge :
    couplingChunk11.toList.map toCZ = czChunk11 := by
  decide

What this page does not claim

The theorem does not prove the Regge identity itself is physically correct. The theorem does not claim the midpoint m² TT identity holds in general. The theorem does not connect the calculation to measured gravity.

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: