Gravity Seven Gaps Cap Shell Bridge Cap Shell Compatibility

The cap-shell bridge

The declaration capShellCompatibility is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It establishes that two different ways of organizing a certain class of geometric objects, called bounded complexes, produce the same total count when phases are assigned. The first way, the cap approach, considers all complexes whose complexity, a measure of size, is at most some bound B. The second way, the shell approach, groups complexes by their exact complexity value n, where n ranges from 0 up to B.

The theorem proves these two organizations are equivalent through a pair of maps that go back and forth. A bounded complex at cap B has a unique exact complexity, so it maps to a shell with that index. Conversely, an exact complex in a shell n ≤ B becomes a bounded complex by reattaching the cap proofs. The two maps carry the original incidence data and relabeling witnesses, so they respect the equivalence relations and are inverse to each other. This means the two quotient carriers, the sets of equivalence classes, are in bijection.

Because the bijection preserves automorphism cardinality, the class measure, which weights each class by 1 divided by the size of its automorphism group, is also preserved. The theorem then shows that for any assignment of phases, a real number attached to each exact path class, the sum over the capped quotient equals the sum over the shell range. The statement capShellCompatibility packages this equality as a single property, named CapShellCompatibility, for the phase family induced at every cap.

The theorem does not claim any target sum equality beyond the one proved, nor does it assert any convergence statement, substrate phase, or physical continuum interpretation. It is a structural result about the combinatorics of these complexes, not a claim about the physical meaning of the sums. The bridge is a formal tool that lets the framework move between the capped and shell views without changing the total weighted count.

/-- **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 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 AUTOMORPHISM PRESERVATION.** -/
theorem shellAutCard_capToShell {B : ℕ} (q : TriangulationClass B) :
    shellAutCard (capToShell q).2 = Nat.card (Aut (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)
  obtain ⟨r⟩ := hrel
  have hcap : Equivalent
      (Quotient.out (Quotient.mk (relabelSetoid B) K)) K :=
    PathSum.equivalent_of_mk_eq
      (Quotient.out_eq (Quotient.mk (relabelSetoid B) K))
  obtain ⟨s⟩ := hcap
  dsimp [capToShell, boundedToShell, shellAutCard]
  calc
    Nat.card (ExactAut (Quotient.out qe))
        = Nat.card (ExactAut (toExact K)) := Nat.card_congr r.autCongr
    _ = Nat.card (Aut K) := (autCard_toExact K).symm
    _ = Nat.card (Aut (Quotient.out (Quotient.mk (relabelSetoid B) K))) :=
        (Nat.card_congr s.autCongr).symm

What this page does not claim

No physical continuum interpretation is asserted for the sums. No convergence statement for infinite sums is proved. The theorem does not claim any particular phase assignment is physically meaningful.

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: