Gravity Seven Gaps Class Pushforward First Endpoint Val Edge Ab

The first endpoint value

In the Recognition Science framework, a recognition event, a discrete record of a comparison, can be encoded as a small labeled complex: a collection of points, edges, and triangles with named vertices. The declaration firstEndpointVal_edgeAB is a theorem about one such object, a single edge on two vertices named edgeAB. It states that the value of the function firstEndpointVal on this edge is 0, meaning the edge lists vertex 0 before vertex 1. The proof is immediate from the definition; the declaration is a record of a fact, not a discovery about physics.

The fact matters because of how the framework builds its sums. A path sum, written Z, adds up a weight over every labeled complex. When two complexes are related by relabeling their vertices, the framework treats them as equivalent, and the sum can be reorganized by these equivalence classes. The theorem Z_eq_classPushforward shows that if a weight is constant on each class, the sum over all labeled complexes equals a sum over classes, where each class contributes its total mass, the sum of the weights of its members. At B = 2, the two edges edgeAB and edgeBA are distinct labeled complexes but are equivalent under a vertex swap. Each class contains both, so the class mass is twice the mass of a single member. The theorem mu_lt_classMass_edgeClass proves that the mass of edgeAB alone is strictly less than the mass of its class. The first endpoint value distinguishes the two edges within the class and is part of what makes the labeled sum differ from a sum that counts each class once.

The declaration itself is narrow. It does not claim anything about the continuum limit of the path sum, about deriving the measure from first principles, or about the physical meaning of the endpoint value. Those remain open targets in the framework's library, recorded as flags in its status structure. The theorem is a piece of bookkeeping, a precise statement about a specific labeled complex, and it is proved with no axioms beyond the standard ones of the ambient type theory.

theorem firstEndpointVal_edgeAB : firstEndpointVal edgeAB = 0 := rfl

/-- **T2 (headline).**  For any weight `w` constant on classes (explicit
hypothesis `hw`; note `unitaryWeight S` is class-constant only when `S`
is), the labeled path sum `Z` equals its class pushforward:
`Z B w = Σ_{q : TriangulationClass B} classMass(q) · w(rep q)`.
HONEST SCOPE: `classMass q = |fiber(q)| · (1/|Aut(rep q)|)`
(see `classMass_eq_fiberCard_mul_mu`), NOT `1/|Aut|` per class; this
theorem does NOT equate `Z` with the inequivalent-class sum with weights
`1/|Aut|` (the two weights are separated as a kernel fact by
`mu_lt_classMass_edgeClass`, built on `exists_nonSingleton_fiber`). -/
theorem Z_eq_classPushforward (B : ℕ) (w : BoundedComplex B → ℂ)
    (hw : ∀ K K', Equivalent K K' → w K = w K') :
    Z B w = ∑ q : TriangulationClass B,
      (classMass q : ℂ) * w (Quotient.out q) := by
  unfold Z
  rw [FiniteQuotient.sum_fiberwise_quotient (relabelSetoid B)
    (fun K => (mu K : ℂ) * w K)]
  refine Finset.sum_congr rfl fun q _ => ?_
  have hmem : ∀ K ∈ classFiber (relabelSetoid B) q, Equivalent K (Quotient.out q) := by
    intro K hK
    exact equivalent_of_mk_eq
      (((mem_classFiber (relabelSetoid B) q K).mp hK).trans (Quotient.out_eq q).symm)
  calc ∑ K ∈ classFiber (relabelSetoid B) q, (mu K : ℂ) * w K
      = ∑ K ∈ classFiber (relabelSetoid B) q, (mu K : ℂ) * w (Quotient.out q) := by
        refine Finset.sum_congr rfl fun K hK => ?_
        rw [hw K (Quotient.out q) (hmem K hK)]
    _ = (∑ K ∈ classFiber (relabelSetoid B) q, (mu K : ℂ)) * w (Quotient.out q) := by
        rw [← Finset.sum_mul]
    _ = (classMass q : ℂ) * w (Quotient.out q) := by
        unfold classMass
        rw [Complex.ofReal_sum]

/-- **T3 FORK VERDICT (numeric witness; the formalized detonation).**
At the `B = 2` edge class the labeled measure of a single representative
is STRICTLY BELOW the pushforward class mass:
`μ(edgeAB) < classMass(⟦edgeAB⟧)`.  Hence a path sum carrying weight
`classMass` per class is NOT the per-class `1/|Aut|` sum, as a kernel
fact (via `classMass_eq_fiberCard_mul_mu`, `one_lt_fiberCard_edgeClass`,
`mu_congr`, and `mu_pos`).  This concerns the LABELED `PathSum.Z` object
only. -/
theorem mu_lt_classMass_edgeClass :
    mu edgeAB < classMass (Quotient.mk (relabelSetoid 2) edgeAB) := by
  have hrep : mu (Quotient.out (Quotient.mk (relabelSetoid 2) edgeAB)) =
      mu edgeAB :=
    mu_congr (equivalent_of_mk_eq (Quotient.out_eq _))
  rw [classMass_eq_fiberCard_mul_mu, hrep]
  have hcard : (1 : ℝ) < (fiberCard (relabelSetoid 2)
      (Quotient.mk (relabelSetoid 2) edgeAB) : ℝ) := by
    exact_mod_cast one_lt_fiberCard_edgeClass
  calc mu edgeAB = 1 * mu edgeAB := (one_mul _).symm
    _ < _ * mu edgeAB := mul_lt_mul_of_pos_right hcard (mu_pos edgeAB)

What this page does not claim

The declaration does not claim a continuum limit for the path sum Z. It does not claim that the 1/|Aut| convention is derived from first principles. It does not claim any physical significance for the endpoint value beyond its role in the labeled sum.

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