ConsentInterfaceCert
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not establish consent for actions that alter sigma.
- Does not supply an empirical bridge to physical systems.
- Does not derive J-cost from the forcing chain inside this module.
- Does not treat multi-agent interactions beyond the single-agent criterion.
formal statement (Lean)
78structure ConsentInterfaceCert where
79 value_at_opt : ∀ s : ℝ, s ≠ 0 → valueFunctional s s = 1
80 sigma_pres_consensual : ∀ s s_max : ℝ, 0 < s → 0 < s_max →
81 IsConsensual s s s_max
82