Encyclopedia Gravity Gravity Seven Gaps Campaign Ledger

ARTICLE 6 claims 6 theorems

Gravity Seven Gaps Campaign Ledger

A machine-checked status board for seven open problems in quantum gravity, recording what has been proved and what remains unfinished.

Verify this page

The campaign ledger

A campaign ledger is a machine-checked status board. The one for the seven-gaps campaign records, gap by gap, what the 2026-07-14/15 campaign proved and what still remains open. It does not flip any closure flags: none of the increments it records is a full-strength physical closure. The theorem ledger, a discrete record of events, states plainly that full physical closure is not claimed.

The ledger covers seven gaps. For each, it lists a proved increment and an open residual. Gap 1 concerns the map from substrate to triangulation: two obstruction theorems rule out the assumed raw-deficit form, and a corrected bridge is built and certified. Gap 2 proves count-finiteness of a bounded combinatorial class for path-sum measures, but the continuum limit remains open. Gap 3 proves the conformal image has rank at most nV on any Triangulation3D, with a proper subspace on the N = 5 Freudenthal torus; full TT polarization decomposition is open. Gap 4 proves eigenvalue convergence for axis modes only, explicitly not isotropic flat-space recovery; direction-resolved symbols, curved backgrounds, and quasinormal-mode spectra remain open. Gap 5 proves exact translation invariance and a discrete hypersurface-deformation relation closing on a Wronskian-smeared momentum density; the continuum Dirac algebra closed later on 2026-07-23. Gap 6 proves the Wick involution acts as alpha -> -alpha with exact non-degeneracy thresholds, and 4D action-level continuation closed on 2026-07-23. Gap 7's seam functional misses the closing load with certified separation; the true mechanism remains open.

The status theorem is the ledger's spine. It records, as a single machine-checked conjunction, which gaps retain an explicit OPEN component and which closed on later dates. Gap 2's continuum limit, gap 3's full TT decomposition, and gap 7's true mechanism are open. Gaps 1, 4, 5, and 6 have closed components. The anchor theorem re-derives one load-bearing campaign-era result per gap directly from the imported modules, so the ledger cannot silently drift from the artifacts. For gap 5, the anchor is the abelian momentum-sector instance from the campaign, not the later 2026-07-23 close, which lives in a separate module to avoid an import cycle.

The ledger's purpose is to keep honest the difference between a scoped increment and a full physical closure. Every proved flag is a theorem, forced by rfl against the imported modules, with no sorry and no new axioms. The campaign-level claim is scoped increments, never full physical closure. This is what the framework's library, a machine-checked collection of formal theorems, can certify: not that the seven gaps are closed, but exactly which parts of them are, and which are not.

THEOREM no_full_physical_closure_claimed · IndisputableMonolith/Gravity/SevenGaps/CampaignLedger.lean
no_full_physical_closure_claimed · IndisputableMonolith/Gravity/SevenGaps/CampaignLedger.lean:150 
/-- The campaign did not achieve (and does not claim) full physical closure:
gaps 2/3/7 retain an explicit OPEN component. Gap 1's hessian-symbol
comparison closed 2026-07-22 under amended intent
(`gap1_hessian_join_closing_package`); gap6 action continuation closed
2026-07-23 via `wick_action_continuation_4d_v2`; gap4 curved/QNM closed
2026-07-23 via `discrete_tt_spectrum_converges_curved` ∧
`quasinormal_mode_spectrum`; gap5 continuum algebra + HKT closed 2026-07-23
via `dirac_algebra_continuum_limit` ∧ `hojman_pins_general_relativity`.
This theorem tracks the remaining opens plus the closed bits. -/
theorem no_full_physical_closure_claimed :
    sevenGapsCampaignStatus.gap1_hessian_symbol_comparison_open = false
      ∧ sevenGapsCampaignStatus.gap2_continuum_limit_open = true
      ∧ sevenGapsCampaignStatus.gap3_full_tt_decomposition_open = true
      ∧ sevenGapsCampaignStatus.gap4_curved_qnm_open = false
      ∧ sevenGapsCampaignStatus.gap5_continuum_algebra_hkt_open = false
      ∧ sevenGapsCampaignStatus.gap6_action_continuation_open = false
      ∧ sevenGapsCampaignStatus.gap6_kinematical_wick_certified = true
      ∧ sevenGapsCampaignStatus.gap7_true_mechanism_open = true :=
  ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
