Gravity Seven Gaps Dynamic Structure Function Blocker No Fixed Background Repres

The background-weight limit

General relativity describes gravity through the geometry of spacetime, which changes as matter and energy move. In the canonical formulation used for quantization, the metric and its conjugate momentum form a phase space, and the dynamics are governed by a Hamiltonian constraint. The Recognition Science framework's machine-checked library of formal theorems contains a result that clarifies a specific technical obstruction in this setting.

The result concerns a simplified model with a discrete phase space of two sites. The library defines a phase space as a pair of functions assigning real numbers to each site, representing the configuration and momentum. A key object is a dynamic inverse metric, a site-dependent weight that varies with the phase-space point. The theorem no_fixed_background_represents_concrete proves that no fixed background weight can represent this dynamic inverse metric, because the metric is not phase-space constant.

In plain language: if a quantity depends on where you are in phase space, you cannot capture it with a single, unchanging background value. The theorem shows this by exhibiting two phase-space points where the dynamic inverse metric takes different values, while a fixed background would have to assign the same value at both. This is a precise statement of underdetermination: the background-weighted bracket, despite its exact lattice identity and continuum smearing reach, cannot by itself be the full dynamic Dirac structure function.

In Recognition Science, this result is tagged as a blocker within the Seven Gaps program. It does not claim that the dynamic inverse metric is impossible to represent, only that a fixed background cannot do it. The library names the missing construction: PhaseSpaceDependentHamiltonianConstruction would supply a Hamiltonian whose bracket produces the phase-space-dependent weight. The result also does not change any closure flag, meaning the overall goal of a dynamic structure function remains open.

The practical consequence is a clear division of labor. A fixed background weight works for constant metrics, and the library proves this: exists_fixed_background_iff_phaseSpaceConstant shows that a fixed background represents a phase-space-dependent metric if and only if that metric is constant. For the full dynamics of gravity, where the inverse spatial metric varies with the canonical data, a different construction is required. The theorem certifies that distinction, and the path forward is named, not yet built.

/-- 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 (exact characterization). A candidate inverse metric admits one
fixed background representation at all phase points exactly when it is
phase-space constant. -/
theorem exists_fixed_background_iff_phaseSpaceConstant
    (g : PhaseSpace n → ZMod n → ℝ) :
    (∃ w : ZMod n → ℝ, FixedBackgroundRepresents w g) ↔
      PhaseSpaceConstant g := by
  constructor
  · rintro ⟨w, hw⟩
    exact fixed_background_represents_only_constant w g hw
  · intro hg
    let x₀ : PhaseSpace n := (fun _ => 0, fun _ => 0)
    refine ⟨g x₀, ?_⟩
    intro x j
    exact hg x₀ x 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 (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

No fixed background can represent any phase-space-dependent metric, only the specific two-site example. The result proves the dynamic structure function cannot exist; it only shows a fixed background cannot serve as it. The phase-space-dependent Hamiltonian construction has been built; the library names it as a missing obligation.

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: