Encyclopedia Gravity Gravity Seven Gaps Full Theory Ledger Gap5 Structure Function Blocker Certified

ARTICLE 3 claims 3 theorems

Gravity Seven Gaps Full Theory Ledger Gap5 Structure Function Blocker Certified

A machine-checked theorem pins down what a discrete gravity theory cannot do, and in doing so it reopens a pillar of the full theory campaign.

Verify this page

The structure function blocker

The declaration gap5_structure_function_blocker_certified is a theorem in the framework's machine-checked library of formal theorems. It establishes a precise limitation on the recovery of general relativity from a discrete substrate. In plain language, it proves that no fixed background structure function can represent the dynamic inverse metric that the discrete theory actually produces. This is not a failure of the theory; it is a certified boundary on what a particular class of approximations can achieve.

The theorem has three parts. First, every weight function on the two-element group ZMod 2 admits a Hamiltonian with a background structure function. Second, every continuous function on the unit interval is reachable as a background-weighted continuum limit. Third, and most importantly, for every such weight function, the fixed background cannot represent the concrete dynamic inverse metric. The third part is the blocker: it rules out a whole family of attempts to recover the continuum constraint algebra by postulating a static background.

In the context of the full-theory campaign, this theorem is one of several certified blockers. The campaign tracks progress toward a quantum gravity theory through a ledger of boolean flags, one per pillar benchmark. A flag flips to true only when its target theorem is kernel-checked, axiom-audited, and critic-passed. The master theorem full_theory_open_pillar3_alone remains provable until every pillar flips. The gap5 blocker is part of pillar 1, which concerns classical recovery. The three recovery strengths still hold, but the criterion now asks a question it previously did not: where did the discretization come from? This blocker answers that question in the negative for one specific route.

What the theorem does not claim is equally important. It does not prove that classical recovery is impossible. It does not show that the discrete theory is wrong. It does not establish that no continuum limit exists at all. It only certifies that a fixed background structure function cannot serve as the bridge. The path to classical recovery must go through a dynamic structure, not a static one. This is a constructive constraint, not a dead end.

THEOREM gap5_structure_function_blocker_certified · IndisputableMonolith/Gravity/SevenGaps/FullTheoryLedger.lean
gap5_structure_function_blocker_certified · IndisputableMonolith/Gravity/SevenGaps/FullTheoryLedger.lean:925 
/-- **GAP 5 STRUCTURE-FUNCTION BLOCKER (THEOREM).** Every fixed background
weight yields a background (phase-space constant) structure function and
reaches the weighted continuum, but no fixed background represents the
explicit positive dynamic inverse metric.  The weighted-bracket route
therefore required a genuinely dynamic structure function; that route was
closed 2026-07-23 via the Dirac continuum + kinetic-normalized HKT pin
(`gap5_constraint_recovery = true`). This blocker remains the certificate
that fixed-background shortcuts stay dead. -/
theorem gap5_structure_function_blocker_certified :
    (∀ w : ZMod 2 → ℝ,
      DynamicStructureFunctionBlocker.HamWHasBackgroundStructureFunction w) ∧
    (∀ W : ℝ → ℝ, ContinuousOn W (Set.Icc 0 1) →
      DynamicStructureFunctionBlocker.BackgroundWeightedContinuumReach W) ∧
    (∀ w : ZMod 2 → ℝ,
      ¬ DynamicStructureFunctionBlocker.FixedBackgroundRepresents w
        DynamicStructureFunctionBlocker.concreteDynamicInverseMetric) :=
  DynamicStructureFunctionBlocker.gap5_background_weight_blocker
THEOREM gap5_structure_function_blocker_certified · IndisputableMonolith/Gravity/SevenGaps/FullTheoryLedger.lean
gap5_structure_function_blocker_certified · IndisputableMonolith/Gravity/SevenGaps/FullTheoryLedger.lean:925 
/-- **GAP 5 STRUCTURE-FUNCTION BLOCKER (THEOREM).** Every fixed background
weight yields a background (phase-space constant) structure function and
reaches the weighted continuum, but no fixed background represents the
explicit positive dynamic inverse metric.  The weighted-bracket route
therefore required a genuinely dynamic structure function; that route was
closed 2026-07-23 via the Dirac continuum + kinetic-normalized HKT pin
(`gap5_constraint_recovery = true`). This blocker remains the certificate
that fixed-background shortcuts stay dead. -/
theorem gap5_structure_function_blocker_certified :
    (∀ w : ZMod 2 → ℝ,
      DynamicStructureFunctionBlocker.HamWHasBackgroundStructureFunction w) ∧
    (∀ W : ℝ → ℝ, ContinuousOn W (Set.Icc 0 1) →
      DynamicStructureFunctionBlocker.BackgroundWeightedContinuumReach W) ∧
    (∀ w : ZMod 2 → ℝ,
      ¬ DynamicStructureFunctionBlocker.FixedBackgroundRepresents w
        DynamicStructureFunctionBlocker.concreteDynamicInverseMetric) :=
  DynamicStructureFunctionBlocker.gap5_background_weight_blocker
THEOREM full_theory_open_pillar3_alone · IndisputableMonolith/Gravity/SevenGaps/FullTheoryLedger.lean
full_theory_open_pillar3_alone · IndisputableMonolith/Gravity/SevenGaps/FullTheoryLedger.lean:470 
/-- **MASTER THEOREM (the honest gate), replaced 2026-07-31 after the D-A
adoptions.** The full theory is NOT closed, and the obstruction is Pillar 3
alone: `discriminating_prediction_confirmed = false` and
`prediction_is_discriminating = false` (flag 11; its residual is E_lat and
the sky). The strength of every closed conjunct: flag 6
(`gap1_provenance_derived`) and flag 12 (`no_free_constants`) closed
2026-07-31 at MODEL strength under the named D-A adoptions (MODEL 1-L and
the SameLatticeUnitsPremise, on top of the already adopted MODEL 1 and
MODEL 2; never derived, the derivation routes kernel-proved dead), composed
in `Gap5UnitIdentificationsAdopted`; Pillar 2 closed 2026-07-31 with flag 9
at derived action shape plus MODEL super-critical strength
(D-qg-flag9-closes-at-model-strength-20260731) on top of the bridge and
measure flags at theorem strength; the four recovery flags of Pillar 1
stand at theorem strength. This theorem replaces `full_theory_not_yet_closed`,
retired the day pillars 1 and 2 closed because its recorded premise (two
pillars open) stopped being true; it fails to build unchanged the moment
flag 11 flips, so it cannot silently coexist with a closure claim. -/
theorem full_theory_open_pillar3_alone :
    ¬ FullTheoryClosed fullTheoryBenchmarks ∧
      Pillar1Closed fullTheoryBenchmarks ∧
        Pillar2Closed fullTheoryBenchmarks ∧
          ¬ Pillar3Closed fullTheoryBenchmarks := by
  refine ⟨?_, ⟨rfl, rfl, rfl, rfl, rfl⟩, ⟨rfl, rfl, rfl, rfl⟩, fun h => ?_⟩
  · intro h
    have := h.2.2.1.1
    simp [fullTheoryBenchmarks] at this
  · have := h.1
    simp [fullTheoryBenchmarks] at this

What this page does not claim

The theorem does not prove that classical recovery of general relativity is impossible. The theorem does not show that the discrete theory is empirically wrong. The theorem does not establish that no continuum limit exists at all.

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