THEOREM campaign_flags_anchored · IndisputableMonolith/Gravity/SevenGaps/CampaignLedger.lean
campaign_flags_anchored · IndisputableMonolith/Gravity/SevenGaps/CampaignLedger.lean:170 
/-- **Anchor theorem (campaign-era).**  The proved flags are not
free-floating booleans: this theorem re-derives one load-bearing
campaign-era result per gap directly from the imported modules, so the
ledger cannot silently drift from the artifacts.  These anchors date from
the 2026-07-14/15 lattice campaign; in particular the gap-5 conjunct is the
abelian momentum-sector instance from that campaign, NOT the 2026-07-23
close.  The closed gap-5 terminal binding lives in
`Gap5ConstraintCloseStatus.gap5_constraint_recovery_bound_to_terminals`
(kept out of this module to avoid an import cycle).
(Gap 7 is quarantined and anchored in `SeamGrammarVerdict` itself.) -/
theorem campaign_flags_anchored :
    -- gap 1 (sign no-go: every bridge forces nonnegative deficits)
    (∀ {Λ : Type} [inst : Fintype Λ] [inst2 : DecidableEq Λ]
      (L : RecognitionLedger.RecognitionLedger Λ) (H : Type)
      (b : LedgerToHingeBridge H L) (i : Λ),
        0 ≤ b.geometricDeficit (b.x_sigma i))
    -- gap 2 (count-finiteness of the scoped class)
    ∧ (∀ B : ℕ, 0 < Fintype.card (PathSumMeasure.BoundedComplex B))
    -- gap 4 (flat TT eigenvalue convergence for every fixed AXIS mode;
    -- axis sector only, see the gap-4 scope note in the module header)
    ∧ (∀ k : ℕ, Filter.Tendsto
        (fun N : ℕ => 4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * k / N) ^ 2)
        Filter.atTop (nhds ((2 * Real.pi * k) ^ 2)))
    -- gap 5 (abelian momentum sector, n = 8 instance; campaign-era anchor,
    -- the 2026-07-23 terminal close is bound in Gap5ConstraintCloseStatus)
    ∧ (∀ (a b : ZMod 8) (x : HypersurfaceDeformation.PhaseSpace 8),
        HypersurfaceDeformation.bracket (HypersurfaceDeformation.Dgen a)
          (HypersurfaceDeformation.Dgen b) x = 0)
    -- gap 6 (exact non-degeneracy iff on the causal class)
    ∧ (∀ (ty : CausalSimplexWick.CausalTetType) (a alpha : ℝ), 0 < a →
        (0 < Geometry.CayleyMengerPolynomial.cm3
            (CausalSimplexWick.euclideanSqEdges ty a alpha)
          ↔ CausalSimplexWick.alphaMin ty < alpha)) := by
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · intro Λ _ _ L H b i
    exact bridge_forces_nonneg_geometricDeficit L b i
  · exact PathSumMeasure.boundedComplex_card_pos
  · intro k
    simpa [DiscreteLichnerowicz.discreteEigenvalue] using
      DiscreteLichnerowicz.discreteEigenvalue_tendsto k
  · intro a b x
    exact HypersurfaceDeformation.bracket_Dgen_Dgen a b x
  · intro ty a alpha ha
    exact CausalSimplexWick.cm3_euclidean_pos_iff ty a alpha ha
THEOREM campaign_flags_anchored · IndisputableMonolith/Gravity/SevenGaps/CampaignLedger.lean
campaign_flags_anchored · IndisputableMonolith/Gravity/SevenGaps/CampaignLedger.lean:170 
/-- **Anchor theorem (campaign-era).**  The proved flags are not
free-floating booleans: this theorem re-derives one load-bearing
campaign-era result per gap directly from the imported modules, so the
ledger cannot silently drift from the artifacts.  These anchors date from
the 2026-07-14/15 lattice campaign; in particular the gap-5 conjunct is the
abelian momentum-sector instance from that campaign, NOT the 2026-07-23
close.  The closed gap-5 terminal binding lives in
`Gap5ConstraintCloseStatus.gap5_constraint_recovery_bound_to_terminals`
(kept out of this module to avoid an import cycle).
(Gap 7 is quarantined and anchored in `SeamGrammarVerdict` itself.) -/
theorem campaign_flags_anchored :
    -- gap 1 (sign no-go: every bridge forces nonnegative deficits)
    (∀ {Λ : Type} [inst : Fintype Λ] [inst2 : DecidableEq Λ]
      (L : RecognitionLedger.RecognitionLedger Λ) (H : Type)
      (b : LedgerToHingeBridge H L) (i : Λ),
        0 ≤ b.geometricDeficit (b.x_sigma i))
    -- gap 2 (count-finiteness of the scoped class)
    ∧ (∀ B : ℕ, 0 < Fintype.card (PathSumMeasure.BoundedComplex B))
    -- gap 4 (flat TT eigenvalue convergence for every fixed AXIS mode;
    -- axis sector only, see the gap-4 scope note in the module header)
    ∧ (∀ k : ℕ, Filter.Tendsto
        (fun N : ℕ => 4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * k / N) ^ 2)
        Filter.atTop (nhds ((2 * Real.pi * k) ^ 2)))
    -- gap 5 (abelian momentum sector, n = 8 instance; campaign-era anchor,
    -- the 2026-07-23 terminal close is bound in Gap5ConstraintCloseStatus)
    ∧ (∀ (a b : ZMod 8) (x : HypersurfaceDeformation.PhaseSpace 8),
        HypersurfaceDeformation.bracket (HypersurfaceDeformation.Dgen a)
          (HypersurfaceDeformation.Dgen b) x = 0)
    -- gap 6 (exact non-degeneracy iff on the causal class)
    ∧ (∀ (ty : CausalSimplexWick.CausalTetType) (a alpha : ℝ), 0 < a →
        (0 < Geometry.CayleyMengerPolynomial.cm3
            (CausalSimplexWick.euclideanSqEdges ty a alpha)
          ↔ CausalSimplexWick.alphaMin ty < alpha)) := by
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · intro Λ _ _ L H b i
    exact bridge_forces_nonneg_geometricDeficit L b i
  · exact PathSumMeasure.boundedComplex_card_pos
  · intro k
    simpa [DiscreteLichnerowicz.discreteEigenvalue] using
      DiscreteLichnerowicz.discreteEigenvalue_tendsto k
  · intro a b x
    exact HypersurfaceDeformation.bracket_Dgen_Dgen a b x
  · intro ty a alpha ha
    exact CausalSimplexWick.cm3_euclidean_pos_iff ty a alpha ha
THEOREM campaign_flags_anchored · IndisputableMonolith/Gravity/SevenGaps/CampaignLedger.lean
campaign_flags_anchored · IndisputableMonolith/Gravity/SevenGaps/CampaignLedger.lean:170 
/-- **Anchor theorem (campaign-era).**  The proved flags are not
free-floating booleans: this theorem re-derives one load-bearing
campaign-era result per gap directly from the imported modules, so the
ledger cannot silently drift from the artifacts.  These anchors date from
the 2026-07-14/15 lattice campaign; in particular the gap-5 conjunct is the
abelian momentum-sector instance from that campaign, NOT the 2026-07-23
close.  The closed gap-5 terminal binding lives in
`Gap5ConstraintCloseStatus.gap5_constraint_recovery_bound_to_terminals`
(kept out of this module to avoid an import cycle).
(Gap 7 is quarantined and anchored in `SeamGrammarVerdict` itself.) -/
theorem campaign_flags_anchored :
    -- gap 1 (sign no-go: every bridge forces nonnegative deficits)
    (∀ {Λ : Type} [inst : Fintype Λ] [inst2 : DecidableEq Λ]
      (L : RecognitionLedger.RecognitionLedger Λ) (H : Type)
      (b : LedgerToHingeBridge H L) (i : Λ),
        0 ≤ b.geometricDeficit (b.x_sigma i))
    -- gap 2 (count-finiteness of the scoped class)
    ∧ (∀ B : ℕ, 0 < Fintype.card (PathSumMeasure.BoundedComplex B))
    -- gap 4 (flat TT eigenvalue convergence for every fixed AXIS mode;
    -- axis sector only, see the gap-4 scope note in the module header)
    ∧ (∀ k : ℕ, Filter.Tendsto
        (fun N : ℕ => 4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * k / N) ^ 2)
        Filter.atTop (nhds ((2 * Real.pi * k) ^ 2)))
    -- gap 5 (abelian momentum sector, n = 8 instance; campaign-era anchor,
    -- the 2026-07-23 terminal close is bound in Gap5ConstraintCloseStatus)
    ∧ (∀ (a b : ZMod 8) (x : HypersurfaceDeformation.PhaseSpace 8),
        HypersurfaceDeformation.bracket (HypersurfaceDeformation.Dgen a)
          (HypersurfaceDeformation.Dgen b) x = 0)
    -- gap 6 (exact non-degeneracy iff on the causal class)
    ∧ (∀ (ty : CausalSimplexWick.CausalTetType) (a alpha : ℝ), 0 < a →
        (0 < Geometry.CayleyMengerPolynomial.cm3
            (CausalSimplexWick.euclideanSqEdges ty a alpha)
          ↔ CausalSimplexWick.alphaMin ty < alpha)) := by
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · intro Λ _ _ L H b i
    exact bridge_forces_nonneg_geometricDeficit L b i
  · exact PathSumMeasure.boundedComplex_card_pos
  · intro k
    simpa [DiscreteLichnerowicz.discreteEigenvalue] using
      DiscreteLichnerowicz.discreteEigenvalue_tendsto k
  · intro a b x
    exact HypersurfaceDeformation.bracket_Dgen_Dgen a b x
  · intro ty a alpha ha
    exact CausalSimplexWick.cm3_euclidean_pos_iff ty a alpha ha
