Gravity Seven Gaps Hinge Stationarity Core Closed Cycle Coboundary Sum Eq Zero

The closed-cycle obstruction

In the Recognition Science framework, the geometry of spacetime is built from a discrete record of recognition events, a ledger that tracks how one cell of space relates to its neighbors. The framework models the stretching between adjacent cells as a strain, and a central question is whether these strains can accumulate around a loop to produce a measurable deficit, a hinge gap. The declaration closedCycle_coboundary_sum_eq_zero answers a narrow but decisive part of that question.

The theorem states that if the strain between two cells can be written as the difference of a single function evaluated at each cell, a property called a coboundary, then the sum of these strains around any closed cycle is exactly zero. The proof is a telescoping sum: each cell's value appears once with a plus sign and once with a minus sign as you walk around the loop, so everything cancels. This is a general mathematical fact, not a claim about any particular physical system.

In Recognition Science, this identity is a kill record. It proves that a nonzero hinge deficit can never be sourced by summing coboundary strains around a closed hinge link. The raw Stokes route, which tried to derive gravity's curvature from such a sum, is therefore closed. The framework does not claim that this identity alone produces gravity; it only removes one specific mechanism from consideration.

What the declaration does not claim is equally important. It does not say that all strains are coboundaries, nor that a hinge deficit is impossible. It says only that if the strains are exact coboundaries, their closed-cycle sum vanishes. The framework's actual mechanism for a sourced stationary ratio uses a different, explicit coupling term, not a coboundary sum. The identity is a constraint on one approach, not a construction of the final theory.

/-- **THEOREM (kill record C6, the raw Stokes route).** For a coboundary
strain s i j = f i - f j and any cyclic chain of cells v 0, v 1, ..., v m
with v m = v 0, the sum of strains around the cycle telescopes to zero.
Exact/coboundary substrate strains can NEVER sum to a nonzero deficit
around a closed hinge link: the raw Stokes route to the bridge relation is
dead, kernel-checked. -/
theorem closedCycle_coboundary_sum_eq_zero {Λ : Type*} {s : Λ → Λ → ℝ}
    (hs : IsCoboundary s) (v : ℕ → Λ) (m : ℕ) (hcycle : v m = v 0) :
    ∑ k ∈ Finset.range m, s (v k) (v (k + 1)) = 0 := by
  obtain ⟨f, hf⟩ := hs
  calc ∑ k ∈ Finset.range m, s (v k) (v (k + 1))
      = ∑ k ∈ Finset.range m,
          ((fun j => f (v j)) k - (fun j => f (v j)) (k + 1)) :=
        Finset.sum_congr rfl fun k _ => hf (v k) (v (k + 1))
    _ = f (v 0) - f (v m) := Finset.sum_range_sub' (fun j => f (v j)) m
    _ = 0 := by rw [hcycle]; ring

/-- **THEOREM (kill record C6, the raw Stokes route).** For a coboundary
strain s i j = f i - f j and any cyclic chain of cells v 0, v 1, ..., v m
with v m = v 0, the sum of strains around the cycle telescopes to zero.
Exact/coboundary substrate strains can NEVER sum to a nonzero deficit
around a closed hinge link: the raw Stokes route to the bridge relation is
dead, kernel-checked. -/
theorem closedCycle_coboundary_sum_eq_zero {Λ : Type*} {s : Λ → Λ → ℝ}
    (hs : IsCoboundary s) (v : ℕ → Λ) (m : ℕ) (hcycle : v m = v 0) :
    ∑ k ∈ Finset.range m, s (v k) (v (k + 1)) = 0 := by
  obtain ⟨f, hf⟩ := hs
  calc ∑ k ∈ Finset.range m, s (v k) (v (k + 1))
      = ∑ k ∈ Finset.range m,
          ((fun j => f (v j)) k - (fun j => f (v j)) (k + 1)) :=
        Finset.sum_congr rfl fun k _ => hf (v k) (v (k + 1))
    _ = f (v 0) - f (v m) := Finset.sum_range_sub' (fun j => f (v j)) m
    _ = 0 := by rw [hcycle]; ring

What this page does not claim

The identity does not prove that all strains are coboundaries. The identity does not prove that a nonzero hinge deficit is impossible. The identity does not by itself construct a model of gravity.

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