Gravity Analysis Regge Exact Flat Hessian Bloch Data4 D Coupling Chunk14 Size

A chunk of the coupling table

The declaration couplingChunk14_size is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It establishes that the array named couplingChunk14 contains exactly 80 elements. The proof is a direct computation: the theorem states couplingChunk14.size = 80 and is verified by the kernel through definitional equality, meaning the statement is true by the very way the array is defined.

This array is the fourteenth of sixteen chunks that together form a larger table called couplingTable. The table encodes a discrete set of coupling data for a four-dimensional Regge calculus analysis of a flat Hessian. Each entry in the table, a Coupling structure, records a rational number s = num/den, two edge displacement vectors De and Dep in four dimensions, and a doubled midpoint offset delta2. These numbers feed into a Bloch symbol, a periodic function used to study wave propagation in a lattice, through the formula (1/2) Σ s · (D_eᵀ H D_e)(D_epᵀ H D_ep) · cos(k·Δ).

The chunking exists for a practical reason: splitting the table into 80-entry pieces keeps the Lean elaboration within its recursion depth limits. The full table, assembled by concatenating all sixteen chunks, is proven to contain 1208 entries. The theorem about chunk 14 is therefore a bookkeeping fact, not a physical law. It guarantees the data structure is complete and consistent, so that later theorems about the Bloch symbol can rely on the table's size without re-checking every entry.

In Recognition Science, this fits into a larger project of deriving physical structure from a ledger of recognition events. The table is a concrete, machine-checked data object within that effort. What the theorem does not claim is any physical content: it says nothing about what the couplings mean, whether the Regge calculus model is correct, or what the Bloch symbol predicts. It only certifies that this particular array has the expected number of entries, a necessary but purely structural step in a much larger formal development.

theorem couplingChunk14_size : couplingChunk14.size = 80 := rfl

theorem couplingTable_size : couplingTable.size = 1208 := by
  simp only [couplingTable, Array.size_append, couplingChunk0_size, couplingChunk1_size, couplingChunk2_size, couplingChunk3_size, couplingChunk4_size, couplingChunk5_size, couplingChunk6_size, couplingChunk7_size, couplingChunk8_size, couplingChunk9_size, couplingChunk10_size, couplingChunk11_size, couplingChunk12_size, couplingChunk13_size, couplingChunk14_size, couplingChunk15_size]

What this page does not claim

The theorem does not assert any physical meaning or correctness of the couplings. It does not claim the Regge calculus model is a valid description of gravity. It does not state what the Bloch symbol predicts about wave propagation.

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