Encyclopedia Gravity Gravity Seven Gaps Class Pushforward Class Pushforward Status Flags
ARTICLE 5 claims 5 theorems
Gravity Seven Gaps Class Pushforward Class Pushforward Status Flags
A machine-checked status board records which parts of a path-sum decomposition are proved theorems and which remain open targets.
Status flags
In mathematics, a path sum adds up values assigned to each object in a collection. The Recognition Science framework's ledger, a discrete record of such objects, here concerns bounded complexes, which are finite arrangements of points, edges, and triangles. The declaration classPushforwardStatus_flags is a machine-checked status board. It records, as a single theorem, exactly which pieces of a certain path-sum decomposition have been proved and which have not.
The proved pieces form a clean story about grouping objects into classes. When two complexes differ only by relabeling their vertices, they belong to the same class. The first theorem shows that any finite sum over all objects can be reorganized as a sum over classes, and that if a weight function assigns the same value to every object in a class, the sum collapses to a per-class mass multiplied by that common weight. This is a generic fact about finite sets and equivalence relations; it needs no group action. A second theorem applies it to the framework's path sum, expressing the total as a sum over classes of a class mass times the weight of a representative object. A third theorem identifies that class mass as the number of labeled objects in the class times a symmetry factor, and a fourth exhibits, at size two, two distinct labeled complexes that are equivalent by a vertex swap, so the class has more than one member and the class mass genuinely exceeds the symmetry factor alone.
The status board also records what is not claimed. Three flags stay false. The framework does not claim a continuum limit for this path sum, does not derive the symmetry-factor convention from invariance and normalization, and does not bridge the first gap in the seven-gaps program. A fourth false flag notes that a quotient-first path sum, defined directly on classes with per-class weights, remains a model for future work, not a constructed object. The declaration's value is that it separates, with kernel-checked precision, the theorems from the targets.
THEOREM classPushforwardStatus_flags · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
theorem classPushforwardStatus_flags :
classPushforwardStatus.generic_fiber_decomposition_proved = true ∧
classPushforwardStatus.classMass_defined = true ∧
classPushforwardStatus.Z_eq_classPushforward_proved = true ∧
classPushforwardStatus.classMass_is_fiberCard_mul_mu = true ∧
classPushforwardStatus.nonSingleton_fiber_exhibited = true ∧
classPushforwardStatus.Z_is_invAut_class_sum = false ∧
classPushforwardStatus.quotient_first_object_constructed = false ∧
classPushforwardStatus.Z_RS_continuum_limit = false ∧
classPushforwardStatus.substrate_measure_derived = false ∧
classPushforwardStatus.gap1_bridge_derived = false :=
⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
THEOREM sum_fiberwise_quotient · sum_eq_quotient_sum_classMass · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
/-- **THEOREM (T1, fiber decomposition).** A finite sum over a `Fintype`
decomposes over the fibers of any quotient map:
`Σ_{a : α} g a = Σ_{q : Quotient s} Σ_{a ∈ fiber q} g a`.
Generic (`AddCommMonoid` values); proved via `Finset.sum_fiberwise`. -/
theorem sum_fiberwise_quotient {α : Type*} [Fintype α] (s : Setoid α)
{M : Type*} [AddCommMonoid M] (g : α → M) :
∑ a : α, g a = ∑ q : Quotient s, ∑ a ∈ classFiber s q, g a := by
classical
rw [← Finset.sum_fiberwise Finset.univ (Quotient.mk s) g]
refine Finset.sum_congr rfl fun q _ => Finset.sum_congr ?_ fun a _ => rfl
ext a
simp only [Finset.mem_filter, Finset.mem_univ, true_and, mem_classFiber]
/-- **THEOREM (T1, class-constant collapse).** If `f` is constant on
classes (mk-equality hypothesis), the fiber sum collapses:
`Σ_{a : α} f a = Σ_{q} fiberCard(q) • f (rep q)` where `rep q = q.out`. -/
theorem sum_eq_quotient_sum_classMass {α : Type*} [Fintype α] (s : Setoid α)
{M : Type*} [AddCommMonoid M] (f : α → M)
(hf : ∀ a b, Quotient.mk s a = Quotient.mk s b → f a = f b) :
∑ a : α, f a = ∑ q : Quotient s, fiberCard s q • f (Quotient.out q) := by
rw [sum_fiberwise_quotient s f]
refine Finset.sum_congr rfl fun q _ => ?_
have hconst : ∀ a ∈ classFiber s q, f a = f (Quotient.out q) := by
intro a ha
exact hf a (Quotient.out q)
(((mem_classFiber s q a).mp ha).trans (Quotient.out_eq q).symm)
rw [Finset.sum_congr rfl hconst, Finset.sum_const]
rfl
THEOREM Z_eq_classPushforward · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
/-- **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]
THEOREM classMass_eq_fiberCard_mul_mu · exists_nonSingleton_fiber · mu_lt_classMass_edgeClass · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
/-- **T3 (the fork detector, identity form).** The pushforward class mass
is the labeled fiber cardinality times the symmetry factor of the class
representative: `classMass q = |fiber(q)| · μ(rep q)`. Kernel-checked on
the actual carrier; uses `mu_congr` (μ is a class function). -/
theorem classMass_eq_fiberCard_mul_mu {B : ℕ} (q : TriangulationClass B) :
classMass q = (fiberCard (relabelSetoid B) q : ℝ) * mu (Quotient.out q) := by
unfold classMass
have hconst : ∀ K ∈ classFiber (relabelSetoid B) q, mu K = mu (Quotient.out q) := by
intro K hK
exact mu_congr (equivalent_of_mk_eq
(((mem_classFiber (relabelSetoid B) q K).mp hK).trans (Quotient.out_eq q).symm))
rw [Finset.sum_congr rfl hconst, Finset.sum_const, nsmul_eq_mul]
rfl
/-- **T3 FORK VERDICT (non-singleton fiber; C1 landmine detonated).**
There exist two distinct labeled complexes that are equivalent: the
quotient fibers of `TriangulationClass` are NOT all singletons, so the
labeled pushforward mass `classMass = |fiber| · (1/|Aut|)` genuinely
differs from the per-class `1/|Aut|` weight. Explicit witness at
`B = 2`. -/
theorem exists_nonSingleton_fiber :
∃ K K' : BoundedComplex 2, K ≠ K' ∧ Equivalent K K' :=
⟨edgeAB, edgeBA, edgeAB_ne_edgeBA, ⟨edgeSwapRelabel⟩⟩
/-- **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)
THEOREM classPushforwardStatus_flags · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
theorem classPushforwardStatus_flags :
classPushforwardStatus.generic_fiber_decomposition_proved = true ∧
classPushforwardStatus.classMass_defined = true ∧
classPushforwardStatus.Z_eq_classPushforward_proved = true ∧
classPushforwardStatus.classMass_is_fiberCard_mul_mu = true ∧
classPushforwardStatus.nonSingleton_fiber_exhibited = true ∧
classPushforwardStatus.Z_is_invAut_class_sum = false ∧
classPushforwardStatus.quotient_first_object_constructed = false ∧
classPushforwardStatus.Z_RS_continuum_limit = false ∧
classPushforwardStatus.substrate_measure_derived = false ∧
classPushforwardStatus.gap1_bridge_derived = false :=
⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
What this page does not claim
The declaration does not prove that the labeled path sum equals a sum with per-class 1/|Aut| weights; that equality is explicitly false at B = 2. The declaration does not construct the quotient-first object or relate it to the labeled sum via orbit counting. The declaration does not claim any continuum limit or convergence preparation for the path 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:
- What is the exact-shell Z_RS_uv wave and how does its quotient-sum convention differ from the labeled path sum?
- What would a quotient-first path sum, defined directly on classes, look like and how would it relate to the labeled sum via orbit counting?
- What is the first gap in the seven-gaps program that the status board flags as unbridged?
- What is the substrate measure whose derivation from invariance and normalization is flagged as open?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM classPushforwardStatus_flags · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
theorem classPushforwardStatus_flags : classPushforwardStatus.generic_fiber_decomposition_proved = true ∧ classPushforwardStatus.classMass_defined = true ∧ classPushforwardStatus.Z_eq_classPushforward_proved = true ∧ classPushforwardStatus.classMass_is_fiberCard_mul_mu = true ∧ classPushforwardStatus.nonSingleton_fiber_exhibited = true ∧ classPushforwardStatus.Z_is_invAut_class_sum = false ∧ classPushforwardStatus.quotient_first_object_constructed = false ∧ classPushforwardStatus.Z_RS_continuum_limit = false ∧ classPushforwardStatus.substrate_measure_derived = false ∧ classPushforwardStatus.gap1_bridge_derived = false := ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩The declaration classPushforwardStatus_flags is a machine-checked status board that records exactly which pieces of a certain path-sum decomposition have been proved and which have not. classPushforwardStatus_flags · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.leanTHEOREM sum_fiberwise_quotient · sum_eq_quotient_sum_classMass · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
/-- **THEOREM (T1, fiber decomposition).** A finite sum over a `Fintype` decomposes over the fibers of any quotient map: `Σ_{a : α} g a = Σ_{q : Quotient s} Σ_{a ∈ fiber q} g a`. Generic (`AddCommMonoid` values); proved via `Finset.sum_fiberwise`. -/ theorem sum_fiberwise_quotient {α : Type*} [Fintype α] (s : Setoid α) {M : Type*} [AddCommMonoid M] (g : α → M) : ∑ a : α, g a = ∑ q : Quotient s, ∑ a ∈ classFiber s q, g a := by classical rw [← Finset.sum_fiberwise Finset.univ (Quotient.mk s) g] refine Finset.sum_congr rfl fun q _ => Finset.sum_congr ?_ fun a _ => rfl ext a simp only [Finset.mem_filter, Finset.mem_univ, true_and, mem_classFiber]/-- **THEOREM (T1, class-constant collapse).** If `f` is constant on classes (mk-equality hypothesis), the fiber sum collapses: `Σ_{a : α} f a = Σ_{q} fiberCard(q) • f (rep q)` where `rep q = q.out`. -/ theorem sum_eq_quotient_sum_classMass {α : Type*} [Fintype α] (s : Setoid α) {M : Type*} [AddCommMonoid M] (f : α → M) (hf : ∀ a b, Quotient.mk s a = Quotient.mk s b → f a = f b) : ∑ a : α, f a = ∑ q : Quotient s, fiberCard s q • f (Quotient.out q) := by rw [sum_fiberwise_quotient s f] refine Finset.sum_congr rfl fun q _ => ?_ have hconst : ∀ a ∈ classFiber s q, f a = f (Quotient.out q) := by intro a ha exact hf a (Quotient.out q) (((mem_classFiber s q a).mp ha).trans (Quotient.out_eq q).symm) rw [Finset.sum_congr rfl hconst, Finset.sum_const] rflThe first theorem shows that any finite sum over all objects can be reorganized as a sum over classes, and that if a weight function assigns the same value to every object in a class, the sum collapses to a per-class mass multiplied by that common weight. sum_fiberwise_quotient · sum_eq_quotient_sum_classMass · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.leanTHEOREM Z_eq_classPushforward · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
/-- **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]A second theorem applies it to the framework's path sum, expressing the total as a sum over classes of a class mass times the weight of a representative object. Z_eq_classPushforward · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.leanTHEOREM classMass_eq_fiberCard_mul_mu · exists_nonSingleton_fiber · mu_lt_classMass_edgeClass · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
/-- **T3 (the fork detector, identity form).** The pushforward class mass is the labeled fiber cardinality times the symmetry factor of the class representative: `classMass q = |fiber(q)| · μ(rep q)`. Kernel-checked on the actual carrier; uses `mu_congr` (μ is a class function). -/ theorem classMass_eq_fiberCard_mul_mu {B : ℕ} (q : TriangulationClass B) : classMass q = (fiberCard (relabelSetoid B) q : ℝ) * mu (Quotient.out q) := by unfold classMass have hconst : ∀ K ∈ classFiber (relabelSetoid B) q, mu K = mu (Quotient.out q) := by intro K hK exact mu_congr (equivalent_of_mk_eq (((mem_classFiber (relabelSetoid B) q K).mp hK).trans (Quotient.out_eq q).symm)) rw [Finset.sum_congr rfl hconst, Finset.sum_const, nsmul_eq_mul] rfl/-- **T3 FORK VERDICT (non-singleton fiber; C1 landmine detonated).** There exist two distinct labeled complexes that are equivalent: the quotient fibers of `TriangulationClass` are NOT all singletons, so the labeled pushforward mass `classMass = |fiber| · (1/|Aut|)` genuinely differs from the per-class `1/|Aut|` weight. Explicit witness at `B = 2`. -/ theorem exists_nonSingleton_fiber : ∃ K K' : BoundedComplex 2, K ≠ K' ∧ Equivalent K K' := ⟨edgeAB, edgeBA, edgeAB_ne_edgeBA, ⟨edgeSwapRelabel⟩⟩/-- **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)A third theorem identifies that class mass as the number of labeled objects in the class times a symmetry factor, and a fourth exhibits, at size two, two distinct labeled complexes that are equivalent by a vertex swap, so the class has more than one member and the class mass genuinely exceeds the symmetry factor alone. classMass_eq_fiberCard_mul_mu · exists_nonSingleton_fiber · mu_lt_classMass_edgeClass · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.leanTHEOREM classPushforwardStatus_flags · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean
theorem classPushforwardStatus_flags : classPushforwardStatus.generic_fiber_decomposition_proved = true ∧ classPushforwardStatus.classMass_defined = true ∧ classPushforwardStatus.Z_eq_classPushforward_proved = true ∧ classPushforwardStatus.classMass_is_fiberCard_mul_mu = true ∧ classPushforwardStatus.nonSingleton_fiber_exhibited = true ∧ classPushforwardStatus.Z_is_invAut_class_sum = false ∧ classPushforwardStatus.quotient_first_object_constructed = false ∧ classPushforwardStatus.Z_RS_continuum_limit = false ∧ classPushforwardStatus.substrate_measure_derived = false ∧ classPushforwardStatus.gap1_bridge_derived = false := ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩The framework does not claim a continuum limit for this path sum, does not derive the symmetry-factor convention from invariance and normalization, and does not bridge the first gap in the seven-gaps program. classPushforwardStatus_flags · IndisputableMonolith/Gravity/SevenGaps/ClassPushforward.lean