Gravity Seven Gaps Exact Shell Gauge Uv Norm Z Rsuvshell Le Entropy

The regularized shell bound

In the Recognition Science framework's study of discrete gravity, the central object is a path sum over configurations of abstract complexes. A complexity shell collects all configurations with the same complexity, measured as the largest of three counts: vertices, edges, and tetrahedra. The declaration norm_zRSUVShell_le establishes a bound on the size of each shell's contribution to the regularized sum. It proves that the norm of each shell term is bounded by a quantity that decays fast enough for the whole series to converge.

The regulator is a Gaussian factor exp(−ρ·n²) inserted by hand, where n is the shell index and ρ is a positive strength. This is a mathematical device, not derived physics. The theorem proves that for every ρ > 0, the shell series is summable, meaning the partial sums approach a finite limit. This convergence is the key technical result: it makes the regularized path sum a well-defined complex number for any choice of phase function on the equivalence classes.

What the theorem does not claim is just as important. The regulator is not derived from any physical principle; it is a chosen mathematical tool. The action or phase entering the sum is a parameter, an arbitrary function on equivalence classes, not a derived physical action. Removing the regulator, the limit as ρ approaches zero from above, is a named open problem, explicitly not claimed. The theorem also does not establish any physical continuum limit, since the complexity cutoff is not mesh refinement.

The bound itself is modest in form: the number of classes in shell n is at most (n+1)^(12·(n+1)), and each class carries a measure of 1 divided by the size of its automorphism group. The convergence theorem builds on these ingredients to show the regulated sum is finite. At zero phase, the sum is real and strictly positive, a non-vacuity check that the construction actually produces a meaningful object rather than an empty formalism.

In Recognition Science, this result is a foundation stone for the seven-gaps program: it shows the regularized path sum is mathematically well-behaved. What it leaves open is the physical interpretation. The framework models the path sum as a discrete ledger of recognition events, but the bridge from this combinatorial structure to continuous spacetime is not made here. That bridge remains a target, not a claim.

/-- The complexity of an exact complex: determined by its signature alone. -/
def exactComplexity {v e t : ℕ} (_ : ExactComplex v e t) : ℕ :=
  max v (max e t)

/-- **THEOREM (shell entropy bound, S1c).**  The number of combinatorially
distinct exact complexes of complexity `n` is at most `(n+1)^(12·(n+1))`.
Counting audit: `≤ (n+1)³` signature choices (`shellSig_card_le`), times
`≤ (n+1)^(6·(n+1))` labeled configurations per signature
(`exactComplex_card_le`, quotient card ≤ labeled card via the surjection
`Quotient.mk`), and `3 + 6·(n+1) ≤ 12·(n+1)`. -/
theorem exactPathClass_card_le (n : ℕ) :
    Nat.card (ExactPathClass n) ≤ (n + 1) ^ (12 * (n + 1)) := by
  have hfiber : ∀ s : ShellSig n,
      Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s))) ≤
        (n + 1) ^ (6 * (n + 1)) := by
    intro s
    have hsurj : Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s))) ≤
        Nat.card (ExactComplex (sigV s) (sigE s) (sigT s)) :=
      Nat.card_le_card_of_surjective
        (Quotient.mk (exactSetoid (sigV s) (sigE s) (sigT s)))
        (fun q => Quotient.exists_rep q)
    have hlab : Nat.card (ExactComplex (sigV s) (sigE s) (sigT s)) ≤
        (n + 1) ^ (6 * (n + 1)) := by
      rw [Nat.card_eq_fintype_card]
      exact exactComplex_card_le n _ _ _ (le_of_lt s.1.1.isLt)
        (le_of_lt s.1.2.1.isLt) (le_of_lt s.1.2.2.isLt)
    exact le_trans hsurj hlab
  rw [Nat.card_sigma]
  calc ∑ s : ShellSig n,
        Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s)))
      ≤ ∑ _s : ShellSig n, (n + 1) ^ (6 * (n + 1)) :=
        Finset.sum_le_sum fun s _ => hfiber s
    _ = Fintype.card (ShellSig n) * (n + 1) ^ (6 * (n + 1)) := by
        rw [Finset.sum_const, Finset.card_univ, smul_eq_mul]
    _ ≤ (n + 1) ^ 3 * (n + 1) ^ (6 * (n + 1)) :=
        Nat.mul_le_mul_right _ (shellSig_card_le n)
    _ = (n + 1) ^ (3 + 6 * (n + 1)) := by rw [← pow_add]
    _ ≤ (n + 1) ^ (12 * (n + 1)) :=
        Nat.pow_le_pow_right (Nat.succ_pos n) (by omega)

/-- **THEOREM (S2e, non-vacuity).**  At zero phase the regulated path sum
has strictly positive real part for every `ρ > 0`: the regulated theory
is not the zero functional.  (All terms are nonnegative real and the
`n = 0` term is positive; positivity passes to the `tsum`.) -/
theorem Z_RS_uv_zeroPhase_re_pos (ρ : ℝ) (hρ : 0 < ρ) :
    0 < (Z_RS_uv ρ zeroPhase).re := by
  have hsC : Summable
      (fun n : ℕ => ((Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ)) :=
    (summable_zRSUVShell ρ hρ zeroPhase).congr
      (fun n => zRSUVShell_zeroPhase_eq ρ n)
  have hsR : Summable
      (fun n : ℕ => Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n) :=
    Complex.summable_ofReal.mp hsC
  have hZ : Z_RS_uv ρ zeroPhase =
      ((∑' n : ℕ, Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ) := by
    unfold Z_RS_uv
    rw [tsum_congr (fun n => zRSUVShell_zeroPhase_eq ρ n),
      ← Complex.ofReal_tsum]
  rw [hZ, Complex.ofReal_re]
  exact hsR.tsum_pos
    (fun n => (mul_pos (Real.exp_pos _) (shellMass_pos n)).le) 0
    (mul_pos (Real.exp_pos _) (shellMass_pos 0))

What this page does not claim

The regulator is not derived from physics; it is a mathematical insertion. The action or phase is a parameter, not a derived physical quantity. Regulator removal and the physical continuum limit are open problems, not results.

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/ExactShellGaugeUV.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: