naiveDynamicHamW
plain-language theorem explainer
Pointwise lookalike Hamiltonian: plug the configuration-dependent inverse metric into the frozen weighted density HamW on the two-site phase space. Gravity/QG residual work cites it as the R0 decoy against which the honest Frechet-aware dynamic Hamiltonian is compared. The body is a one-line composition, not a derived identity.
Claim. For a lapse $N:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$ and phase-space point $x=(q,\pi)$ on two sites, the naive dynamic density is $H_w[N](x)$ with weight $w_j=1+q_j^2$ (the concrete dynamic inverse metric at $x$), i.e. $\sum_i (N_i/2)\bigl(\pi_i^2+w_i(q_{i+1}-q_i)^2\bigr)$.
background
The ambient setting is the two-site lattice wave field. Phase space is pairs $(q,\pi)$ of maps $\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$. The frozen weighted Hamiltonian density $H_w[N]$ smears kinetic $\pi_i^2$ and stiffness $w_i(q_{i+1}-q_i)^2$ by the lapse $N$; its weight $w$ is a background function of the site alone, never of the phase-space point.
The concrete dynamic inverse metric replaces that background by a positive, configuration-dependent candidate $w_j(x)=1+q_j^2$. The module targets Wave C2 residuals R0 and R1 of the dynamic structure-function bracket: R0 is exactly the claim that naively substituting this $w(x)$ into frozen $H_w$ and reusing frozen partials fails, because $\partial/\partial q$ picks up an uncompensated $\partial w/\partial q$ term.
proof idea
Pure definitional wrapper: evaluate the weighted density at weight equal to the concrete dynamic inverse metric of the same phase-space point. No lemmas, no tactics; the equality with the named dynamic Hamiltonian is proved downstream by unfolding and ring.
why it matters
Names the R0 decoy explicitly so residual bookkeeping can separate "plug $g(x)$ into frozen $H_w$" from the honest Frechet construction. Downstream, HamDyn_eq_naive shows the packaged dynamic Hamiltonian agrees with this lookalike as a function of $(N,x)$, after which Frechet calculus (including $\partial g/\partial q$) is used to place it in the phase-space-dependent Hamiltonian construction at $n=2$ and recover the target dynamic structure function in the Hamiltonian–Hamiltonian bracket (R1).
It does not discharge continuum or HKT residuals, and the module doc states it does not flip gap5_constraint_recovery. Landmark contact is local QG structure-function work on the lattice, not the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.