Reference · Algorithm guarantees

rainbow.algorithms.proofs.decision-guarantee-audit

Algorithm guarantees src/rainbow/algorithms/proofs/decision_guarantee_audit.clj34 definitions, 11 theorems

Finite exact-rational decision-bound auditing as native proof data. Refusals are typed results of a deterministic premise checker. They are not kernel claims that the underlying proposition is false; they state that the declared proof route is unavailable without the required evidence.

audit/PremiseSet

DefinitionSource, line 177

audit/PremiseSet :
  → Type

audit/premises

DefinitionSource, line 184

audit/premises :
  (x₁ x₂ x₃ x₄ : data/Bool)
  → data/Product data/Bool (Product)
  where Product := data/Product data/Bool (data/Product data/Bool data/Bool)

audit/Claim

DefinitionSource, line 194

audit/Claim :
  → Type

audit/claim

DefinitionSource, line 211

audit/claim :
  (actions : Finset ℕ) (outcomes : ℕ → ℕ) (loss : ℕ → ℚ≥0) (bound : ℚ≥0)
  (premises : data/Product data/Bool (Product))
  → audit/Claim
  where Product := data/Product data/Bool (data/Product data/Bool data/Bool)

Finset = finset-data/Finsetℕ = data/Natℚ≥0 = nnrat/NonnegativeRational

audit/has-cap

DefinitionSource

audit/has-cap :
  (x₁ : data/Product data/Bool (Product))
  → data/Bool
  where Product := data/Product data/Bool (data/Product data/Bool data/Bool)

audit/has-support

DefinitionSource

audit/has-support :
  (x₁ : data/Product data/Bool (Product))
  → data/Bool
  where Product := data/Product data/Bool (data/Product data/Bool data/Bool)

audit/has-info-field

DefinitionSource

audit/has-info-field :
  (x₁ : data/Product data/Bool (Product))
  → data/Bool
  where Product := data/Product data/Bool (data/Product data/Bool data/Bool)

audit/has-no-hindsight

DefinitionSource

audit/has-no-hindsight :
  (x₁ : data/Product data/Bool (Product))
  → data/Bool
  where Product := data/Product data/Bool (data/Product data/Bool data/Bool)

nnrat/base-at-most

DefinitionSource, line 246

nnrat/base-at-most :
  (x₁ x₂ : ℚ≥0)
  → Prop

ℚ≥0 = nnrat/NonnegativeRational

nnrat/at-most

DefinitionSource, line 258

nnrat/at-most :
  (x₁ x₂ : ℚ≥0)
  → Prop

ℚ≥0 = nnrat/NonnegativeRational

audit/decide-nnrat-at-most

DefinitionSource, line 279

audit/decide-nnrat-at-most :
  (x₁ x₂ : ℚ≥0)
  → data/Bool

ℚ≥0 = nnrat/NonnegativeRational

audit/decision

DefinitionSource, line 296

audit/decision :
  (x₁ x₂ x₃ x₄ : data/Bool)
  → audit/AuditResult

audit/evaluate

DefinitionSource, line 320

audit/evaluate :
  (x₁ : data/Product data/Bool (Product)) (x₂ x₃ : ℚ≥0)
  → audit/AuditResult
  where Product := data/Product data/Bool (data/Product data/Bool data/Bool)

ℚ≥0 = nnrat/NonnegativeRational

audit-ex/action-space

DefinitionSource, line 335

audit-ex/action-space :
  → Finset ℕ

Finset = finset-data/Finsetℕ = data/Nat

audit-ex/outcome-support

DefinitionSource, line 342

audit-ex/outcome-support :
  → Finset ℕ

Finset = finset-data/Finsetℕ = data/Nat

audit-ex/accept

DefinitionSource

audit-ex/accept :
  → ℕ

ℕ = data/Nat

audit-ex/renegotiate

DefinitionSource

audit-ex/renegotiate :
  → ℕ

ℕ = data/Nat

audit-ex/decline

DefinitionSource

audit-ex/decline :
  → ℕ

ℕ = data/Nat

audit-ex/outcomes

DefinitionSource, line 356

audit-ex/outcomes :
  (x₁ : ℕ)
  → ℕ

ℕ = data/Nat

audit-ex/loss

DefinitionSource, line 363

audit-ex/loss :
  (x₁ : ℕ)
  → ℚ≥0

ℕ = data/Natℚ≥0 = nnrat/NonnegativeRational

audit-ex/cap-numerator

DefinitionSource

audit-ex/cap-numerator :
  → ℕ

ℕ = data/Nat

audit-ex/ten

DefinitionSource, line 389

audit-ex/ten :
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

audit-ex/three

DefinitionSource, line 393

audit-ex/three :
  → ℚ≥0

ℚ≥0 = nnrat/NonnegativeRational

audit-ex/complete-premises

DefinitionSource, line 397

audit-ex/complete-premises :
  → data/Product data/Bool (Product)
  where Product := data/Product data/Bool (data/Product data/Bool data/Bool)

audit-ex/missing-cap-premises

DefinitionSource, line 402

audit-ex/missing-cap-premises :
  → data/Product data/Bool (Product)
  where Product := data/Product data/Bool (data/Product data/Bool data/Bool)

audit-ex/missing-support-premises

DefinitionSource, line 407

audit-ex/missing-support-premises :
  → data/Product data/Bool (Product)
  where Product := data/Product data/Bool (data/Product data/Bool data/Bool)

audit-ex-1/claim

DefinitionSource

audit-ex-1/claim :
  → audit/Claim

audit-ex-2/claim

DefinitionSource

audit-ex-2/claim :
  → audit/Claim

audit-ex-3/claim

DefinitionSource

audit-ex-3/claim :
  → audit/Claim

audit-ex-4/claim

DefinitionSource

audit-ex-4/claim :
  → audit/Claim

audit-ex-1/result

DefinitionSource

audit-ex-1/result :
  → audit/AuditResult

audit-ex-2/result

DefinitionSource

audit-ex-2/result :
  → audit/AuditResult

audit-ex-3/result

DefinitionSource

audit-ex-3/result :
  → audit/AuditResult

audit-ex-4/result

DefinitionSource

audit-ex-4/result :
  → audit/AuditResult

nnrat/at-most-from-cross

TheoremFor all inputsNo axiomsSource, line 477

nnrat/at-most-from-cross :
  (left right : ℚ≥0) (ordered : nnrat/base-at-most left right)
  → left ≤ right

ℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most

nnrat/at-most-reflexive

TheoremFor all inputsNo axiomsSource, line 500

nnrat/at-most-reflexive :
  (value : ℚ≥0)
  → value ≤ value

ℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most

nnrat/at-most-transitive

TheoremFor all inputsNo axiomsSource, line 518

nnrat/at-most-transitive :
  (left middle right : ℚ≥0)
  (first : left ≤ middle)
  (second : middle ≤ right)
  → left ≤ right

ℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most

audit/decision-guarantee-sound

TheoremFor all inputsNo axiomsSource, line 554

audit/decision-guarantee-sound.{u, v} :
  (Action : Type u) (Outcome : Type v) (actions : Finset Action)
  (outcomes : Action → Outcome) (loss : Outcome → ℚ≥0) (bound : ℚ≥0)
  (premises : data/Product data/Bool (data/Product data/Bool (data/Product data/Bool data/Bool)))
  (cap : ℚ≥0) (support : Finset Outcome)
  (cap-present : product/first data/Bool (data/Product data/Bool (data/Product data/Bool data/Bool)) premises = data/true)
  (support-present : product/first data/Bool (data/Product data/Bool data/Bool) (product/second data/Bool (data/Product data/Bool (data/Product data/Bool data/Bool)) premises) = data/true)
  (no-hindsight-present : product/second data/Bool data/Bool (second) = data/true)
  (cap-law : ∀ (action : Action), ∀ (member : membership action), loss (outcomes action) ≤ cap)
  (support-law : ∀ (action : Action), ∀ (member : membership action), list/membership Outcome (finset-data/enumeration Outcome support) (outcomes action))
  (cap-within-bound : cap ≤ bound)
  (action : Action) (member : membership action)
  → loss (outcomes action) ≤ bound
  where membership := list/membership Action (finset-data/enumeration Action actions)
  where second := product/second data/Bool (data/Product data/Bool data/Bool) (product/second data/Bool (data/Product data/Bool (data/Product data/Bool data/Bool)) premises)

= = equality/EqFinset = finset-data/Finsetℚ≥0 = nnrat/NonnegativeRational≤ = nnrat/at-most

audit/refusal-path

TheoremFor all inputsNo axiomsSource, line 615

audit/refusal-path :
  (support hindsight ordered : data/Bool)
  → proposition/conjunction (decision = audit/missing-cap) (conjunction)
  where conjunction := proposition/conjunction (audit/decision data/true data/false hindsight ordered = audit/missing-support) (proposition/conjunction (audit/decision data/true data/true data/false ordered = audit/hindsight-premise) (audit/decision data/true data/true data/true data/false = audit/cap-exceeds-bound))
  where decision := audit/decision data/false support hindsight ordered

= = equality/Eq

audit-ex/loss-at-most-ten

TheoremFor all inputsNo axiomsSource, line 669

audit-ex/loss-at-most-ten :
  (outcome : ℕ)
  → (fun outcome₁ => audit-ex/loss outcome₁ ≤ audit-ex/ten) outcome

ℕ = data/Nat≤ = nnrat/at-most

audit-ex-1/all-losses-at-most-ten

TheoremFor all inputsNo axiomsSource, line 709

audit-ex-1/all-losses-at-most-ten :
  (action : ℕ) (member : list/membership ℕ (enumeration) action)
  → audit-ex/loss (audit-ex/outcomes action) ≤ audit-ex/ten
  where enumeration := finset-data/enumeration ℕ ahof-d40/candidates

ℕ = data/Nat≤ = nnrat/at-most

audit-ex-1/audit-approved

TheoremWorked exampleNo axiomsSource

audit-ex-1/audit-approved :
  → audit-ex-1/result = audit/approved

= = equality/Eq

audit-ex-2/refused-missing-cap

TheoremWorked exampleNo axiomsSource

audit-ex-2/refused-missing-cap :
  → audit-ex-2/result = audit/missing-cap

= = equality/Eq

audit-ex-3/refused-cap-exceeds-bound

TheoremWorked exampleNo axiomsSource

audit-ex-3/refused-cap-exceeds-bound :
  → audit-ex-3/result = audit/cap-exceeds-bound

= = equality/Eq

audit-ex-4/refused-missing-support

TheoremWorked exampleNo axiomsSource

audit-ex-4/refused-missing-support :
  → audit-ex-4/result = audit/missing-support

= = equality/Eq