Gravity Seven Gaps Cap Shell Bridge Shell To Cap Bounded To Shell

The cap-shell bridge

In the study of triangulated spaces, a cap is a bound on the total complexity of a complex, while a shell is a bound on the complexity of each individual piece. The declaration shellToCap_boundedToShell is part of a larger bridge: it proves that any complex that fits within a shell also fits within the corresponding cap, and that this conversion preserves the essential structure. The theorem states that if you take a bounded complex and convert it to its shell representation, then convert that back to a cap, you recover the original complex exactly, up to the standard notion of equivalence.

The proof works by constructing explicit maps in both directions. Going from cap to shell, a complex is assigned to the shell indexed by its exact complexity, which is the maximum of its vertex, edge, and tetrahedron counts. Going from shell to cap, a complex in a shell of size n is reattached to the cap of size B by supplying the necessary inequality proofs. The key theorem shellToCap_boundedToShell shows that these two maps are inverses: starting with a bounded complex, converting to shell and back yields the same complex. This is the core of the equivalence capShellEquiv, which establishes that the two quotient carriers, the collections of equivalence classes under relabeling, are in bijection.

The bridge also preserves the counting measure used in the framework. The theorem autCard_toExact shows that the number of automorphisms of a complex is unchanged when passing to its exact representation, and mu_eq_exactMu_toExact extends this to the class measure. This means that the sum over shells of the weighted phase amplitudes equals the sum over caps, as shown in sum_shellsUpTo_eq_exactComplexityCutoff. The consequence is that the framework can compute the same physical quantities whether it organizes states by cap or by shell, and the two descriptions are not merely compatible but identical in content.

What the declaration does not claim is just as important. It does not assert that any particular sum converges, nor that any specific phase value is physical. It does not assume that the shell representation corresponds to a substrate or to a continuum interpretation. The bridge is a purely combinatorial and algebraic fact about the two ways of organizing the same finite complexes. It establishes an equivalence of carriers, not a statement about the physical meaning of the phases or the convergence of the sums they appear in.

/-- Attaching a cap after forgetting it returns the original bounded class. -/
theorem shellToCap_boundedToShell {B : ℕ} (K : BoundedComplex B) :
    shellToCap (boundedToShell K) =
      Quotient.mk (relabelSetoid B) K := by
  apply Quotient.sound
  exact ⟨{
    vEquiv := Equiv.refl _
    eEquiv := Equiv.refl _
    tEquiv := Equiv.refl _
    edge_comm := by
      intro e
      change K.edgeVerts e =
        Prod.map (Equiv.refl _) (Equiv.refl _) (K.edgeVerts e)
      cases K.edgeVerts e
      rfl
    tet_comm := by
      intro t i
      rfl }⟩

/-- Attaching a cap after forgetting it returns the original bounded class. -/
theorem shellToCap_boundedToShell {B : ℕ} (K : BoundedComplex B) :
    shellToCap (boundedToShell K) =
      Quotient.mk (relabelSetoid B) K := by
  apply Quotient.sound
  exact ⟨{
    vEquiv := Equiv.refl _
    eEquiv := Equiv.refl _
    tEquiv := Equiv.refl _
    edge_comm := by
      intro e
      change K.edgeVerts e =
        Prod.map (Equiv.refl _) (Equiv.refl _) (K.edgeVerts e)
      cases K.edgeVerts e
      rfl
    tet_comm := by
      intro t i
      rfl }⟩

/-- The labeled symmetry-factor measures agree under cap forgetting. -/
theorem mu_eq_exactMu_toExact {B : ℕ} (K : BoundedComplex B) :
    mu K = exactMu (toExact K) := by
  unfold mu exactMu
  rw [autCard_toExact K]

/-- 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 declaration does not assert that any particular sum converges. The declaration does not assume a substrate or a continuum interpretation for the shell representation. The declaration does not assign physical meaning to the phase values that appear in the sums.

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: