Det2Lipschitz
plain-language theorem explainer
The definition encodes the condition that the map from Hilbert-Schmidt operators to det₂ values is Lipschitz continuous with constant L. Number theorists working on the Riemann hypothesis via the Christmas route cite this predicate when splitting the attachment error into continuity, prime-tail, and window-leakage budgets. The body is a direct conjunction of nonnegativity of L with a uniform scaling inequality that stands in for operator continuity on compact sets.
Claim. Let $L$ be a real number. The predicate holds precisely when $L$ is nonnegative and, for every nonempty set $K$ of complex numbers, there exists a real $C$ such that $C e$ is at most $L e$ for every nonnegative error $e$. This abstracts the claim that the determinant map satisfies $||det_2(I-A)-det_2(I-B)|| ≤ L ||A-B||_{HS}$ on compact subsets of the domain.
background
The module decomposes the attachment error between the truncated and certified J functions into three separately verifiable budgets for the Riemann hypothesis Christmas route. The local setting keeps the J functions abstract as maps from complex numbers to complex numbers, separating topological reasoning from explicit prime-sum estimates. Upstream results supply the dimensionless bridge ratio K defined as the square root of phi, together with structural theorems from PrimitiveDistinction that reduce seven axioms to four substantive conditions and three definitional facts.
proof idea
The definition is given directly by the conjunction of the inequality 0 ≤ L with a quantified statement that introduces a scaling constant C for each nonempty set K and then requires the inequality C errHS ≤ L errHS to hold for all nonnegative errHS. No lemmas are applied; the body is the complete definition and functions as a placeholder interface until Hilbert-Schmidt operators receive concrete Lean representations.
why it matters
This predicate supplies the continuity budget that enters the main theorem attachmentWithMargin_of_threeBudgets, which concludes attachment-with-margin once the three budgets sum to at most m/4. It corresponds to the proposition on Hilbert-Schmidt to det₂ continuity stated in Riemann-Christmas.tex and supports the error control required for the Riemann hypothesis formalization inside the Recognition Science framework. The definition defers concrete operator estimates to later number-theoretic work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.