Pith. sign in
module module low

IndisputableMonolith.Verification.KnetDerivationCert

show as:
view Lean formalization →

Verification module packaging a certificate that a Knet derivation obeys the Coercive Projection Method (CPM) Law of Existence. Auditors cite it when checking that local projection-defect, coercivity, and aggregation hypotheses are wired into a single cert object. Structure is definitional: it imports the generic A/B/C CPM core and exposes a named certificate bundle rather than a deep proof.

claimA verification certificate object asserting that a Knet derivation satisfies the three CPM Law-of-Existence clauses: (A) a projection-defect inequality, (B) coercivity factorization in which an energy gap controls the defect, and (C) an aggregation principle under which local tests imply membership.

background

Recognition Science verification modules package machine-checkable certificates that named physical or combinatorial derivations sit inside the Coercive Projection Method (CPM). The upstream module LawOfExistence supplies the generic, domain-agnostic A/B/C skeleton: A is a projection-defect inequality, B factors coercivity so that an energy gap controls the defect, and C aggregates local tests into membership.

This module specializes that skeleton to a Knet derivation. In the RS setting, such certificates sit in the Verification domain and are meant to be consumed by higher-level audit or export layers rather than by the forcing chain (T0–T8) itself. Notation and inequality shapes are inherited from the CPM core; no new cost functional (e.g. $J$) is introduced here.

proof idea

Definition and packaging module, not a deep proof development. It imports Mathlib and the CPM Law-of-Existence core, then exposes a certificate bundle (sibling KnetDerivationCert) that records the A/B/C hypotheses and any linking lemmas for the Knet case. Argument structure is wiring and type-level assembly of the generic projection-defect, coercivity, and aggregation interfaces rather than a multi-step tactic proof.

why it matters in Recognition Science

Gives the Verification layer a named, reusable certificate that a Knet derivation has been placed under CPM Law of Existence. Downstream consumers (none listed yet in the graph) would cite this when discharging existence or membership obligations that depend on projection-defect control and local-to-global aggregation. It does not advance the T0–T8 forcing chain, RCL, or the phi-ladder mass formula; it only certifies that one derivation channel is CPM-shaped. With empty used-by edges, its present role is archival and audit-facing inside the monolith.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)