phaseSpaceDependentDiracPremise_two_site
plain-language theorem explainer
At two lattice sites, a concrete configuration-dependent inverse metric admits an honest Hamiltonian whose Hamiltonian–Hamiltonian bracket recovers the target dynamic structure function. Gravity and constraint-algebra workers cite this to discharge the phase-space-dependent Dirac premise in the Gap-5 residual DAG. The proof is a three-field structure inhabitant packaging the metric, its non-constancy, and the already-built Hamiltonian construction.
Claim. There exists a positive inverse-metric field $g$ on the two-site phase space that is not constant in the configuration coordinates, together with a differentiable Hamiltonian family $H_N$ built from $g$ such that the Hamiltonian–Hamiltonian Poisson bracket recovers the dynamic structure function $\sum_j (N_j M_{j+1}-M_j N_{j+1})\, g_j\, p_{j+1}(q_{j+1}-q_j)$.
background
Wave C2 of the Gap-5 residual DAG targets the dynamic structure-function identity on a discrete two-site phase space. The inverse-metric candidate is $g(x)_j = 1 + q_j^2$, which depends on the configuration coordinate at each site $j\in\mathbb{Z}/2\mathbb{Z}$ and is therefore not phase-space constant.
The naive lookalike that freezes $g$ into the static Hamiltonian slot fails: the configuration partial picks up an uncompensated $\partial g/\partial q$ term (residual R0). The honest Fréchet derivative, including those extra terms, cancels inside the Hamiltonian–Hamiltonian bracket, so the dynamic structure function is recovered exactly (residual R1).
PhaseSpaceDependentDiracPremise n packages existence of a non-constant inverse metric on $n$ sites together with a PhaseSpaceDependentHamiltonianConstruction for it. The upstream headline identity is bracket_HamDyn_HamDyn, which states the exact two-site dynamic structure-function formula for this concrete $g$.
proof idea
Term-mode structure inhabitant. The three fields of PhaseSpaceDependentDiracPremise 2 are filled by:
concreteDynamicInverseMetric(the model $g_j = 1+q_j^2$),concreteDynamicInverseMetric_not_constant(witnessed by comparing the zero and unit configuration points),- a singleton packing
concreteDynamicHamiltonianConstruction, itself the record with HamiltonianHamDyn, its differentiability proof, and the bracket identitybracket_HamDyn_HamDyn.
No new algebra is done here; the theorem is the packaging step that turns the R1 construction into the Dirac-premise interface expected by the residual DAG.
why it matters
Closes Wave C2 residual R2 (folded into R1 at $n=2$) in the Gap-5 constraint residual DAG. The sole downstream consumer is typedResidual_gap5_phaseSpaceDependentDirac_closed, whose body is exactly this theorem, marking the phase-space-dependent Dirac premise as discharged.
In the broader Recognition gravity program this is a discrete, two-site existence certificate that a configuration-dependent inverse metric can still generate a consistent Dirac-style constraint algebra via an honest Hamiltonian bracket. It does not flip gap5_constraint_recovery; continuum and HKT residuals remain open, as the module doc states. The result is local to the two-site model and does not yet address the eight-tick or $D=3$ forcing chain landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.