finite_helicity_of_H1
plain-language theorem explainer
Finite initial energy supplies an explicit upper bound on helicity in the D=3 topological model. Researchers deriving the capacity veto on rigid rotations cite this step to guarantee that linking budgets remain finite before applying Alexander duality. The proof is a one-line term construction that selects the energy value itself as the witness and invokes reflexivity of the order relation.
Claim. Let $E$ be a real number satisfying $0leq E$. Then there exists a real number $B$ such that $0leq Bleq E$, serving as an upper bound on the helicity.
background
The module develops the topological capacity veto in three spatial dimensions, using Alexander duality to define an integer linking invariant that exists only for D=3. Each crossing carries a positive cost ln φ drawn from the Recognition Composition Law. The shifted cost function satisfies H(x) = J(x) + 1 = ½(x + x^{-1}), converting the RCL into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). Helicity is the topological invariant whose magnitude is controlled by the L2 energy norm of the initial data u0.
proof idea
The term proof directly supplies the witness energy together with the nonnegativity hypothesis. It closes the inequality energy ≤ energy by applying the reflexivity theorem le_refl from ArithmeticFromLogic.
why it matters
The declaration supplies F6.2.3 in the Foundation paper F6, establishing the finite helicity budget that precedes the finite_capacity_veto result. That veto shows rigid rotation cannot emerge from finite-energy initial data. The step therefore supports the eight-tick periodicity and the restriction to D=3 by keeping all topological invariants finite under the energy constraint. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.