Gravity Seven Gaps Cap Shell Bridge Sum Shells Up To Eq Exact Complexity Cutoff

The shell sum identity

In the Recognition Science framework, the declaration sum_shellsUpTo_eq_exactComplexityCutoff proves a precise identity about how to count and weight certain discrete geometric objects called shells, which are collections of cells (vertices, edges, tetrahedra) organized by a complexity measure. The theorem states that summing over all shells up to a cap B, with each shell weighted by a phase factor and a measure, equals the value of a separate function exactComplexityCutoff that sums over the same range using a different indexing. In plain terms, it shows two different bookkeeping systems for the same set of objects give the same total.

The identity is not an isolated calculation. It is the capstone of a bridge construction in the framework's library, a machine-checked collection of formal theorems. The bridge connects two ways of describing a bounded complex, a geometric object with a complexity bound. On one side, you have a bounded complex directly. On the other, you have an exact complex in a shell, which carries additional structure. The proof constructs maps back and forth between these descriptions, shows they are inverses, and verifies that the maps preserve the key measure, the reciprocal of the automorphism group size. This measure is what weights each shell in the sum.

The theorem's power is that it lets a physicist or mathematician choose whichever description is more convenient for a calculation, knowing the sums will agree. It is a formal guarantee of consistency between two representations. The proof itself is carried out in the Lean 4 proof assistant, with no axioms beyond the standard three (propext, Classical.choice, Quot.sound). This means the identity is not a conjecture or a heuristic; it is a proved theorem in the framework's library.

What the theorem does not claim is equally important. It does not assert any physical interpretation of the shells or the phases. It does not claim the sums converge in any analytic sense, nor does it specify what the phases represent physically. The theorem is purely combinatorial and algebraic: given a phase function on exact path classes, the two sums are equal. Any physical meaning, such as identifying these sums with a gravitational partition function, is a separate step that the theorem does not take.

The practical consequence is that the framework has a verified tool for translating between a bounded and an exact description of geometric states. This is a necessary step for any future work that wants to use the exact description for computations, because it guarantees the two views are interchangeable without loss of information. The identity is a piece of infrastructure, not a physical law, but it is infrastructure that has been checked to the letter.

/-- Splitting the disjoint-union carrier gives exactly the shell cutoff
through `B`; the range is `B + 1`, so shell `B` is included. -/
theorem sum_shellsUpTo_eq_exactComplexityCutoff
    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (B : ℕ) :
    (∑ x : ShellsUpTo B,
      (classMu x.2 : ℂ) *
        Complex.exp (Complex.I * (phase x.1 x.2 : ℂ))) =
      exactComplexityCutoff phase B := by
  rw [Fintype.sum_sigma]
  change (∑ n : Fin (B + 1), exactShellAmplitude phase n) =
    ∑ n ∈ Finset.range (B + 1), exactShellAmplitude phase n
  exact sum_fin_eq_sum_range (exactShellAmplitude phase) (B + 1)

/-- **HEADLINE CARRIER EQUIVALENCE.**  Bounded quotient classes at cap `B`
are exactly the disjoint union of exact quotient shells `0, ..., B`. -/
def capShellEquiv (B : ℕ) : TriangulationClass B ≃ ShellsUpTo B where
  toFun := capToShell
  invFun := shellToCap
  left_inv := shellToCap_capToShell
  right_inv := capToShell_shellToCap

/-- **QUOTIENT-LEVEL MEASURE PRESERVATION.**  The class measure on the
exact-shell image is the capped representative measure. -/
theorem classMu_capToShell {B : ℕ} (q : TriangulationClass B) :
    classMu (capToShell q).2 = mu (Quotient.out q) := by
  refine Quotient.inductionOn q ?_
  intro K
  let qe := Quotient.mk (exactSetoid K.nV K.nE K.nT) (toExact K)
  have hrel : GlobalEquivalent (Quotient.out qe) (toExact K) :=
    Quotient.exact (Quotient.out_eq qe)
  have hcap : Equivalent
      (Quotient.out (Quotient.mk (relabelSetoid B) K)) K :=
    PathSum.equivalent_of_mk_eq
      (Quotient.out_eq (Quotient.mk (relabelSetoid B) K))
  dsimp [capToShell, boundedToShell, classMu]
  show classMuOn K.nV K.nE K.nT qe =
    mu (Quotient.out (Quotient.mk (relabelSetoid B) K))
  rw [RegulatorRemovalNoGo.classMuOn_out qe]
  calc
    exactMu (Quotient.out qe) = exactMu (toExact K) := exactMu_congr hrel
    _ = mu K := (mu_eq_exactMu_toExact K).symm
    _ = mu (Quotient.out (Quotient.mk (relabelSetoid B) K)) :=
        (mu_congr hcap).symm

/-- Splitting the disjoint-union carrier gives exactly the shell cutoff
through `B`; the range is `B + 1`, so shell `B` is included. -/
theorem sum_shellsUpTo_eq_exactComplexityCutoff
    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (B : ℕ) :
    (∑ x : ShellsUpTo B,
      (classMu x.2 : ℂ) *
        Complex.exp (Complex.I * (phase x.1 x.2 : ℂ))) =
      exactComplexityCutoff phase B := by
  rw [Fintype.sum_sigma]
  change (∑ n : Fin (B + 1), exactShellAmplitude phase n) =
    ∑ n ∈ Finset.range (B + 1), exactShellAmplitude phase n
  exact sum_fin_eq_sum_range (exactShellAmplitude phase) (B + 1)

/-- Splitting the disjoint-union carrier gives exactly the shell cutoff
through `B`; the range is `B + 1`, so shell `B` is included. -/
theorem sum_shellsUpTo_eq_exactComplexityCutoff
    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (B : ℕ) :
    (∑ x : ShellsUpTo B,
      (classMu x.2 : ℂ) *
        Complex.exp (Complex.I * (phase x.1 x.2 : ℂ))) =
      exactComplexityCutoff phase B := by
  rw [Fintype.sum_sigma]
  change (∑ n : Fin (B + 1), exactShellAmplitude phase n) =
    ∑ n ∈ Finset.range (B + 1), exactShellAmplitude phase n
  exact sum_fin_eq_sum_range (exactShellAmplitude phase) (B + 1)

What this page does not claim

The theorem does not assert any physical meaning for the shells or the phases. The theorem does not claim the sums converge in an analytic sense. The theorem does not identify the sums with a gravitational partition function.

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/SevenGaps/CapShellBridge.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: