SolveProfileFEQuadratic
plain-language theorem explainer
Packages the full PDE conclusion for a CanonicalMom HKT target: some smooth local Hamiltonian profile is exactly the ADM quadratic form with nonzero kinetic, gradient, and momentum coefficients linked by c_Mom = 4 c_Kin c_Grad, and the structure and momentum densities match the profiled ansatz. Gravity workers on gap-5 rigidity cite it as the Prop that later sessions must inhabit. It is a pure definition (existential Prop), not a proved theorem.
Claim. For a CanonicalMom point-split HKT target $T$, there exist a smooth local Hamiltonian profile $h$, a structure map $g:\mathbb{R}\to\mathbb{R}$, and coefficients $c_{\mathrm{Kin}},c_{\mathrm{Grad}},c_{\mathrm{Vac}},c_{\mathrm{Mom}}\in\mathbb{R}$ with $c_{\mathrm{Kin}},c_{\mathrm{Grad}},c_{\mathrm{Mom}}\neq 0$ and $c_{\mathrm{Mom}}=4\,c_{\mathrm{Kin}}c_{\mathrm{Grad}}$, such that $T$'s Hamiltonian density equals $h$ on adjacent phase-space slots, its structure function is $g$ of the configuration coordinate, $h(a,b,p)=c_{\mathrm{Kin}}p^{2}+c_{\mathrm{Grad}}\,g(a)(b-a)^{2}+c_{\mathrm{Vac}}$, and its momentum density is $c_{\mathrm{Mom}}\,p_{j+1}(q_{j+1}-q_{j})$.
background
Module context is Wave C2 gap5, session C1 of the CanonicalMom rigidity route (binding design D-qg-hkt-rigidity-route-20260722). Session C1 extracts the alternating functional equation forced by the ham-ham identity under local, structure, and canonical profiles at $n=2$, and freezes the remaining differentiation/integration wall as named Props so later sessions only owe the PDE core.
A local Hamiltonian profile is a map $h(a,b,p)$ on adjacent configuration values and a momentum slot. Smoothness packages Frechet coefficients of $h$ in phase-space coordinates. The ADM quadratic ansatz is the standard kinetic-plus-gradient-plus-vacuum split; CanonicalMom further ties the momentum density to a single coefficient times $p_{j+1}(q_{j+1}-q_j)$.
Sibling obligations HpLinearInP and HbPIndependent record the intermediate PDE steps: the momentum partial of $h$ must be linear in $p$, and the configuration partial must be $p$-independent. Session C2 is expected to force those after a ContDiff strengthening, then integrate back to the quadratic form packaged here.
proof idea
No proof body: this is a definitional Prop. The right-hand side is an existential package over a smooth local profile $h$, a structure map $g$, and four real coefficients, conjoined with the nonzero and $c_{\mathrm{Mom}}=4 c_{\mathrm{Kin}} c_{\mathrm{Grad}}$ constraints, the two density-matching identities for Hamiltonian and structure, the pointwise ADM quadratic formula for $h$, and the CanonicalMom formula for momentum density. Downstream lemmas inhabit or consume this Prop; they do not expand it further.
why it matters
This is the full PDE conclusion Prop for CanonicalMom rigidity. The glue theorem canonicalMom_rigidity_of_FE_solution states that any witness of this Prop yields the CanonicalMom rigidity conclusion (nonzero coefficients with $c_{\mathrm{Mom}}=4 c_{\mathrm{Kin}} c_{\mathrm{Grad}}$ and the profiled densities). The universal quantification solve_profile_FE_quadratic asserts the Prop for every CanonicalMom target; the sanity theorem shows the honest HamDyn target inhabits it by explicit coefficients.
In the PDE module, SolveProfileFEQuadratic_of_smoothScopedData discharges the Prop from smooth-scoped data via an ADM-quadratic-of-gauges lemma, and hamDyn_smooth_scoped_rigidity records the resulting coefficient form. Session C1 leaves the Prop open as a defined interface; C2+ is charged with ContDiff strengthening, then HpLinearInP, then HbPIndependent, then integration back to $h$. Binding constraints: do not flip gap5 constraint recovery, and do not claim the full N=2 CanonicalMom rigidity statement as a theorem from this definition alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.