concreteDynamicHamiltonianConstruction
plain-language theorem explainer
Packages the two-site dynamic Hamiltonian as an inhabitant of the phase-space-dependent Hamiltonian construction for the configuration-dependent inverse metric $1+q_j^2$. Cited by anyone closing the Wave C2 R1 residual or the two-site Dirac premise. The body is a structure instance wiring three already-proved fields: the Hamiltonian, its Fréchet differentiability, and the exact bracket identity.
Claim. On the two-site phase space, the Hamiltonian $\mathrm{Ham}_{\mathrm{dyn}}(N,x)=\sum_{i\in\mathbb{Z}/2\mathbb{Z}}(N_i/2)\bigl(p_i^2+(1+q_i^2)(q_{i+1}-q_i)^2\bigr)$ inhabits the phase-space-dependent Hamiltonian construction for the inverse metric $g(x)_j=1+q_j^2$: it is Fréchet differentiable in $x$, and the Hamiltonian–Hamiltonian bracket recovers the target dynamic structure function built from $g$.
background
Wave C2 targets typed residuals of the dynamic structure-function bracket on a discrete two-site phase space (configuration $q$ and momentum $p$ indexed by $\mathbb{Z}/2\mathbb{Z}$). The frozen (configuration-independent) Hamiltonian construction is inadequate once the inverse metric depends on $q$: a naive plug-in of $g(x)$ into the frozen slot leaves an uncompensated $\partial g/\partial q$ term in the configuration partial (residual R0, the decoy).
The honest candidate is $\mathrm{Ham}_{\mathrm{dyn}}$, the unfolded two-site sum used for Fréchet calculus. The model inverse metric is $g(x)_j=1+q_j^2$, a positive configuration-dependent candidate. The structure PhaseSpaceDependentHamiltonianConstruction demands three data: the Hamiltonian map, its differentiability, and the identity that the Hamiltonian–Hamiltonian bracket equals the dynamic structure function built from $g$.
Upstream, differentiable_HamDyn supplies Fréchet differentiability, and bracket_HamDyn_HamDyn is the R1 headline: the bracket of two dynamic Hamiltonians with lapses $N,M$ equals $\sum_j(N_j M_{j+1}-M_j N_{j+1}),g(x)j,p{j+1}(q_{j+1}-q_j)$.
proof idea
One-line structure instance. Set ham to $\mathrm{Ham}_{\mathrm{dyn}}$; discharge ham_differentiable by differentiable_HamDyn; discharge ham_ham by bracket_HamDyn_HamDyn. No new algebra is performed here: the hard work lives in the Fréchet derivative computation (including $\partial g/\partial q$) and the subsequent cancellation inside the Poisson bracket that recovers the target dynamic structure function.
why it matters
This is the R1 inhabitant named in the Wave C2 residual DAG: once the Fréchet derivative is computed honestly, the same candidate Hamiltonian that failed as a decoy (R0) becomes a legitimate phase-space-dependent construction for the concrete two-site inverse metric. Downstream it is the sole witness in typedResidual_dynamic_bracket_concrete_two_site and is packed into phaseSpaceDependentDiracPremise_two_site (the hard-core R2 corollary folded into R1 at $n=2$), which asserts existence of a non-constant inverse metric together with such a construction.
In the broader Seven Gaps gravity program this is a discrete, finite-site step toward dynamic structure functions needed for constraint recovery. It does not flip gap5_constraint_recovery; continuum and HKT residuals remain open. No direct appeal to the T0–T8 forcing chain or the Recognition Composition Law is required: the content is pure Hamiltonian geometry on a two-site phase space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.