Encyclopedia Gravity Gravity Seven Gaps Regulator Removal No Go Sum Card Relabel Eq Orbit

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Regulator Removal No Go Sum Card Relabel Eq Orbit

A machine-checked proof shows that when you count physical configurations by their symmetries, the total is exactly the labeled count divided by the number of ways to relabel the parts.

Verify this page

Counting by symmetry

In combinatorics, when objects come with symmetries, you can count them two ways: by listing every labeled object, or by grouping them into equivalence classes and counting each class once. The theorem sum_card_relabel_eq_orbit proves these two counts agree in a precise sense for a certain class of geometric complexes. It states that for any complex with v vertices, e edges, and t tetrahedra, the sum over all complexes of the number of relabelings from a fixed base complex equals the size of its orbit (the number of complexes reachable by relabeling) multiplied by the size of its automorphism group (the relabelings that leave it unchanged).

This is a Burnside-style identity, a standard tool in group theory. The proof works by constructing a torsor: a bijection between the set of all relabeling triples and the disjoint union over all target complexes of the relabelings from the base to that target. This torsor splits the relabeling group into fibers, one per orbit, and the orbit-stabilizer theorem then counts each fiber. The result is a clean equality: the total number of relabeling triples equals the orbit size times the automorphism group size. A corollary, sum_classMuOn_eq_card_div_factorials, divides by the full relabeling gauge volume v!·e!·t! to get the per-class measure 1/|Aut|.

In Recognition Science, this identity is not an isolated counting curiosity. It feeds a shell-mass calculation: the sum of per-class measures over all classes equals the labeled count divided by the gauge volume. The framework proves this shell mass grows without bound, at least n^(3n) for the signature (n,n,n). That unbounded growth is the mechanism behind a no-go theorem: at zero phase, the Gaussian-regulated quotient path sum has no limit as the regulator is removed. Every regulated term is real and nonnegative, so a single shell with mass greater than any proposed limit forces a contradiction.

What the theorem does not claim is equally important. It says nothing about oscillatory phases, where cancellation between unit phases might rescue regulator removal; that remains an open question. It does not establish anything about a physical continuum limit, since the complexity cutoff is not mesh refinement. And it does not equate the quotient-sum convention with the labeled-sum convention of another path-sum measure; the two are distinct and must not be conflated.

