PrimeAnalyticPathology
plain-language theorem explainer
The pathology predicate on prime-analytic display records is definitionally true for every input. Auditors of the prime-critical-line certificate bridge use it as the pathology half of a ProblemAudit pair. The body is the constant True, so the conservative check is immediate.
Claim. For every prime-analytic display record $d$ (a bundle of a prime-critical-line certificate, window radius, balance depth, and display payload), the pathology proposition associated to $d$ holds; it is definitionally $\top$.
background
This module builds certificate audits for several hard analytic and geometric problems inside the Primitive Recognition Calculus. Each audit pairs a domain certificate with a display record and two predicates: legitimate and pathology, plus a completion map and conservativity lemmas.
A prime-analytic display packages a prime-critical-line certificate together with a natural window radius, a balance depth, and a display payload. That structure is the sole argument of the pathology predicate defined here. Sibling audits cover Navier–Stokes energy, Yang–Mills gap, and Hodge algebraicity under the same pattern.
The surrounding import surface is Mathlib plus the quantized proof-method layer; the local goal is bookkeeping of certificate legitimacy versus pathology, not a new prime-number theorem.
proof idea
There is no proof obligation. The declaration is a definition that ignores its display argument and returns the proposition True. Downstream conservativity only needs that the predicate is inhabited, which is immediate from True.intro (or the corresponding constructor).
why it matters
It fills the pathology slot of primeAnalyticAudit, the ProblemAudit record for prime-critical-line certificates, and is one conjunct of the conservativity theorem for that completion. Without a named pathology predicate, the audit interface cannot be instantiated uniformly with the Navier–Stokes, Yang–Mills, and Hodge audits in the same module.
In the Recognition stack this is scaffolding for hard-problem certificate hygiene inside Foundation, not a step of the T0–T8 forcing chain, RCL, or the mass ladder. It lets later work treat prime-critical-line displays under the same legitimate/pathology discipline as the other bridges without claiming a resolution of the critical-line problem itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.