StubObligation
plain-language theorem explainer
Every Millennium-facing application stub carries a uniform propositional obligation, currently discharged as the trivial proposition True. Anyone wiring a hard-problem name into the quantized proof method cites this to mark that a certificate-preserving audit is still owed. The definition is a one-line constant Prop, not a proof.
Claim. For every application stub $s$ (prime critical line, Navier–Stokes energy transfer, Yang–Mills mass gap, or Hodge finite algebraic witness), the stub obligation of $s$ is the proposition $\top$.
background
The module packages a quantized proof method: continuum problems are meant to be audited by a certificate-preserving completion interface so that both legitimate displays and pathologies collapse to finite certificates.
ApplicationStub is an inductive name tag for the first four hard-problem targets. The doc states these are typed targets for the finite-certificate method, not solutions. Sibling notions include problem audits and the finite-reduction property that every such audit admits a finite certificate.
Upstream, the method sits beside TraceLogic conjunctions of stable trace predicates and the broader Clifford/8-tick bridge, but this definition only depends on the stub type itself.
proof idea
Pure definitional abbreviation. The body ignores the stub argument and returns the constant proposition True. No lemmas, tactics, or algebraic reduction are involved.
why it matters
It is the uniform placeholder obligation attached to every Millennium-facing stub until a concrete problem audit is supplied. The headline theorem quantized_proof_method_headline packages two conjuncts: every problem audit has a finite reduction, and every stub satisfies StubObligation s = StubObligation s (by reflexivity). Downstream, strong-closure certificate assembly in Delta-native closure can mention the same stub surface. In the Recognition stack this is scaffolding language for T0–T8-style forcing applied to open continuum problems, not a solved mass-gap or RH claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.