Encyclopedia Gravity Gravity Seven Gaps Quotient First Z Quotient First Status Grounded

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Quotient First Z Quotient First Status Grounded

A machine-checked status record for a path-sum construction: which bridges are proved, which are not, and why the unconditional equality was killed.

Verify this page

The grounded status record

A path sum is a way of adding up contributions from many possible configurations, here triangulations of a surface, to get a single number. The declaration quotientFirstStatus_grounded is a machine-checked status record for one such path sum, built by grouping triangulations into classes under relabeling. It states plainly which parts of the construction are proved and which are not, with no unproved assumptions hidden inside.

The record proves three positive facts. First, the quotient-first object Zq is constructed: it sums over classes, weighting each by a symmetry factor evaluated on a chosen representative. Second, the standing labeled path sum, when given a class-constant weight, equals the quotient sum multiplied by the size of each class's fiber, the number of labeled triangulations in that class. Third, the exact relation between the two is not an unconditional equality: the labeled sum equals the quotient sum plus an explicit excess term, and the two agree exactly when that excess vanishes.

The status record also keeps four flags false. It does not derive an orbit-stabilizer theorem for the full bounded setoid, does not reach a continuum limit, does not derive the substrate measure, and does not bridge gap 1. The ledger, a discrete record of events, here the triangulations, keeps these negative results visible rather than burying them.

In Recognition Science, the framework models physical structure through such discrete records and their sums. This declaration establishes that the quotient-first path sum is a well-defined object with a proved bridge to the labeled sum, but that the bridge carries a mandatory fiber factor. The unconditional claim that the labeled sum equals the per-class 1/|Aut| quotient sum was killed by the P2c panel and is not resurrected here.

THEOREM Zq · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean
Zq · IndisputableMonolith/Gravity/SevenGaps/QuotientFirstZ.lean:52 
/-- The quotient-first path sum over triangulation classes, with the
per-class symmetry-factor measure evaluated on the chosen representative.
This is the quotient convention, not the standing labeled `PathSumMeasure.Z`.
-/
noncomputable def Zq (B : ℕ) (wq : TriangulationClass B → ℂ) : ℂ :=
  ∑ q : TriangulationClass B, (mu (Quotient.out q) : ℂ) * wq q
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 · Zq_eq_labeledZ_iff_fiberExcess_vanishes · 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
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 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⟩

What this page does not claim

No orbit-stabilizer theorem for the full bounded setoid is derived here. The quotient-first object does not equal the labeled sum unconditionally; the fiber excess is not assumed to vanish. The 1/|Aut| measure is a model input, not a derived result.

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