CertificateLegitimate
plain-language theorem explainer
Schema-layer legitimacy predicate on finite certificates: every certificate of any type is treated as legitimate. Hard-problem audit constructors (identity audits over certificate types) plug this in as the default legitimate field. The body is the constantly-true proposition, so the schema never rejects a certificate here; later analytic interfaces are expected to refine it.
Claim. For an arbitrary certificate type $C$ and any certificate $c\in C$, the native legitimacy predicate holds. Equivalently, the predicate is the constantly true proposition on $C$.
background
This module builds schema-level audits for hard-problem certificates (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraicity). An audit packages a completion map together with two predicates: legitimacy and pathology, plus conservation lemmas that those predicates are stable under the completion.
At the schema layer, legitimacy is intentionally unconstrained. The same pattern appears elsewhere in the stack: ledger admissibility in the recognition operator and in information thermodynamics is defined as True on every state, so a hypothesis of admissibility adds no content until a later carrier specializes it. The companion pathology predicate is dual: every obstruction certificate is admissible at schema level, with problem-specific bad events deferred.
The identity audit then wires this predicate in as the legitimate field over a finite certificate type, with the identity completion and a matching pathology field.
proof idea
Pure definitional abbreviation: the predicate is definitionally equal to the constantly true proposition on the certificate type. No lemmas, no tactics, no hypotheses beyond the dummy certificate argument that fixes the type.
why it matters
Gives the default legitimate slot for identityCertificateAudit, which builds a full ProblemAudit over a finite certificate type with identity completion and conservative legitimacy/pathology. Sibling audits (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraic) sit in the same module and share this schema pattern: schema predicates stay trivial so that later analytic interfaces can refine legitimacy to problem-specific certificates without rewriting the audit plumbing.
In the Recognition stack this is foundation scaffolding, not a forcing-chain step (T5–T8) or an RCL identity. It keeps hard-problem certificate audits honest about what is proved versus what is only schema-admissible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.