YangMillsAnalyticPathology
plain-language theorem explainer
Trivial pathology predicate on Yang-Mills analytic displays: it holds for every display. The Yang-Mills analytic audit bundle wires it in as the pathology slot, and the matching conservativity lemma discharges against it by projecting the embedded gap certificate. The body is the constant true proposition, so no analytic obstruction is recorded at this layer.
Claim. For every Yang-Mills analytic display $d$ (a record carrying a gap certificate, plaquette resolution, excitation level, and display payload), the pathology predicate on $d$ holds; equivalently the predicate is the constant proposition $\top$.
background
This module builds certificate audits for several hard analytic problems (prime critical line, Navier-Stokes energy, Yang-Mills gap, Hodge). Each audit pairs a completion map with two predicates, legitimate and pathology, and asks that both be conservative relative to completion: they may only depend on the underlying certificate, not on display decoration.
A Yang-Mills analytic display is the domain-specific record for the Yang-Mills bridge: it packages a YangMillsGapCert, a natural plaquette resolution, an excitation level, and a display payload. The pathology slot is the Prop-valued check that the audit treats as the obstruction side of that pair.
Upstream, only the display structure is required. No deeper gap theorem is invoked here; the definition sits at the audit interface, not inside continuum Yang-Mills analysis.
proof idea
Pure definitional abbreviation: the predicate ignores its display argument and returns the constant true proposition. There is no tactic proof and no lemma application. Downstream conservativity for this predicate is the one-line projection that recovers the embedded gap certificate and reflexivity on the completion, which is valid precisely because the predicate never constrains the display.
why it matters
Fills the pathology field of yangMillsAnalyticAudit, the ProblemAudit bundle for the Yang-Mills gap certificate with analytic displays. Also appears in yangMillsAnalytic_conservative, which asserts joint conservativity of the legitimate and pathology predicates under analytic completion.
Inside Recognition Science this is scaffolding for hard-problem certificate hygiene, not a derivation of the mass gap from the forcing chain (T0-T8), the Recognition Composition Law, or the eight-tick octave. It records that, at present, the analytic-display layer imposes no extra pathology beyond what the gap certificate already carries. Parent consumers treat it as a conservative no-op obstruction check so the audit API stays uniform across problem domains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.