Pith. sign in
module module high

IndisputableMonolith.Verification.RecognitionStabilityAudit.Core

show as:
view Lean formalization →

Core interface layer for the Recognition Stability Audit (RSA). It defines the Schur-bound predicate on a region Ω, boundary-hit events, the RSA problem package, and the Cayley field built from a sensor. Front-end and back-end audit modules import this layer as shared vocabulary. Mostly definitions and interface wiring rather than deep proofs.

claimShared RSA core objects: a Schur (disk) bound $\|f(z)\|\le 1$ for all $z\in\Omega$; a boundary-hit predicate at a point; an RSA problem package; and the Cayley field $\Xi$ from a sensor $\mathcal{J}$ via $\Xi=\theta(\mathcal{J})=(2\mathcal{J}-1)/(2\mathcal{J}+1)$.

background

Recognition Stability Audit (RSA), as in papers/tex/Recognition_Stability_Audit.tex, checks whether a holomorphic obstruction can force a boundary hit of a Cayley-transformed sensor field, or whether a Schur bound plus analyticity rules such hits out.

The Cayley plumbing module supplies the algebraic map sending the closed right half-plane into the closed unit disk. This Core module sits above that algebra and names the audit predicates: SchurOn (disk bound $|f z|\le 1$ on a region $\Omega$), BoundaryHitAt, the Problem bundle, and XiFromSensor building $\Xi$ from a sensor $\mathcal{J}$.

Cost is imported for the ambient recognition-cost language; the audit itself is complex-analytic and operator-norm style rather than a direct J-cost identity.

proof idea

This is a definition and interface module, not a theorem file. It introduces named predicates and data bundles (Schur bound on $\Omega$, boundary hit, Problem, $\Xi$ from sensor, FrontEnd/BackEnd hooks, correctness) that FrontEnd and BackEnd instantiate. No substantial proof obligation lives here; argument structure is deferred to those consumers and to the Cayley algebra underneath.

why it matters in Recognition Science

RSA's umbrella re-exports this core so downstream code can import one module. FrontEnd uses the shared vocabulary to turn an obstruction $G$, sensor $\mathcal{J}:=1/G$, and Cayley field $\Xi$ into a pole-implies-boundary-hit step. BackEnd assumes a Schur bound $|\Xi z|\le 1$ on $\Omega$, analyticity, and nontriviality, then argues a Herglotz/Schur pinch with no boundary hits.

Without this layer, front-end obstruction language and back-end disk-bound language would drift. In the broader Recognition stack the audit is a verification tool for stability of recognition fields, not a forcing-chain step (T5–T8), but it sits in the Verification domain that certifies claims built on those foundations.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)