identityCertificateAudit
plain-language theorem explainer
The identity audit packages a finite certificate type as a full Delta audit of a continuum problem: display is the identity map, both legitimacy and pathology are the trivial (always-true) schema predicates, and both are conservative under identity completion. Anyone wiring a hard-problem certificate (primes, Navier–Stokes, Yang–Mills, Hodge) into the quantized proof method cites this base case. The construction is a four-field structure instance filled by the identity completion and its conservativity lemma.
Claim. For any type $C$, the identity audit is the Delta audit of a continuum problem with native type, display type, and certificate type all equal to $C$, whose completion is the identity completion (display $=\mathrm{id}$, certifies by equality), whose legitimacy and pathology predicates are the trivial schema predicates (always true), and whose two conservativity obligations hold by the identity-completion conservativity lemma.
background
In the quantized proof method, a ProblemAudit is the Delta audit of a continuum problem: a completion interface from a native type $N$ through a display type $D$ to certificates $Cert$, together with two predicates on $D$ (legitimate vs pathology) that are each required to be conservative for that completion. Conservativity means every display witness that satisfies the predicate lifts to a native certificate the completion accepts.
Identity completion is the base case: display is the identity on $N$, and a certificate certifies a display exactly when they are equal. Its conservativity theorem states that for any predicate $P$ on $N$, every $d$ with $P(d)$ is certified by $d$ itself. The two native schema predicates used here (legitimate and pathology) are both the constantly-true proposition on the certificate type; later analytic interfaces may refine them to problem-specific good or bad events.
This module sits in the Primitive Recognition Calculus foundation layer and supplies the audit scaffolding for the hard-problem certificate types (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraic).
proof idea
Four-field structure instance, not a tactic proof. Completion is set to identity completion on $C$. Legitimate and pathology are the two constantly-true schema predicates. Each conservativity field is discharged by a direct application of the identity-completion conservativity theorem to $C$ and the corresponding predicate: given a display $d$ satisfying the predicate, return certificate $d$ with reflexivity of equality.
why it matters
This is the uniform base audit that every hard-problem certificate in the module instantiates. Downstream, the prime-critical-line, Navier–Stokes energy, Yang–Mills gap, and Hodge algebraic audits are each one-line specializations of the identity audit to their finite certificate types. It closes the schema layer of the Delta audit before any analytic refinement of legitimacy or pathology, so the quantized proof method can treat those four continuum problems under a common conservative-completion interface. In the Recognition Science stack this is foundation scaffolding for certificate-preserving reductions, not a forcing-chain (T0–T8) step; it does not yet encode mass ladders, the eight-tick octave, or the J-cost law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.