ConsentInterfaceCert
plain-language theorem explainer
The ConsentInterfaceCert structure packages the optimum condition for the recognition value functional together with the sigma-preserving consent criterion. Researchers extending Recognition Science into ethical interfaces would cite it when formalizing agent consent from J-cost. It is assembled as a direct container for the two properties drawn from valueFunctional and IsConsensual.
Claim. A structure consisting of (i) $V(s,s)=1$ for all $s≠0$, and (ii) IsConsensual$(s,s,s_{max})$ for all $s,s_{max}>0$, where $V(σ,σ_{max}):=1-J(σ/σ_{max})$ and IsConsensual holds precisely when the value functional does not decrease.
background
The module defines the recognition value functional as $V_i=1-J(σ_i/σ_{max})$, with $J$ the J-cost from the forcing chain. IsConsensual$(σ_b,σ_a,σ_m)$ is the proposition that $V(σ_a,σ_m)≥V(σ_b,σ_m)$. The local setting upgrades the consent interface scaffold in pre_big_bang_origin_paper.tex §consent by mechanizing tangent-data structures and σ-preserving moves at the algebraic level.
proof idea
This is a structure definition that directly records the two fields value_at_opt and sigma_pres_consensual, each taken verbatim from the sibling definitions valueFunctional and IsConsensual. No lemmas or tactics are invoked.
why it matters
The structure supplies the certificate type used by the explicit cert construction and the inhabitedness theorem cert_inhabited in the same module. It upgrades the consent interface from SCAFFOLD to PARTIAL THEOREM in the pre-Big-Bang paper §ethics, linking the J-uniqueness step (T5) to agent-level constraints via the value functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.