SchurOn
plain-language theorem explainer
The Schur bound on a complex region Ω is the pointwise disk condition ‖f(z)‖ ≤ 1 for every z in Ω. Recognition Stability Audit cites it as the global certificate that a Cayley field Ξ stays inside the unit disk on the audited domain. The declaration is a one-line propositional definition, not a proved theorem.
Claim. A function $f:\mathbb{C}\to\mathbb{C}$ is Schur-bounded on a set $\Omega\subseteq\mathbb{C}$ when $\|f(z)\|\le 1$ for every $z\in\Omega$.
background
Recognition Stability Audit (RSA) is the Lean interface for the paper pipeline that treats candidate existence claims as a compiler: front-end encodes a candidate into a forbidden boundary-hit for a bounded Cayley field Ξ; back-end supplies a finite certificate that Ξ stays Schur-bounded on the audited region, so the hit cannot occur.
The classical Schur class is the family of holomorphic maps of the disk into itself. Here the same disk bound is stated as a pure Prop on an arbitrary region Ω and map f, without holomorphicity baked in. Holomorphicity, openness, and connectedness are supplied later by the back-end lemmas that consume this predicate.
RSA sits on the canonical reciprocal cost $J(x)=\frac12(x+x^{-1})-1$ already formalized as Jcost; this module only references that cost layer and focuses on the audit checklist structures.
proof idea
Definitional abbreviation: the body is the universal quantification ∀ z ∈ Ω, ‖f z‖ ≤ 1. No tactics, no lemmas, no sorry. Downstream simp lemmas unfold it by rfl.
why it matters
SchurOn is the first field of the BackEnd structure: every RSA back-end certificate must assert a global Schur bound for Ξ on Ω, together with the derived no-boundary-hit conclusion. The pinch lemma eq_const_one_of_boundaryHit uses it with holomorphicity on a preconnected open set to force Ξ ≡ 1 after any interior boundary hit. The main back-end lemma no_boundaryHit_of_schur_holomorphic_nontrivial and the constructor backEnd_of_schur_holomorphic_nontrivial both take SchurOn as a hypothesis, so nontrivial Schur-holomorphic fields cannot hit the forbidden boundary state. RL micro-goals (goal_boundaryHit_forces_const_one, SchurOn_def) expose the same predicate for checklist-style training. In the paper this is the Schur/Herglotz half of the finite certificate that closes the audit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.