Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuantizedProofMethod

show as:
view Lean formalization →

Defines the Delta-audit interface for continuum problems: a problem is audited when it admits a finite reduction that transfers certificates from a discrete, quantized witness. Downstream Delta-native analysis and hard-problem audits import this scaffolding. The module is mostly structure and predicates (ProblemAudit, HasFiniteReduction, stubs), not a deep proof tree.

claimA continuum problem $P$ has a Delta audit when there exists a finite reduction $R$ such that certificates for the reduced discrete instance transfer back to $P$. The module packages the audit record, the finite-reduction predicate, and application stubs for quantized proof obligations.

background

In the Primitive Recognition Calculus, continuum claims are not accepted raw. They must pass a Delta audit: reduce to a finite certificate, then transfer the certificate back. The upstream module FiniteCertificateTransfer supplies the transfer mechanism; this module names the audit objects that sit on top of it.

Sibling definitions sketch the interface. ProblemAudit is the audit record for a continuum problem. HasFiniteReduction and problemAudit_finiteReduction assert that a finite reduction exists and is attached to the audit. ApplicationStub and StubObligation mark places where a concrete quantized proof still has to be filled in. The headline declaration quantized_proof_method_headline states the module thesis in one place.

The local setting is foundation-level: before mass ladders or forcing-chain landmarks (T5--T8), one needs a disciplined way to say that a continuum statement is only as strong as its finite witness.

proof idea

This is largely a definition and interface module, not a long proof development. It introduces the audit and finite-reduction predicates, wires them to FiniteCertificateTransfer, and leaves ApplicationStub / StubObligation as named holes for later concrete problems. Downstream modules import the interface and discharge or analyze specific audits; there is no single deep tactic script here.

why it matters in Recognition Science

Without a quantized proof method, continuum claims in Recognition Science would float free of finite certificates. This module is the named gate those claims pass through. It is imported by DeltaNativeAnalysis, DeltaNativeStrongClosure, and HardProblemCertificateAudits, which perform native Delta analysis, strong closure, and audits of hard problems respectively.

In the broader framework it supports the discipline behind forcing and cost arguments: uniqueness of $J$, the $\varphi$ fixed point, and related continuum identities are only trusted once a finite-certificate path exists. The stubs mark open application sites rather than closed physics results.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)