Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.DynamicStructureFunctionBlocker

show as:
view Lean formalization →

On the periodic lattice, a fixed background weight can represent an inverse metric only when that metric is phase-space constant (insensitive to canonical data at every site). The module builds a concrete dynamic inverse metric that varies with phase space, proves it is not constant, and therefore cannot arise from any fixed background. Gravity and QG constraint-algebra workers cite it as the blocker separating frozen-weight brackets from truly dynamical structure functions.

claimA lattice inverse metric $g^{-1}$ is phase-space constant if its value at every site is unchanged under variations of the canonical data. A fixed background weight $w$ represents $g^{-1}$ only if $g^{-1}$ is phase-space constant. There exists a concrete positive dynamic inverse metric that is not phase-space constant, hence is represented by no fixed background; the weighted Hamiltonian density therefore carries a genuine background structure function rather than a dynamical one.

background

This sits in the QG Seven-Gaps campaign, Pillar 1 (constraint algebra), downstream of the background-weighted hypersurface bracket. That upstream module generalizes the frozen hypersurface-deformation theorem to a Hamiltonian generator whose stiffness slot carries a fixed lattice weight $w:\mathbb{Z}/n\mathbb{Z}\to\mathbb{R}$, and derives the exact lattice bracket in which $w$ appears as a structure function.

Phase-space constancy means: changing the canonical data (configuration and momentum fields on the lattice) cannot change the inverse-metric value at any site. Fixed-background representation means the inverse metric coincides with (or is determined by) such a frozen $w$. The module introduces a concrete dynamic inverse metric built from explicit phase and configuration test points, together with positivity and non-constancy witnesses.

The local claim is a separation theorem: the weighted bracket technology is faithful only for the phase-space-constant sector; dynamical structure functions lie outside fixed-background representability.

proof idea

Definitions first: phase-space constancy of a lattice inverse metric, and the predicate that a fixed background represents it. A short lemma shows fixed backgrounds represent only constants, and an iff links existence of a representing background to phase-space constancy.

A concrete dynamic inverse metric is then exhibited, with auxiliary zero-phase and unit-configuration points. Positivity and an explicit witness establish it is a legitimate inverse metric; a direct evaluation shows it is not phase-space constant. Composing with the representation lemma yields that no fixed background represents this concrete metric.

A final packaging statement records that the weighted Hamiltonian carries a background (not dynamical) structure function in the sense of the upstream weighted bracket.

why it matters in Recognition Science

The module is imported by the Full Theory Ledger (Phase 0c), the machine-checked status record for the full quantum-gravity campaign: one boolean flag per pillar benchmark, flipped only when the target is kernel-checked and critic-passed. It supplies the negative control that fixed-weight structure functions cannot stand in for dynamical inverse metrics, so ledger claims about dynamical gravity must not silently reduce to the weighted frozen case.

In the Seven-Gaps constraint-algebra line this is the blocker between Pillar 1's weighted bracket (upstream) and any full-theory assertion that the structure functions themselves evolve. Without it, one could misread a background $w$ as a dynamical $g^{-1}$. It does not itself close a T0–T8 forcing step; it polices the gravity side of the ledger so that dynamical claims stay honest.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (20)