pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Certificates.Consent

show as:
view Lean formalization →

The Certificates.Consent module supplies the ConsentDerivative audit certificate summarizing static gate status in the LNAL framework. LNALReports adapters cite it when assembling formal verification outputs from the compiler. The module consists entirely of definitions drawn from the LNAL.Compiler import, with no theorems or proofs present.

claimThe module defines ConsentCert, the audit certificate that summarizes static gate status for the ConsentDerivative.

background

This module belongs to the Certificates domain and imports Mathlib together with IndisputableMonolith.LNAL.Compiler. Its sole sibling definition is ConsentCert, which encodes the static gate status summary. The local setting is therefore an audit layer over LNAL compilation results, providing a fixed certificate object rather than any derived theorem.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds IndisputableMonolith.URCAdapters.LNALReports by supplying the ConsentDerivative certificate structure required for LNAL report generation. It completes the static gate status component needed for downstream formal reporting in the Recognition Science certificate chain.

scope and limits

used by (1)

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 (1)