yangMillsAnalyticCompletion
plain-language theorem explainer
Packages each finite Yang-Mills mass-gap certificate as a trivial analytic display (zero plaquette resolution, zero excitation level, connection-display tag) and certifies a display exactly when the certificate equals the display's embedded certificate. Auditors of the Yang-Mills gap bridge cite it as the native-to-display completion map. The body is a direct structure instance: display is a constant-payload constructor, certification is bare equality.
Claim. The Yang-Mills analytic completion is the map sending each finite mass-gap certificate $c$ to the analytic display record $(c,\,0,\,0,\,\mathrm{connection})$, together with the certification predicate that $c$ certifies a display $d$ precisely when $c=d.\mathrm{cert}$.
background
In the Primitive Recognition Calculus, hard-problem audits are organized by a completion interface: a map from native data $N$ to display data $D$, plus a relation saying which certificates cover which displays. The upstream Completion structure records exactly those two fields (display and certifies).
For Yang-Mills, the native inventory is the three-constructor certificate type: finite plaquette ledger, excitation-gap witness, and zero-mode obstruction witness. The analytic display record packages one such certificate with two natural-number resolution parameters (plaquette resolution, excitation level) and a payload tag (connection, excitation, or zero-mode).
This module sits in the hard-problem certificate-audit layer: each Millennium-style target gets a finite certificate inventory, a domain-specific display, and a completion that bridges them so conservativity and legitimacy checks can be stated uniformly.
proof idea
Pure structure instance, no tactics. The display field sends every certificate $c$ to the record with that same certificate, both resolution parameters set to $0$, and payload fixed to the connection-display tag. The certifies field is propositional equality of the certificate against the display's embedded cert field. No lemmas are invoked.
why it matters
This completion is the native-to-display bridge for the Yang-Mills mass-gap audit. Downstream, yangMillsAnalyticAudit installs it as the completion field of the full problem audit (alongside legitimate and pathology predicates), and yangMillsAnalytic_conservative proves both legitimacy and pathology are conservative for it by the one-line witness $d.\mathrm{cert}$.
In the Recognition framework it is scaffolding for the analytic side of the mass-gap certificate story: it does not itself force a spectral gap, but it makes the finite-certificate inventory speak the same display language used for the other hard-problem audits (primes, Navier-Stokes, Hodge). Conservativity of the audit then reduces to matching certificates on displays, which this definition makes definitional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.