structure
definition
ExclusivityCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.ExclusivityProof on GitHub at line 99.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
96
97/-! ## Certificate -/
98
99structure ExclusivityCert where
100 chain_valid : Nonempty RCLDerivation
101 cost_unique : ∀ (ec : ExclusivityConstraints), ec.all_hold →
102 ∃ (J : ℝ → ℝ), (∀ x, 0 < x → J x ≥ 0) ∧ J 1 = 0
103
104theorem exclusivity_cert_exists : Nonempty ExclusivityCert :=
105 ⟨{ chain_valid := rcl_chain_is_valid
106 cost_unique := constraints_determine_cost }⟩
107
108end IndisputableMonolith.Foundation.ExclusivityProof