THEOREM sum_card_relabel_eq_orbit · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean
sum_card_relabel_eq_orbit · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean:224 
/-- Summing witness counts over all targets factorizes through the orbit:
each on-orbit fiber is an `Aut`-torsor, each off-orbit fiber is empty. -/
theorem sum_card_relabel_eq_orbit (K : ExactComplex v e t) :
    ∑ K' : ExactComplex v e t, Nat.card (ExactRelabel K K')
      = orbitCard K * Nat.card (ExactAut K) := by
  classical
  calc ∑ K' : ExactComplex v e t, Nat.card (ExactRelabel K K')
      = ∑ K' : ExactComplex v e t,
          (if GlobalEquivalent K K' then Nat.card (ExactAut K) else 0) := by
        refine Finset.sum_congr rfl fun K' _ => ?_
        by_cases h : GlobalEquivalent K K'
        · rw [if_pos h]
          obtain ⟨r0⟩ := h
          exact (Nat.card_congr (torsorEquiv r0)).symm
        · rw [if_neg h]
          haveI : IsEmpty (ExactRelabel K K') := ⟨fun r => h ⟨r⟩⟩
          exact Nat.card_of_isEmpty
    _ = ∑ K' ∈ Finset.univ.filter (fun K' => GlobalEquivalent K K'),
          Nat.card (ExactAut K) := (Finset.sum_filter _ _).symm
    _ = (Finset.univ.filter (fun K' => GlobalEquivalent K K')).card
          * Nat.card (ExactAut K) := by
        rw [Finset.sum_const, smul_eq_mul]
    _ = orbitCard K * Nat.card (ExactAut K) := by
        congr 1
        show (Finset.univ.filter (fun K' => GlobalEquivalent K K')).card
            = Nat.card {K' : ExactComplex v e t // GlobalEquivalent K K'}
        rw [Nat.card_eq_fintype_card, Fintype.card_subtype]
THEOREM sum_classMuOn_eq_card_div_factorials · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean
sum_classMuOn_eq_card_div_factorials · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean:310 
/-- **HEADLINE IDENTITY (Burnside / orbit-stabilizer route).**  At every
exact signature, the total per-class measure equals the labeled count
divided by the full gauge volume:
`∑_classes 1/|Aut| = |labeled| / (v!·e!·t!)`. -/
theorem sum_classMuOn_eq_card_div_factorials (v e t : ℕ) :
    ∑ c : Quotient (exactSetoid v e t), classMuOn v e t c
      = (Fintype.card (ExactComplex v e t) : ℝ)
        / ((v.factorial * e.factorial * t.factorial : ℕ) : ℝ) := by
  classical
  have hfactpos : 0 < v.factorial * e.factorial * t.factorial :=
    Nat.mul_pos (Nat.mul_pos v.factorial_pos e.factorial_pos) t.factorial_pos
  have hfactR : (0 : ℝ) < ((v.factorial * e.factorial * t.factorial : ℕ) : ℝ) := by
    exact_mod_cast hfactpos
  rw [eq_div_iff hfactR.ne', Finset.sum_mul]
  have hterm : ∀ c : Quotient (exactSetoid v e t),
      classMuOn v e t c * ((v.factorial * e.factorial * t.factorial : ℕ) : ℝ)
        = (orbitCard (Quotient.out c) : ℝ) := by
    intro c
    have hOS := orbitCard_mul_autCard (Quotient.out c)
    have hautpos : (0 : ℝ) < (Nat.card (ExactAut (Quotient.out c)) : ℝ) := by
      exact_mod_cast exactAutCard_pos (Quotient.out c)
    have hcast : (orbitCard (Quotient.out c) : ℝ)
        * (Nat.card (ExactAut (Quotient.out c)) : ℝ)
        = ((v.factorial * e.factorial * t.factorial : ℕ) : ℝ) := by
      exact_mod_cast congrArg (Nat.cast : ℕ → ℝ) hOS
    rw [classMuOn_out c]
    unfold exactMu
    rw [div_mul_eq_mul_div, one_mul, ← hcast, mul_div_assoc,
      div_self hautpos.ne', mul_one]
  rw [Finset.sum_congr rfl fun c _ => hterm c, ← Nat.cast_sum]
  exact_mod_cast congrArg (Nat.cast : ℕ → ℝ) (sum_orbitCard v e t)
THEOREM shellMass_lower · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean
shellMass_lower · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean:384 
/-- **Quantitative shell-mass lower bound.**
`shellMass n ≥ n^(6n)/(n!)³ ≥ n^(3n)`: the labeled entropy of the cube
signature beats its factorial gauge volume. -/
theorem shellMass_lower (n : ℕ) :
    ((n : ℝ)) ^ (3 * n) ≤ shellMass n := by
  have hfact3 : n.factorial * n.factorial * n.factorial ≤ n ^ (3 * n) := by
    have h := Nat.factorial_le_pow n
    calc n.factorial * n.factorial * n.factorial
        ≤ n ^ n * n ^ n * n ^ n := Nat.mul_le_mul (Nat.mul_le_mul h h) h
      _ = n ^ (3 * n) := by
          rw [← pow_add, ← pow_add]
          congr 1
          omega
  have hcard : Fintype.card (ExactComplex n n n) = n ^ (6 * n) := by
    rw [exactComplex_card_eq, ← pow_two, ← pow_mul, ← pow_mul, ← pow_add]
    congr 1
    omega
  have hfactR : (0 : ℝ) < ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ) := by
    exact_mod_cast
      Nat.mul_pos (Nat.mul_pos n.factorial_pos n.factorial_pos) n.factorial_pos
  have hkey : ((n : ℝ)) ^ (3 * n)
      ≤ (Fintype.card (ExactComplex n n n) : ℝ)
        / ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ) := by
    rw [le_div_iff₀ hfactR]
    calc ((n : ℝ)) ^ (3 * n)
          * ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ)
        ≤ ((n : ℝ)) ^ (3 * n) * ((n : ℝ)) ^ (3 * n) := by
          refine mul_le_mul_of_nonneg_left ?_ (by positivity)
          calc ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ)
              ≤ ((n ^ (3 * n) : ℕ) : ℝ) := by exact_mod_cast hfact3
            _ = ((n : ℝ)) ^ (3 * n) := Nat.cast_pow n (3 * n)
      _ = ((n : ℝ)) ^ (6 * n) := by
          rw [← pow_add]
          congr 1
          omega
      _ = ((n ^ (6 * n) : ℕ) : ℝ) := (Nat.cast_pow n (6 * n)).symm
      _ = (Fintype.card (ExactComplex n n n) : ℝ) := by rw [hcard]
  calc ((n : ℝ)) ^ (3 * n)
      ≤ (Fintype.card (ExactComplex n n n) : ℝ)
          / ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ) := hkey
    _ = ∑ q : Quotient (exactSetoid n n n), classMuOn n n n q :=
        (sum_classMuOn_eq_card_div_factorials n n n).symm
    _ ≤ shellMass n := cube_sum_le_shellMass n
