YangMillsAnalyticLegitimate
plain-language theorem explainer
The legitimacy predicate on Yang–Mills analytic display records is the constant true proposition: every such display is treated as legitimate. Certificate-audit consumers of the Yang–Mills gap bridge cite it as the “legitimate” slot in the problem audit. The body is definitional, not a derived proof.
Claim. For every Yang–Mills analytic display record $d$ (a package of a Yang–Mills gap certificate, plaquette resolution, excitation level, and display payload), the legitimacy predicate on $d$ holds; equivalently, the predicate is the constant proposition $\top$.
background
This module builds audit scaffolding for hard-problem certificates in the Primitive Recognition Calculus. A Yang–Mills analytic display is a domain-specific record for the Yang–Mills bridge: it carries a gap certificate, a natural-number plaquette resolution, an excitation level, and a display payload kind.
Audits separate completion maps from two predicates on displays: legitimacy and pathology. Conservativity then requires that whenever a predicate holds of a completed display, the underlying certificate is recoverable unchanged. The present definition supplies the legitimacy side for the Yang–Mills analytic path.
In this layer, “legitimate” is not a dynamical or continuum claim about the mass gap; it is a bookkeeping Prop attached to the display type so the generic ProblemAudit interface can be instantiated uniformly across bridges (primes, Navier–Stokes, Hodge, Yang–Mills).
proof idea
There is no proof obligation. The declaration is a definition: the legitimacy predicate ignores its display argument and is definitionally True. Downstream, the conservativity theorem for the Yang–Mills analytic completion discharges the legitimate branch by returning the display’s own certificate with a reflexivity witness, which is possible precisely because legitimacy never constrains the display.
why it matters
It fills the legitimate field of yangMillsAnalyticAudit, the packaged ProblemAudit for Yang–Mills gap certificates with analytic displays. The companion theorem yangMillsAnalytic_conservative proves that both this legitimacy predicate and the matching pathology predicate are conservative for the analytic completion (certificate projection is identity on success).
Within Recognition Science foundation work, this is audit plumbing for the Yang–Mills gap certificate path, not a derivation of the continuum mass gap or a forcing-chain step (T0–T8). It keeps the hard-problem certificate layer honest: analytic displays can be marked legitimate by default while still forcing any nontrivial claim to live in the certificate or completion data rather than in a hidden hypothesis on the display.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.