gap5_background_weight_blocker
plain-language theorem explainer
The background-weighted Hamiltonian family has an exact lattice bracket with fixed site weights and continuum smearing reach for every continuous profile, yet no fixed two-site weight can match the explicit positive dynamic inverse metric at every phase-space point. Gravity auditors cite this as the certified Gap-5 structure-function blocker. The proof is a one-line packaging of three already-proved conjuncts.
Claim. For every two-site weight $w$, the weighted Hamiltonian $H_w$ has fixed background structure function $w$ in its Hamiltonian-Hamiltonian bracket; every continuous background profile $W$ on $[0,1]$ has continuum smearing reach (Riemann sums of $W\cdot W_r\cdot S$ tend to the corresponding integral); and no fixed two-site weight $w$ represents the concrete dynamic inverse metric $g(x,j)=1+(x^1_j)^2$ at all phase-space points and sites.
background
In the background-weighted Dirac bracket, a fixed site weight $w:(\mathbb{Z}/n)\to\mathbb{R}$ sits in the structure-function slot of the Hamiltonian-Hamiltonian bracket of $H_w$. The proposition that this holds exactly for every test densities $N,M$ and every phase point is the fixed-background structure-function claim. Separately, a continuous profile $W$ on $[0,1]$ has continuum smearing reach when the weighted Riemann sums of $W\cdot W_r\cdot S$ tend to $\int_0^1 W,W_r,S$ for continuous $W_r,S$.
A fixed weight $w$ represents a candidate inverse metric $g$ when $w_j=g(x)_j$ at every phase point $x$ and site $j$. The module records that any such representation forces $g$ to be phase-space constant. The concrete two-site model $g(x,j)=1+(x^1_j)^2$ is positive and not constant (witnessed by the zero and unit configuration points), so no fixed $w$ can represent it.
The local setting is Gap 5 of the gravity ledger: full ADM needs the inverse spatial metric in the structure slot to vary with canonical data, while the existing weighted bracket keeps the weight fixed as the phase point varies.
proof idea
One-line term proof: the conjunction is assembled by exact from three prior results. The first conjunct is the theorem that every two-site weight supplies the fixed-background structure-function proposition (the exact lattice identity bracket_HamW_HamW). The second is the continuum-reach theorem, which applies the existing quadrature/weightedStructureSum_tendsto result to every continuous profile on $[0,1]$. The third is the non-representation theorem for the concrete dynamic inverse metric, itself obtained from the equivalence "fixed background represents $g$ iff $g$ is phase-space constant" plus the explicit non-constancy witness for $g(x,j)=1+(x^1_j)^2$.
why it matters
This is the certified Gap-5 structure-function blocker. Downstream, gap5_structure_function_blocker_certified in the full theory ledger restates the same three conjuncts and concludes that the weighted-bracket route to constraint recovery needs a genuinely dynamic structure function; the substrate derivation of that dynamic object remains open and the closure flag stays false.
The module doc is explicit: no closure flag is changed. PhaseSpaceDependentHamiltonianConstruction names the missing Hamiltonian construction, and the Gap-5 dynamic Dirac/HKT rigidity target records that this construction and the existing HKT rigidity statement are separate remaining obligations. The blocker therefore separates what the background-weighted family already delivers (exact bracket, continuum reach) from what full ADM still requires (phase-space-dependent inverse metric in the structure slot).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.