Gravity Seven Gaps Cap Shell Bridge Shell Aut Card Cap To Shell

The shell automorphism bridge

In the Recognition Science framework, physical structure is built from a discrete record of recognition events, called a ledger. One of the framework's tools is the study of triangulated complexes, which are spaces built from vertices, edges, and tetrahedra. These complexes come in two related forms: bounded complexes, whose size is capped by a number B, and exact complexes, which are organized into shells by their complexity. The theorem shellAutCard_capToShell establishes that the number of symmetries, or automorphisms, of a complex is the same whether you count it in the bounded or the exact-shell setting.

The theorem is a formal statement in the machine-checked library of formal theorems that the framework maintains. It states that for any triangulation class q up to cap B, the automorphism cardinality of the shell associated to q equals the automorphism cardinality of q itself. In plainer terms, if you take a bounded complex, convert it to its exact-shell form, and count the symmetries of that shell, you get the same number as if you counted the symmetries of the original bounded complex directly. This is a coherence result: the two descriptions of the same underlying structure agree on their symmetry counts.

The theorem is part of a bridge between two ways of organizing triangulated spaces. The bridge is a bijection between bounded complexes up to cap B and exact shells up to B, meaning each bounded complex corresponds to exactly one shell and vice versa. The theorem shellAutCard_capToShell shows that this bijection preserves the number of symmetries. This matters because the framework uses the reciprocal of the automorphism count, the 1/|Aut| class measure, as a weight in its sums over complexes. If the bridge did not preserve this count, the sums would not agree between the two descriptions.

The framework proves this bridge as a theorem, not as an assumption. The result is established in the Lean 4 proof assistant, with the proof checked by the kernel. The theorem is one of several in the CapShellBridge module that together show the capped-quotient and exact-shell carrier descriptions of triangulated spaces are equivalent. This equivalence is a technical but necessary step in the framework's larger program of deriving physical constants from the ledger structure.

The theorem does not claim anything about the physical interpretation of these complexes. It does not say that triangulated complexes are spacetime, nor that the automorphism counts correspond to any measured physical quantity. It is a purely combinatorial and algebraic statement about the structure of the framework's own objects. The bridge is a formal tool, and its consequences for physics are a separate question that the framework addresses elsewhere, if at all.

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

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

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

What this page does not claim

The theorem does not claim that triangulated complexes represent physical spacetime. The theorem does not claim that automorphism counts correspond to any measured physical quantity. The theorem does not claim any physical continuum interpretation of the bridge.

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: