ConsentCert
ConsentCert is a record that holds the enabled flag, verification outcome, violation list, and messages for the ConsentDerivative static gate. Manifest builders such as lnal_manifest_json cite it when assembling aggregated certificate outputs. The definition supplies a direct field-mapping constructor from CompileReport together with a source-string wrapper that invokes the compiler.
claimA consent certificate is a 4-tuple $(b_e, b_o, v, m)$ where $b_e, b_o$ are booleans, $v$ is a list of natural numbers indexing violations, and $m$ is a list of diagnostic strings.
background
The Certificates.Consent module supplies audit records for static gates inside the LNAL compiler pipeline. ConsentCert records the consent sub-report produced by CompileReport. The fromReport constructor copies the four consent fields and populates messages according to the enabled and ok flags; fromSource is a thin wrapper that runs compile before delegating to fromReport.
proof idea
The structure declaration supplies default empty lists for violations and messages. fromReport performs a direct field projection with a nested conditional that emits either an empty list or a single diagnostic string. fromSource is a one-line wrapper that pattern-matches the result of compile and passes the report onward.
why it matters in Recognition Science
ConsentCert supplies the consent component consumed by lnal_manifest_json when it builds the full Certificate Engine v2 manifest containing ΔJ bars and falsifier flags. It therefore closes the static verification step for the ConsentDerivative gate inside the LNAL report pipeline.
scope and limits
- Does not execute the source program at runtime.
- Does not compute J-cost, defectDist, or any phi-ladder quantities.
- Does not inspect the mathematical validity of the LNAL program itself.
formal statement (Lean)
11structure ConsentCert where
12 enabled : Bool
13 ok : Bool
14 violations : List Nat := []
proof body
Definition body.
15 messages : List String := []
16deriving Repr
17
18@[simp] def ConsentCert.verified (c : ConsentCert) : Prop := c.ok = true
19
20def ConsentCert.fromReport (report : CompileReport) : ConsentCert :=
21 { enabled := report.consent.enabled,
22 ok := report.consent.ok,
23 violations := report.consent.violations,
24 messages :=
25 if report.consent.enabled then
26 if report.consent.ok then []
27 else ["ConsentDerivative gate violated"]
28 else if report.consent.violations.isEmpty then []
29 else ["ConsentDerivative gate disabled; potential violations detected"] }
30
31noncomputable def ConsentCert.fromSource (src : String) (enableGate : Bool := false) : ConsentCert :=
32 let (report, _) := compile src enableGate
33 fromReport report
34
35end Certificates
36end IndisputableMonolith