THEOREM campaign_flags_anchored · IndisputableMonolith/Gravity/SevenGaps/CampaignLedger.lean
campaign_flags_anchored · IndisputableMonolith/Gravity/SevenGaps/CampaignLedger.lean:170 
/-- **Anchor theorem (campaign-era).**  The proved flags are not
free-floating booleans: this theorem re-derives one load-bearing
campaign-era result per gap directly from the imported modules, so the
ledger cannot silently drift from the artifacts.  These anchors date from
the 2026-07-14/15 lattice campaign; in particular the gap-5 conjunct is the
abelian momentum-sector instance from that campaign, NOT the 2026-07-23
close.  The closed gap-5 terminal binding lives in
`Gap5ConstraintCloseStatus.gap5_constraint_recovery_bound_to_terminals`
(kept out of this module to avoid an import cycle).
(Gap 7 is quarantined and anchored in `SeamGrammarVerdict` itself.) -/
theorem campaign_flags_anchored :
    -- gap 1 (sign no-go: every bridge forces nonnegative deficits)
    (∀ {Λ : Type} [inst : Fintype Λ] [inst2 : DecidableEq Λ]
      (L : RecognitionLedger.RecognitionLedger Λ) (H : Type)
      (b : LedgerToHingeBridge H L) (i : Λ),
        0 ≤ b.geometricDeficit (b.x_sigma i))
    -- gap 2 (count-finiteness of the scoped class)
    ∧ (∀ B : ℕ, 0 < Fintype.card (PathSumMeasure.BoundedComplex B))
    -- gap 4 (flat TT eigenvalue convergence for every fixed AXIS mode;
    -- axis sector only, see the gap-4 scope note in the module header)
    ∧ (∀ k : ℕ, Filter.Tendsto
        (fun N : ℕ => 4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * k / N) ^ 2)
        Filter.atTop (nhds ((2 * Real.pi * k) ^ 2)))
    -- gap 5 (abelian momentum sector, n = 8 instance; campaign-era anchor,
    -- the 2026-07-23 terminal close is bound in Gap5ConstraintCloseStatus)
    ∧ (∀ (a b : ZMod 8) (x : HypersurfaceDeformation.PhaseSpace 8),
        HypersurfaceDeformation.bracket (HypersurfaceDeformation.Dgen a)
          (HypersurfaceDeformation.Dgen b) x = 0)
    -- gap 6 (exact non-degeneracy iff on the causal class)
    ∧ (∀ (ty : CausalSimplexWick.CausalTetType) (a alpha : ℝ), 0 < a →
        (0 < Geometry.CayleyMengerPolynomial.cm3
            (CausalSimplexWick.euclideanSqEdges ty a alpha)
          ↔ CausalSimplexWick.alphaMin ty < alpha)) := by
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · intro Λ _ _ L H b i
    exact bridge_forces_nonneg_geometricDeficit L b i
  · exact PathSumMeasure.boundedComplex_card_pos
  · intro k
    simpa [DiscreteLichnerowicz.discreteEigenvalue] using
      DiscreteLichnerowicz.discreteEigenvalue_tendsto k
  · intro a b x
    exact HypersurfaceDeformation.bracket_Dgen_Dgen a b x
  · intro ty a alpha ha
    exact CausalSimplexWick.cm3_euclidean_pos_iff ty a alpha ha
THEOREM campaign_flags_anchored · IndisputableMonolith/Gravity/SevenGaps/CampaignLedger.lean
campaign_flags_anchored · IndisputableMonolith/Gravity/SevenGaps/CampaignLedger.lean:170 
/-- **Anchor theorem (campaign-era).**  The proved flags are not
free-floating booleans: this theorem re-derives one load-bearing
campaign-era result per gap directly from the imported modules, so the
ledger cannot silently drift from the artifacts.  These anchors date from
the 2026-07-14/15 lattice campaign; in particular the gap-5 conjunct is the
abelian momentum-sector instance from that campaign, NOT the 2026-07-23
close.  The closed gap-5 terminal binding lives in
`Gap5ConstraintCloseStatus.gap5_constraint_recovery_bound_to_terminals`
(kept out of this module to avoid an import cycle).
(Gap 7 is quarantined and anchored in `SeamGrammarVerdict` itself.) -/
theorem campaign_flags_anchored :
    -- gap 1 (sign no-go: every bridge forces nonnegative deficits)
    (∀ {Λ : Type} [inst : Fintype Λ] [inst2 : DecidableEq Λ]
      (L : RecognitionLedger.RecognitionLedger Λ) (H : Type)
      (b : LedgerToHingeBridge H L) (i : Λ),
        0 ≤ b.geometricDeficit (b.x_sigma i))
    -- gap 2 (count-finiteness of the scoped class)
    ∧ (∀ B : ℕ, 0 < Fintype.card (PathSumMeasure.BoundedComplex B))
    -- gap 4 (flat TT eigenvalue convergence for every fixed AXIS mode;
    -- axis sector only, see the gap-4 scope note in the module header)
    ∧ (∀ k : ℕ, Filter.Tendsto
        (fun N : ℕ => 4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * k / N) ^ 2)
        Filter.atTop (nhds ((2 * Real.pi * k) ^ 2)))
    -- gap 5 (abelian momentum sector, n = 8 instance; campaign-era anchor,
    -- the 2026-07-23 terminal close is bound in Gap5ConstraintCloseStatus)
    ∧ (∀ (a b : ZMod 8) (x : HypersurfaceDeformation.PhaseSpace 8),
        HypersurfaceDeformation.bracket (HypersurfaceDeformation.Dgen a)
          (HypersurfaceDeformation.Dgen b) x = 0)
    -- gap 6 (exact non-degeneracy iff on the causal class)
    ∧ (∀ (ty : CausalSimplexWick.CausalTetType) (a alpha : ℝ), 0 < a →
        (0 < Geometry.CayleyMengerPolynomial.cm3
            (CausalSimplexWick.euclideanSqEdges ty a alpha)
          ↔ CausalSimplexWick.alphaMin ty < alpha)) := by
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · intro Λ _ _ L H b i
    exact bridge_forces_nonneg_geometricDeficit L b i
  · exact PathSumMeasure.boundedComplex_card_pos
  · intro k
    simpa [DiscreteLichnerowicz.discreteEigenvalue] using
      DiscreteLichnerowicz.discreteEigenvalue_tendsto k
  · intro a b x
    exact HypersurfaceDeformation.bracket_Dgen_Dgen a b x
  · intro ty a alpha ha
    exact CausalSimplexWick.cm3_euclidean_pos_iff ty a alpha ha

What this page does not claim

The ledger does not claim any full-strength physical closure for the seven gaps. The gap 4 axis-sector convergence is not isotropic flat-space recovery. The gap 5 anchor is the campaign-era abelian instance, not the later 2026-07-23 continuum Dirac algebra close.

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/CampaignLedger.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