differentiable_MomBalanced
plain-language theorem explainer
For any real weight map on Z/2Z, the balanced momentum functional on two-mode phase space is differentiable over the reals. HKT rigidity and gap-5 workers cite it when wiring the balanced quartic into the weak point-split target. The proof is a one-line term: the existing Fréchet derivative at each point yields DifferentiableAt, hence Differentiable.
Claim. For every weight $w:\mathbb{Z}/2\mathbb{Z}\to\mathbb{R}$, the balanced momentum map $x\mapsto\sum_{j\in\mathbb{Z}/2\mathbb{Z}} w(j)\,\rho^{\mathrm{mom}}_{\mathrm{bal}}(x,j)$ is differentiable as a real-valued function on two-mode phase space.
background
Module setting is Wave C2 gap5: kill strong rigidity and repair the CanonicalMom class (binding design D-qg-hkt-rigidity-route-20260722). Session A inhabits the strong point-split target by the balanced quartic falsifier; Session B defines the CanonicalMom variant, exhibits an honest HamDyn inhabitant, and banks a DEFINED-only rigidity statement. No ledger flag is flipped.
The balanced momentum functional is the weighted sum, over the two Z/2Z modes, of the balanced quartic momentum densities on PhaseSpace 2. Differentiability is the global property that every point admits a Fréchet derivative; the sibling lemma already constructs that derivative (MomBalancedD) and proves HasFDerivAt at every phase-space point by rewriting the sum as an explicit polynomial combination of coordinate projections.
proof idea
One-line term proof. At each phase-space point x, apply the sibling lemma hasFDerivAt_MomBalanced to obtain HasFDerivAt of MomBalanced w at x, then project to DifferentiableAt via the standard HasFDerivAt.differentiableAt coercion. The resulting pointwise DifferentiableAt bundle is exactly Differentiable ℝ (MomBalanced w).
why it matters
Feeds the construction of quarticBalancedWeakTarget, the balanced-quartic inhabitant of the weak point-split schema (hamDensity, momDensity, structureFunction, and the two hamAdv maps). That target is the Session-A/B witness separating the balanced quartic from strong rigidity while keeping CanonicalMom honest. Inside the SevenGaps gravity stack it is a small calculus lemma, not a physics claim: it licenses later variational or advective arguments that need the momentum side of the balanced quartic to be a C^1 functional on PhaseSpace 2. It does not flip gap5_constraint_recovery; it only clears the differentiability obligation on the momentum density used by the weak target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.