Encyclopedia Gravity Gravity Seven Gaps Quotient First Z

ARTICLE 5 claims 5 theorems

Gravity Seven Gaps Quotient First Z

A machine-checked module defines a quotient-first path sum and proves exactly when it matches the standing labeled sum, with the difference made explicit.

Verify this page

The quotient-first path sum

A path sum is a way of adding up contributions from many possible routes or configurations, each weighted by a measure. In the Recognition Science framework, the standing object, called the labeled path sum, adds over every individual labeled configuration. The quotient-first object, named Zq, adds instead over equivalence classes: configurations considered the same up to relabeling are counted once, with a symmetry factor that divides by the size of the automorphism group of the representative.

The module proves three things. First, the representative symmetry factor is independent of which representative you pick from a class; any representative gives the same factor. Second, the labeled path sum with a class-constant weight equals the quotient sum weighted by the class mass, which is the fiber size times the representative measure. Third, the exact relation between the two sums is not an unconditional equality: the labeled sum equals the quotient sum plus an explicit excess term, which is the sum over classes of (fiber size minus one) times the measure times the weight.

The key theorem is the iff form: the quotient-first object equals the labeled sum exactly when the fiber excess vanishes. A sufficient condition for this is that every fiber has size one, but the framework inherits a theorem that this condition is false in general: for a particular edge class, the fiber size is strictly greater than one. So the unconditional equality is not available, and the module does not resurrect it.

In Recognition Science, the module is part of the Seven Gaps program, which aims to derive gravity-related structure from the recognition ledger. The quotient-first object is a candidate for the physical path sum, but the bridge to the labeled sum is not yet closed. The status record keeps the relevant flags red: no orbit-stabilizer theorem for the full bounded setoid, no continuum limit, no derived substrate measure, and no gap-1 bridge. These remain open targets, not achievements.

THEOREM mu_out_eq_of_mk_eq · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean
mu_out_eq_of_mk_eq · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean:59 
/-- The representative symmetry factor is independent of the chosen
representative of a triangulation class. -/
theorem mu_out_eq_of_mk_eq {B : ℕ} {K : BoundedComplex B}
    (q : TriangulationClass B) (hK : Quotient.mk (relabelSetoid B) K = q) :
    mu (Quotient.out q) = mu K := by
  exact mu_congr (PathSum.equivalent_of_mk_eq ((Quotient.out_eq q).trans hK.symm))
THEOREM labeledZ_eq_sum_fiberCard_mul_mu · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean
labeledZ_eq_sum_fiberCard_mul_mu · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean:66 
/-- **Bridge to the labeled sum, with the mandatory fiber factor.**  For a
class weight `wq`, the standing labeled path sum with pulled-back weight is
the quotient sum weighted by the pushforward class mass
`|fiber q| · μ(out q)`. -/
theorem labeledZ_eq_sum_fiberCard_mul_mu (B : ℕ)
    (wq : TriangulationClass B → ℂ) :
    Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) =
      ∑ q : TriangulationClass B,
        (((fiberCard (relabelSetoid B) q : ℂ) * (mu (Quotient.out q) : ℂ))
          * wq q) := by
  classical
  have hw : ∀ K K' : BoundedComplex B, Equivalent K K' →
      wq (Quotient.mk (relabelSetoid B) K) =
        wq (Quotient.mk (relabelSetoid B) K') := by
    intro K K' h
    exact congrArg wq (Quotient.sound h)
  calc
    Z B (fun K => wq (Quotient.mk (relabelSetoid B) K))
        = ∑ q : TriangulationClass B,
            (PathSum.classMass q : ℂ) *
              wq (Quotient.mk (relabelSetoid B) (Quotient.out q)) := by
          simpa using PathSum.Z_eq_classPushforward B
            (fun K => wq (Quotient.mk (relabelSetoid B) K)) hw
    _ = ∑ q : TriangulationClass B,
        (((fiberCard (relabelSetoid B) q : ℂ) * (mu (Quotient.out q) : ℂ))
          * wq q) := by
          refine Finset.sum_congr rfl fun q _ => ?_
          rw [PathSum.classMass_eq_fiberCard_mul_mu]
          rw [show wq (Quotient.mk (relabelSetoid B) (Quotient.out q)) = wq q
            from congrArg wq (Quotient.out_eq q)]
          simp only [Complex.ofReal_mul]
          norm_num
THEOREM labeledZ_eq_Zq_plus_fiberExcess · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean
labeledZ_eq_Zq_plus_fiberExcess · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean:107 
/-- **Exact relation.**  The labeled class-constant path sum is the
quotient-first path sum plus the labeled-fiber excess.  This is the honest
replacement for the killed unconditional claim `Z = Σ_q wq/|Aut q|`. -/
theorem labeledZ_eq_Zq_plus_fiberExcess (B : ℕ)
    (wq : TriangulationClass B → ℂ) :
    Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) =
      Zq B wq + fiberExcess B wq := by
  classical
  rw [labeledZ_eq_sum_fiberCard_mul_mu, Zq, fiberExcess, ← Finset.sum_add_distrib]
  refine Finset.sum_congr rfl fun q _ => ?_
  let f : ℂ := fiberCard (relabelSetoid B) q
  let m : ℂ := mu (Quotient.out q)
  let z : ℂ := wq q
  calc
    (((fiberCard (relabelSetoid B) q : ℂ) * (mu (Quotient.out q) : ℂ)) * wq q)
        = (f * m) * z := rfl
    _ = m * z + ((f - 1) * m) * z := by ring
    _ = (mu (Quotient.out q) : ℂ) * wq q +
        ((((fiberCard (relabelSetoid B) q : ℂ) - 1) *
          (mu (Quotient.out q) : ℂ)) * wq q) := rfl
