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

The cap-to-shell bridge

In the Recognition Science framework's ledger, a discrete record of events, the study of gravity works with triangulations, networks of triangles glued along edges. The framework groups these triangulations into classes, where two are considered the same if one can be relabeled to become the other. The declaration capToShell_shellToCap establishes that two seemingly different ways of organizing these classes are actually the same.

The first organization, called the cap, collects all triangulations whose complexity, a measure of how many vertices, edges, and tetrahedra they have, is at most a bound B. The second, called the shell, organizes triangulations by their exact complexity, placing each in a specific shell indexed by that exact number. The bridge provides a two-way translation: a map from cap classes to shell classes, and a map back. The key result is that these two maps are inverses, meaning the two organizations contain exactly the same information.

This equivalence is not just structural. The bridge also preserves the automorphism cardinality, the number of ways a triangulation can be relabeled to itself. This matters because the framework's measure of a class, its contribution to the sum over all classes, is one over this automorphism count. By preserving this count, the bridge proves that the total sum computed using the cap organization equals the sum computed using the shell organization, for any choice of phase, a real number assigned to each exact shell class.

This equality is the content of the theorem capShellCompatibility. It shows that a phase defined on exact shells can be transported to a phase model at every cap, and the resulting sums agree. This is a technical consistency result: it ensures that the framework's bookkeeping does not depend on which of two equivalent organizational schemes is chosen.

What the declaration does not do is make any physical claim. It does not assert that any particular sum converges, nor does it identify a specific phase or a physical continuum interpretation. It is a statement about the internal consistency of the framework's combinatorial bookkeeping, not about the physical content of the model. The bridge is a piece of pure structure, a guarantee that two ledgers are kept in the same way.

/-- **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

/-- Left inverse law on bounded quotient classes. -/
theorem shellToCap_capToShell {B : ℕ} (q : TriangulationClass B) :
    shellToCap (capToShell q) = q := by
  refine Quotient.inductionOn q ?_
  intro K
  exact shellToCap_boundedToShell K

/-- Right inverse law on exact-shell quotient classes. -/
theorem capToShell_shellToCap {B : ℕ} (x : ShellsUpTo B) :
    capToShell (shellToCap x) = x := by
  rcases x with ⟨⟨n, hn⟩, s, q⟩
  refine Quotient.inductionOn q ?_
  intro K
  exact boundedToShell_exactToBounded (Nat.le_of_lt_succ hn) s K

/-- **AUTOMORPHISM-CARDINALITY PRESERVATION.** -/
theorem autCard_toExact {B : ℕ} (K : BoundedComplex B) :
    Nat.card (Aut K) = Nat.card (ExactAut (toExact K)) :=
  Nat.card_congr (autEquivToExact K)

/-- **P2.3 CLOSER.**  Every exact-shell phase has a canonically transported
capped phase family satisfying the previously missing
`ZqContinuumBlocker.CapShellCompatibility`. -/
theorem capShellCompatibility
    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) :
    CapShellCompatibility (capPhaseFamily phase) phase :=
  ⟨phasedZq_eq_exactComplexityCutoff phase⟩

/-- **HEADLINE FINITE-SUM REINDEXING.**  The phased capped quotient sum
transported from any exact-shell phase equals its exact-shell cutoff through
shell `B`. -/
theorem phasedZq_eq_exactComplexityCutoff
    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (B : ℕ) :
    phasedZqSequence (capPhaseFamily phase) B =
      exactComplexityCutoff phase B := by
  unfold phasedZqSequence
  change Zq B (phasedWeight (phaseModelAtCap phase B)) =
    exactComplexityCutoff phase B
  rw [Zq]
  calc
    (∑ q : TriangulationClass B,
      (mu (Quotient.out q) : ℂ) *
        phasedWeight (phaseModelAtCap phase B) q)
        = ∑ x : ShellsUpTo B,
            (classMu x.2 : ℂ) *
              Complex.exp (Complex.I * (phase x.1 x.2 : ℂ)) := by
            apply Fintype.sum_equiv (capShellEquiv B)
            intro q
            change (mu (Quotient.out q) : ℂ) *
                phasedWeight (phaseModelAtCap phase B) q =
              (classMu (capToShell q).2 : ℂ) *
                Complex.exp (Complex.I * (phase (capToShell q).1 (capToShell q).2 : ℂ))
            rw [classMu_capToShell]
            simp only [phasedWeight, classPhase_phaseModelAtCap]
    _ = exactComplexityCutoff phase B :=
      sum_shellsUpTo_eq_exactComplexityCutoff phase B

What this page does not claim

The bridge does not assert that any particular sum over triangulation classes converges. The declaration does not identify a specific phase function or a physical continuum interpretation. This result does not by itself derive any physical constant or law.

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: