cert_inhabited
plain-language theorem explainer
cert_inhabited establishes that ConsentInterfaceCert is non-empty by supplying the explicit witness cert. Researchers updating the pre-Big-Bang ethics section cite it to confirm the structural model for consent via J-cost is concretely realized. The proof is a direct term construction that packages the prior cert definition into the Nonempty type.
Claim. The structure ConsentInterfaceCert is inhabited: there exists a certificate $C$ such that for all nonzero $s$, valueFunctional$(s,s)=1$, and for all $s,s_max>0$, IsConsensual$(s,s,s_max)$ holds.
background
The module mechanizes the consent interface from J-cost as a tangent-data structure for bond-space directions together with algebraic closure of sigma-preserving moves. The recognition value functional is $V_i=1-J(sigma_i/sigma_max)$ where sigma_i is agent i's sigma-charge; consent holds precisely when the post-action J-cost on sigma_i does not increase. ConsentInterfaceCert encodes exactly these two properties: value_at_opt requires valueFunctional$(s,s)=1$ for nonzero $s$, while sigma_pres_consensual requires IsConsensual for positive charges.
proof idea
The proof is a one-line term that constructs the inhabitant of Nonempty ConsentInterfaceCert by applying the cert constructor directly to the definitions of valueFunctional and IsConsensual.
why it matters
This declaration closes the structural theorem for the consent interface, upgrading the SCAFFOLD tag in pre_big_bang_origin_paper.tex §consent to PARTIAL THEOREM. It supplies the concrete model required for the ethics upgrade inside the Recognition Science framework and sits immediately after the ConsentInterfaceCert structure definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.