THEOREM not_hasZRSRegulatorRemoval_zeroPhase · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean
not_hasZRSRegulatorRemoval_zeroPhase · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean:469 
/-- **HEADLINE (kernel no-go).**  Regulator removal FAILS at zero phase:
the Gaussian-regulated quotient path sum `Z_RS_uv ρ zeroPhase` has NO
limit as `ρ → 0⁺`.  Mechanism: any putative limit `L` is beaten by a
single shell of mass `> L.re + 2` (shell masses diverge), whose regulated
contribution tends to its full mass as the regulator is removed. -/
theorem not_hasZRSRegulatorRemoval_zeroPhase :
    ¬ HasZRSRegulatorRemoval zeroPhase := by
  rintro ⟨L, hL⟩
  have hre : Filter.Tendsto (fun ρ : ℝ => (Z_RS_uv ρ zeroPhase).re)
      (nhdsWithin 0 (Set.Ioi 0)) (nhds L.re) :=
    (Complex.continuous_re.tendsto L).comp hL
  obtain ⟨n₀, hn₀⟩ := shellMass_unbounded (L.re + 2)
  have hexp : Filter.Tendsto
      (fun ρ : ℝ => Real.exp (-ρ * (n₀ : ℝ) ^ 2) * shellMass n₀)
      (nhdsWithin 0 (Set.Ioi 0)) (nhds (shellMass n₀)) := by
    refine Filter.Tendsto.mono_left ?_ nhdsWithin_le_nhds
    refine Continuous.tendsto' ?_ 0 (shellMass n₀) ?_
    · exact (Real.continuous_exp.comp
        (continuous_neg.mul continuous_const)).mul continuous_const
    · simp only [neg_zero, zero_mul, Real.exp_zero, one_mul]
  have hev1 : ∀ᶠ ρ in nhdsWithin (0 : ℝ) (Set.Ioi 0),
      L.re + 1 < Real.exp (-ρ * (n₀ : ℝ) ^ 2) * shellMass n₀ :=
    hexp.eventually_const_lt (by linarith)
  have hev2 : ∀ᶠ ρ in nhdsWithin (0 : ℝ) (Set.Ioi 0),
      (Z_RS_uv ρ zeroPhase).re < L.re + 1 :=
    hre.eventually_lt_const (by linarith)
  have hev3 : ∀ᶠ ρ in nhdsWithin (0 : ℝ) (Set.Ioi 0), ρ ∈ Set.Ioi (0 : ℝ) :=
    eventually_mem_nhdsWithin
  obtain ⟨ρ, ⟨h1, h2⟩, h3⟩ := ((hev1.and hev2).and hev3).exists
  have h4 := single_shell_re_lower_bound ρ (Set.mem_Ioi.mp h3) n₀
  linarith

What this page does not claim

Nothing is claimed about oscillatory phases, where regulator removal remains an open problem. The theorem does not establish a physical continuum limit, since the complexity cutoff is not mesh refinement. The quotient-sum convention is not silently equated with the labeled-sum convention of another path-sum measure.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND