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

The carrier bridge

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition is the act of matching a new event to a stored one. The framework models physical structure by counting such recognitions. This page concerns a technical bridge between two ways of organizing the ledger's objects: bounded complexes and exact shells.

A complex here is a triangulated space built from vertices, edges, and tetrahedra. A bounded complex has a complexity value, the maximum of its counts of vertices, edges, and tetrahedra, that does not exceed some cap B. An exact shell is a complex whose complexity is exactly n, for some n. The two organizations differ: the bounded view collects everything up to a cap, the exact view separates by precise size. The bridge, named boundedToShell_exactToBounded, proves that these two views are equivalent.

Specifically, the theorem shows that if you take an exact complex in shell n, with n at most B, and convert it to a bounded complex by attaching the cap proofs, then converting it back to a shell returns the original exact complex. The two maps carry the incidence data and relabeling witnesses, so they descend to the quotient carriers and are inverse there. This means the finite sum over all shells up to B equals the sum over the bounded carrier, a result called capShellCompatibility. The bridge preserves automorphism cardinality and hence the class measure, the 1 divided by the number of automorphisms.

In Recognition Science, this bridge is a load-bearing step. It shows that the partition function, the sum of weighted phases over all complexes, does not depend on whether you organize the sum by cap or by shell. This is a formal theorem, machine-checked in the framework's library. It is not a statement about physics directly; it is a statement about the mathematics of the ledger.

What the bridge does not claim is equally precise. It does not assume any target sum equality, convergence statement, substrate phase, or physical continuum interpretation. It is a carrier equivalence, not a physical law. The theorem holds for any phase function, any assignment of real numbers to exact path classes. The bridge is a tool for organizing the ledger, not a claim about what the ledger contains.

/-- Forgetting the cap after attaching it returns the original exact-shell
class.  Proof fields disappear by proof irrelevance; incidence data is
unchanged. -/
theorem boundedToShell_exactToBounded {B n : ℕ} (hn : n ≤ B)
    (s : ShellSig n) (K : ExactComplex (sigV s) (sigE s) (sigT s)) :
    boundedToShell (exactToBounded hn s K) =
      ⟨⟨n, Nat.lt_succ_of_le hn⟩, s, Quotient.mk _ K⟩ := by
  rcases s with ⟨⟨v, e, t⟩, hs⟩
  rcases v with ⟨v, hv⟩
  rcases e with ⟨e, he⟩
  rcases t with ⟨t, ht⟩
  dsimp only [sigV, sigE, sigT] at K ⊢
  dsimp only at hs
  subst n
  simp [boundedToShell, boundedShellIndex, boundedShellSig, exactToBounded,
    sigV, sigE, sigT, complexity]
  exact Quotient.sound ⟨ExactRelabel.refl K⟩

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

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

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

What this page does not claim

The bridge does not assume any convergence statement or physical continuum interpretation. The theorem does not claim that any particular phase function is physically realized. The bridge does not establish that bounded and exact complexes are identical as data, only equivalent as carriers.

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: