Gravity Seven Gaps Dynamic Structure Function Blocker

The dynamic structure function gap

In the Recognition Science framework's approach to canonical quantum gravity, the Dirac bracket between two Hamiltonians must contain a structure function: a site-dependent quantity that plays the role of the inverse spatial metric. The framework's existing lattice bracket uses a fixed background weight in that slot, and two theorems certify its reach. The exact lattice identity `bracket_HamW_HamW` places the weight correctly, and `weightedStructureSum_tendsto` shows that its smearing shape converges to the continuum. Both results hold with the weight held fixed as the phase-space point varies.

Full ADM gravity, by contrast, requires the inverse spatial metric in that slot to vary with the canonical metric data. The module certifies that distinction. A fixed background weight can represent a phase-space-dependent inverse metric at every phase point only if that metric is phase-space constant. The theorem `fixed_background_represents_only_constant` proves exactly this: if a fixed weight represents a metric at every point, the metric must be constant. The positive two-site example `concreteDynamicInverseMetric` is not constant, so no background weight can represent it. The theorem `no_fixed_background_represents_concrete` closes that case.

In Recognition Science, this result is a blocker: it names a precise obstruction to using the background-weighted bracket as the full dynamic Dirac structure function. The existing bracket is not wrong, it is incomplete. No closure flag is changed. The definition `PhaseSpaceDependentHamiltonianConstruction` names the missing Hamiltonian construction, and `Gap5DynamicDiracAndHKTRigidityTarget` records that this construction and the existing HKT rigidity statement remain separate obligations. The physical recognition-to-linking bridge for gravity remains open.

The practical consequence is a clear boundary. The framework's lattice bracket has exact reach and continuum smearing, but it cannot by itself be the dynamic structure function of full gravity. The module does not solve the missing construction; it proves that a particular shortcut cannot work. That negative result is what makes the remaining target precise.

/-- THEOREM. If one fixed background weight represents `g` at every
phase-space point, then `g` is phase-space constant. -/
theorem fixed_background_represents_only_constant
    (w : ZMod n → ℝ) (g : PhaseSpace n → ZMod n → ℝ)
    (h : FixedBackgroundRepresents w g) :
    PhaseSpaceConstant g := by
  intro x y j
  rw [← h x j, ← h y j]

/-- THEOREM. The positive two-site metric candidate is genuinely
phase-space-dependent. -/
theorem concreteDynamicInverseMetric_not_constant :
    ¬ PhaseSpaceConstant concreteDynamicInverseMetric := by
  intro h
  have hEq := h zeroPhasePoint unitConfigurationPoint (0 : ZMod 2)
  have hw := concreteDynamicInverseMetric_witness
  rw [hw.1, hw.2] at hEq
  norm_num at hEq

/-- THEOREM (concrete no-go). No fixed two-site background weight represents
the concrete dynamic inverse metric at every phase-space point. -/
theorem no_fixed_background_represents_concrete
    (w : ZMod 2 → ℝ) :
    ¬ FixedBackgroundRepresents w concreteDynamicInverseMetric := by
  intro h
  exact concreteDynamicInverseMetric_not_constant
    (fixed_background_represents_only_constant w concreteDynamicInverseMetric h)

/-- THEOREM (certified blocker). The present background-weighted family has
its exact bracket and continuum reach, but no choice of its fixed two-site
weight can represent the explicit positive dynamic metric at all phase
points. -/
theorem gap5_background_weight_blocker :
    (∀ w : ZMod 2 → ℝ, HamWHasBackgroundStructureFunction w) ∧
      (∀ W : ℝ → ℝ, ContinuousOn W (Set.Icc 0 1) →
        BackgroundWeightedContinuumReach W) ∧
      (∀ w : ZMod 2 → ℝ,
        ¬ FixedBackgroundRepresents w concreteDynamicInverseMetric) := by
  exact ⟨HamW_has_background_structure_function,
    background_weighted_continuum_reach,
    no_fixed_background_represents_concrete⟩

What this page does not claim

The module does not construct the missing phase-space-dependent Hamiltonian. The module does not prove that no such construction exists. The module does not change any closure flag for the seven gaps. The physical recognition-to-linking bridge for gravity remains open, not proved.

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