until
plain-language theorem explainer
Source fragment at line 402 is not a mathematical theorem: the parser captured the English clause “theorem until a proof lands” from a closing doc-comment, with empty proof body and no type. Gravity auditors should treat it as documentation residue in the HKT point-split repair module, not a citeable lemma. Nothing is proved; downstream “uses” are almost certainly spurious token matches on the word until.
Claim. No proposition is stated. The line is residual documentation text of the form “theorem until a proof lands,” not a typed claim $P$ with a proof term. In particular it does not assert existence, uniqueness, or any identity for the point-split Hojman–Kuchař–Teitelboim momentum sector.
background
Module context is the Wave C2 R5 repair of the HKT dynamic target in Recognition gravity. The widened dynamic target keeps an unsplit momentum–Hamiltonian field that cannot be inhabited by honest nearest-neighbor local momentum profiles against the frozen quadratic Hamiltonian: at lattice size $n=2$, unsplit advection forces a singular relation when $p_0+p_1=0$.
The repaired sibling replaces that unsplit field by a smeared point-split momentum density (source/target advection densities already used in the HamDyn brackets). On $\mathrm{ZMod},2$ one has $-1=1$, so the symmetric generator is identically zero and the older $D_{\mathrm{gen}}^{\mathrm{sym}}$ sketch is empty at HamDyn size. The momentum sector is not abelian: the momentum–momentum bracket carries a Wronskian density.
The module states explicitly that no rigidity theorem is proved and no ledger flag is flipped. The load-bearing class is the strong point-split target; the weak target is schema-only after adjudication.
proof idea
There is no proof. Reported proof body length is zero, dependency count is zero, and the signature is not a well-formed Lean theorem (no type after the name, comment closer inline). Nothing is applied: no lemmas, no tactics, no term mode. Treat as a parse artifact of a doc-comment sentence, not as a wrapper or stub proof.
why it matters
Inside Recognition Science this file sits in the gravity seven-gaps stack repairing the HKT dynamic target so local momentum profiles can meet a frozen quadratic Hamiltonian without the unsplit singularity. That is infrastructure for quantum-gravity side conditions, not a step of the T0–T8 forcing chain, not an RCL identity, and not a mass-ladder or $\alpha$ result.
Reported consumers (baryon rung product, cosmic scale factor, recognition-equilibrium cost vanishing, d’Alembert square identity, circle $H_1$ computations, canonical RCL surface) do not mathematically depend on this fragment; the edge list is inconsistent with an empty untyped declaration and should be ignored by auditors.
What remains open in the module’s own terms is rigidity for the point-split target and the analogous unsplit obstruction against campaign HamDyn. This line closes none of that.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.