THEOREM Zq_eq_labeledZ_iff_fiberExcess_vanishes · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean
Zq_eq_labeledZ_iff_fiberExcess_vanishes · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean:128 
/-- **IFF form of the exact relation.**  The quotient-first object equals
the standing labeled sum for a pulled-back class weight exactly when the
explicit fiber excess vanishes. -/
theorem Zq_eq_labeledZ_iff_fiberExcess_vanishes (B : ℕ)
    (wq : TriangulationClass B → ℂ) :
    Zq B wq = Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) ↔
      fiberExcess B wq = 0 := by
  rw [labeledZ_eq_Zq_plus_fiberExcess]
  constructor
  · intro h
    have h' : Zq B wq + fiberExcess B wq = Zq B wq + 0 := by
      simpa using h.symm
    exact add_left_cancel h'
  · intro h
    rw [h, add_zero]
THEOREM Zq_eq_labeledZ_of_singleton_fibers · quotientFirstStatus_grounded · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean
Zq_eq_labeledZ_of_singleton_fibers · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean:144 
/-- A sufficient singleton-fiber condition under which the quotient-first
object agrees with the labeled sum.  `ClassPushforward` proves this
condition is false in general (`PathSum.one_lt_fiberCard_edgeClass`). -/
theorem Zq_eq_labeledZ_of_singleton_fibers (B : ℕ)
    (wq : TriangulationClass B → ℂ)
    (hfiber : ∀ q : TriangulationClass B,
      fiberCard (relabelSetoid B) q = 1) :
    Zq B wq = Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) := by
  rw [Zq_eq_labeledZ_iff_fiberExcess_vanishes]
  unfold fiberExcess
  refine Finset.sum_eq_zero fun q _ => ?_
  rw [hfiber q]
  norm_num
quotientFirstStatus_grounded · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean:189 
/-- **Grounding theorem.**  The status flags are tied to the constructed
object and kernel bridges.  The RED flags remain false, and the inherited
non-singleton fiber theorem records why the unconditional labeled/quotient
equality is not available. -/
theorem quotientFirstStatus_grounded :
    (quotientFirstStatus.quotient_first_object_constructed = true ∧
      ∀ B : ℕ, ∀ wq : TriangulationClass B → ℂ,
        Zq B wq = ∑ q : TriangulationClass B,
          (mu (Quotient.out q) : ℂ) * wq q) ∧
    (quotientFirstStatus.labeled_bridge_has_fiber_factor = true ∧
      ∀ B : ℕ, ∀ wq : TriangulationClass B → ℂ,
        Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) =
          ∑ q : TriangulationClass B,
            (((fiberCard (relabelSetoid B) q : ℂ) * (mu (Quotient.out q) : ℂ))
              * wq q)) ∧
    (quotientFirstStatus.exact_excess_relation_proved = true ∧
      ∀ B : ℕ, ∀ wq : TriangulationClass B → ℂ,
        Zq B wq = Z B (fun K => wq (Quotient.mk (relabelSetoid B) K)) ↔
          fiberExcess B wq = 0) ∧
    (quotientFirstStatus.nonSingleton_fiber_inherited = true ∧
      1 < fiberCard (relabelSetoid 2)
        (Quotient.mk (relabelSetoid 2) PathSum.edgeAB)) ∧
    quotientFirstStatus.bounded_orbit_stabilizer_derived = false ∧
    quotientFirstStatus.Z_RS_continuum_limit = false ∧
    quotientFirstStatus.substrate_measure_derived = false ∧
    quotientFirstStatus.gap1_bridge_derived = false :=
  ⟨⟨rfl, fun _ _ => rfl⟩,
    ⟨rfl, labeledZ_eq_sum_fiberCard_mul_mu⟩,
    ⟨rfl, Zq_eq_labeledZ_iff_fiberExcess_vanishes⟩,
    ⟨rfl, PathSum.one_lt_fiberCard_edgeClass⟩,
    rfl, rfl, rfl, rfl⟩

What this page does not claim

The quotient-first object equals the labeled sum unconditionally. The 1/|Aut| symmetry measure is derived rather than chosen as a model input. The module derives the continuum limit or the substrate 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/QuotientFirstZ.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