Encyclopedia Gravity Gravity Seven Gaps Quotient First Z Quotient First Status

ARTICLE 4 claims 3 theorems 1 model

Gravity Seven Gaps Quotient First Z Quotient First Status

A formal status record for a path-sum object: what is proved, what is a model input, and which bridges remain open.

Verify this page

The quotient-first status record

In Recognition Science, a path sum is a way of adding up contributions from many possible histories or configurations, each weighted by a measure. The declaration QuotientFirstStatus is a formal record, a list of named flags, that states exactly which parts of one such path-sum construction are proved and which are not. It is a status report, not a new physical law.

The construction in question groups configurations into classes, where two configurations belong to the same class if one can be relabeled into the other. The quotient-first object, called Zq, sums over these classes directly. The record establishes three proved facts. First, the object Zq is constructed and equals a sum over classes of the measure times the weight. Second, the standing labeled path sum, which sums over individual configurations, relates to Zq through an explicit fiber factor: the number of configurations in each class. Third, the exact relation between Zq and the labeled sum is an equality plus an explicit excess term, and the two agree exactly when that excess vanishes.

The record also states what is not established. It does not prove a full orbit-stabilizer theorem for the bounded setoid, meaning there is no single global relabeling group action supplied. The 1/|Aut| measure, the symmetry factor dividing by the size of the automorphism group, remains a model input, not a derived result. The record keeps four flags false: the continuum limit of Z, the derivation of the substrate measure, and the gap1 bridge are all open targets.

What this means in practice: the framework's library has an honest boundary. It proves the quotient-first object and its exact relation to the labeled sum, but it does not claim an unconditional equality between them. The non-singleton fiber fact, inherited from another module, shows why that unconditional claim fails: some classes contain more than one configuration, so the fiber factor does not cancel in general.

THEOREM quotientFirstStatus_grounded · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean
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⟩
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
MODEL quotientFirstStatus · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean
quotientFirstStatus · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean:178 
/-- The canonical status record for this quotient-first module. -/
def quotientFirstStatus : QuotientFirstStatus where
  quotient_first_object_constructed := true
  labeled_bridge_has_fiber_factor := true
  exact_excess_relation_proved := true
  nonSingleton_fiber_inherited := true
  bounded_orbit_stabilizer_derived := false
  Z_RS_continuum_limit := false
  substrate_measure_derived := false
  gap1_bridge_derived := false

What this page does not claim

This answer does not claim that the quotient-first object equals the labeled sum unconditionally. This answer does not claim that the 1/|Aut| measure is derived from the forcing chain. This answer does not claim that any continuum limit or substrate measure is established.

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