Note_modVacuumSectorsRemainOpen
plain-language theorem explainer
Named honesty wall recording that C^{2} regularity plus the ham–ham functional equation do not force the kinetic/gradient sectors of CanonicalMom dynamics. The sqrt-affine profile is blocked from that sector only by structure-nonconstancy (g ≡ 1), and even that barrier was later superseded by the C4 variable-kinetic kill. Gap auditors cite it when tracking what remains open after the vacuum-sector counterexample. The body is the trivial proposition True.
Claim. The honesty note that $C^2$ regularity together with the alternating ham–ham functional equation alone do not force the kinetic/gradient sectors (the sqrt-affine profile is excluded from CanonicalMom only by structure-nonconstancy $g\equiv 1$, later superseded by the C4 variable-kinetic kill) is recorded as the trivial proposition $\mathrm{True}$.
background
Module setting is Wave C3 gap5: the unconditioned CanonicalMom rigidity statement at $n=2$ is false. The killer is a vacuum-shift density
$$h(a,b,p)=\tfrac12\bigl(p^2+(1+a^2)(b-a)^2\bigr)+a^2,\quad g(a)=1+a^2,$$
with $m_j=\pi_{j+1}(q_{j+1}-q_j)$ and $c_{\mathrm{Mom}}=1$. The ham–ham alternating functional equation is blind to the zero-gradient vacuum term $a^2$, so the rigidity conclusion would force a constant vacuum while this density evaluates to $q^2$ on coincident configurations.
The sqrt-affine profile does not lift to CanonicalMom: its FE forces $g$ constant, violating structure-nonconstancy, so it is not the kill. The repaired terminal is the mod-vacuum statement. Whether structure-nonconstancy plus the FE forces the kinetic/gradient sectors remains open mathematics; this note is the honesty wall for that residual gap.
proof idea
Definitional honesty wall: the body is simply True. No lemmas, no tactics. Downstream the companion theorem discharges it by trivial.
why it matters
Marks residual openness after the vacuum-sector kill of unconditioned CanonicalMom rigidity (gap5). Downstream the trivial theorem note_modVacuumSectorsRemainOpen is the C4 flip marker: bool status lives with the kill in HKTKineticNormalizedRigidity, and this note records the supersession. ContDiff-2 + FE alone never forced the kinetic/gradient sectors; the earlier witness was blocked only by structure-nonconstancy ($g\equiv 1$), and C4 shows structure-nonconstancy itself fails to close mod-vacuum via the variable-kinetic kill. Keeps auditors from flipping gap5_constraint_recovery or treating the repaired mod-vacuum terminal as a full sector classification. Local to the HKT rigidity gauge-scope adjudication (branch A), not a global RS forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.