module module high

`IndisputableMonolith.URCAdapters.LNALReports`

This module aggregates LNAL reports and manifests for Certificate Engine v2, including invariants, compiler checks, opcode soundness, and cost ceilings with ΔJ bars and falsifier flags. Researchers auditing LNAL implementations against Recognition Science certificates would cite it to verify static gate status and VM preservation. The module structure consists of report functions that bundle data from imported certificates with no additional proofs.

claimAggregated manifest of LNAL invariants certificates with $\Delta J$ bars and falsifier flags, bundling VM preservation and token $\delta$-unit bounds from ConsentDerivative audits.

background

The module sits in the URCAdapters domain and aggregates reports from LNAL.Compiler, LNAL.JBudget, URCGenerators.LNALCerts, and Certificates.Consent. Upstream Consent provides ConsentDerivative audit certificates summarising static gate status. Upstream LNALCerts provides LNAL invariants certificate: bundles VM preservation and token δ‑unit bound. The module imports Mathlib and Lean.Data.Json to format the aggregated manifests.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module feeds aggregated reports into the broader URCAdapters and certificate system, supporting verification of LNAL invariants certificates. It aggregates data for Certificate Engine v2 to enable checks on J-cost differences and falsifier flags.

scope and limits

Does not prove theorems from the forcing chain T0 to T8.
Does not define the J function or Recognition Composition Law.
Does not implement the phi-ladder or mass formula.
Does not execute or compile LNAL code at runtime.

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Certificates.Consent module_import
IndisputableMonolith.LNAL.Compiler module_import
IndisputableMonolith.LNAL.JBudget module_import
IndisputableMonolith.URCGenerators.LNALCerts module_import

declarations in this module (19)

def lnal_invariants_report L14
def compiler_checks_report L19
def opcode_soundness_report L24
def schedule_neutrality_report L29
def cost_ceiling_report L34
def su3_mask_report L39
def previewNatArray L44
def jmonotone_report L52
def units_kgate_report L68
def mkJson L75
def lnal_invariants_report_json L81
def compiler_checks_report_json L85
def opcode_soundness_report_json L89
def schedule_neutrality_report_json L94
def cost_ceiling_report_json L98
def su3_mask_report_json L102
def jmonotone_report_json L107
def units_kgate_report_json L131
def lnal_manifest_json L136