Encyclopedia Gravity Gravity Seven Gaps Regulator Removal No Go Orbit Card Mul Aut Card

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Regulator Removal No Go Orbit Card Mul Aut Card

A counting identity about symmetries of labeled objects, proved in the framework's machine-checked library, sets up a no-go result for a path-sum regulator.

Verify this page

The orbit-stabilizer identity

In combinatorics, the orbit-stabilizer theorem relates the size of a group, the size of an orbit of an object under that group, and the size of the stabilizer, the subgroup that leaves the object fixed. The Recognition Science declaration orbitCard_mul_autCard is a formal, kernel-checked instance of this classical theorem for a specific class of objects: exact complexes, which are finite combinatorial structures built from vertices, edges, and tetrahedra. It states that for any such complex, the number of distinct complexes globally equivalent to it (its orbit) multiplied by the number of its automorphisms (its relabeling symmetries) equals the total number of ways to independently permute its vertices, edges, and tetrahedra. In symbols, for a complex with v vertices, e edges, and t tetrahedra, the identity is orbitCard(K) * |Aut(K)| = v! * e! * t!.

This identity is not an isolated curiosity. It is the key step in proving a shell-mass identity: the sum over equivalence classes of the per-class measure 1/|Aut| equals the total number of labeled complexes divided by the full relabeling gauge volume v!·e!·t!. That identity, in turn, feeds a lower bound on a quantity called shell mass, showing it grows without bound as the complexity n increases. The growth is dramatic: shellMass n is at least n^(3n). This unboundedness is the engine behind the framework's headline result, a no-go theorem for a Gaussian-regulated quotient path sum at zero phase. The theorem proves that this regulated sum has no limit as the regulator is removed, because the positive contributions from individual shells overwhelm any proposed finite limit.

In Recognition Science, this no-go result is a kernel-checked refutation of a specific regulator-removal procedure, not a claim about the physical continuum limit. The framework models a discrete ledger of recognition events, and this result concerns a particular quotient-sum convention for path sums over exact complexes. The declaration and its surrounding theorems are proved in the framework's machine-checked library, with zero unproved axioms beyond the standard logical basis. The no-go statement is precise: it refutes the existence of a limit for the regulated sum at zero phase, where all terms are real and nonnegative.

What the declaration does not claim is as important as what it proves. It says nothing about oscillatory phases, where terms carry complex phases and cancellation might allow a limit; that case remains an explicitly named open problem. It also does not address the physical continuum limit, since the complexity cutoff here is not mesh refinement. The identity itself is a theorem about finite combinatorial structures, not a physical law. It is a tool, proved rigorously, that establishes a negative result about a particular mathematical procedure within the framework's model.

THEOREM orbitCard_mul_autCard · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean
orbitCard_mul_autCard · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean:252 
/-- **THEOREM (orbit-stabilizer, exact form).**  Orbit size times
automorphism count equals the full gauge volume `v!·e!·t!` for EVERY
labeled complex. -/
theorem orbitCard_mul_autCard (K : ExactComplex v e t) :
    orbitCard K * Nat.card (ExactAut K)
      = v.factorial * e.factorial * t.factorial := by
  rw [← sum_card_relabel_eq_orbit K]
  exact sum_card_relabel K
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

This answer does not claim the orbit-stabilizer identity is a physical law; it is a theorem about finite combinatorial structures. This answer does not claim the no-go result applies to oscillatory phases; that case is an open problem. This answer does not claim the regulator removal result says anything about the physical continuum limit.

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