gap5_structure_function_blocker_certified
plain-language theorem explainer
Every fixed two-site background weight has an exact Hamiltonian bracket with that weight as structure function and reaches the weighted continuum, yet no such fixed weight equals the explicit positive dynamic inverse metric at all phase points. Gravity and QG campaign auditors cite this as the certified Gap 5 structure-function blocker in the full-theory ledger. The proof is a one-line re-export of the upstream background-weight blocker.
Claim. For every two-site weight $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the Hamiltonian $H_w$ has $w$ as a fixed background structure function in its Hamiltonian-Hamiltonian bracket; every continuous profile $W$ on $[0,1]$ has weighted continuum reach; and for every such $w$, $w$ does not represent the concrete dynamic inverse metric $g(x,j)=1+(x^1_j)^2$ at all phase-space points.
background
This module is the Phase 0c full-theory ledger for the quantum-gravity campaign: boolean flags per pillar benchmark flip only when the target theorem is kernel-checked. It re-anchors the seven-gaps starting line so the full-theory record cannot contradict the campaign ledger it extends.
Gap 5 concerns recovery of the gravitational constraint algebra via a weighted bracket. A fixed background weight $w$ on the two-site phase space yields the Hamiltonian family $\mathrm{Ham}W,w$. The proposition HamWHasBackgroundStructureFunction asserts that the exact bracket equals the discrete diffeomorphism form with structure function $w$ (phase-space constant). BackgroundWeightedContinuumReach is the continuum smearing limit of such fixed profiles. FixedBackgroundRepresents says a site weight equals a candidate inverse metric $g$ at every phase point and site. The model metric $g(x,j)=1+(x^1_j)^2$ is positive and configuration-dependent.
Upstream, gap5_background_weight_blocker already packages the three conjuncts: every $w$ has the background structure function, every continuous $W$ reaches the weighted continuum, and no fixed $w$ represents the dynamic metric.
proof idea
One-line term wrapper: the theorem is definitionally the upstream certified blocker gap5_background_weight_blocker from DynamicStructureFunctionBlocker. No new tactics or lemmas are introduced here; the ledger merely re-exports that conjunction under the Gap 5 structure-function name used by the full-theory status record.
why it matters
In the full-theory campaign, classical recovery (Pillar 1) needs a constraint algebra that reproduces Einstein gravity in the continuum limit. The weighted-bracket route toward gap5_constraint_recovery looked promising because fixed backgrounds already give exact brackets and continuum reach. This certificate shows that route is blocked: any structure function that represents the explicit positive dynamic inverse metric cannot be a fixed background weight. A genuinely dynamic structure function is required, and its substrate derivation remains open, so the Gap 5 flag stays false.
The declaration sits in FullTheoryLedger beside the other certified gap blockers and the master claim full_theory_not_yet_closed. It does not yet feed a downstream theorem (no used_by edges), but it is the machine-checked status line that keeps Pillar 1 from flipping until the dynamic-structure gap is closed. Relative to the Recognition forcing chain, this is campaign infrastructure rather than a T0-T8 landmark; it polices what counts as a completed classical-recovery step before continuum Einstein gravity can be claimed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.