ConsentCert
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.