Lax Lean Archive

The duplication incentive survives every choice of error weights

Lax303562.WeightedFamily · concepts/Lax303562/WeightedFamily.lean · lax-303562

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Panoptic Quality is the member a=b=½a = b = ½ of the family of metrics

    ma,b=sn+a ∣FP∣+b ∣FN∣,m_{a,b} = \frac{s}{n + a\,|FP| + b\,|FN|},

    which weigh false positives by aa and false negatives by bb. One might hope that some choice of weights removes the incentive to duplicate matched predictions under all-pairs accumulation. It does not: a duplicate adds one true positive and no error, so the weights never enter the condition, which is the same v>ma,bv > m_{a,b} for every aa and bb. Under one-to-one matching the duplicate is a false positive, and it lowers the score exactly when false positives carry positive weight; with a=0a = 0 it leaves the score unchanged, so 0<a0 < a is the precise hypothesis. The last statement identifies Panoptic Quality as the member a=b=½a = b = ½.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 6 statements. Each proof establishes one of them relative to its assumptions.

    1 dup_iff proven

    2 falsePositive_eq_of_zero_weight proven

    3 falsePositive_lt proven

    4 no_weights_remove_incentive proven

    5 opposite_directions proven

    6 pq_eq_wm_half proven

    Lean source view on GitHub

    1import Lax303562.PanopticQuality
    2
    3/-!
    4---
    5title: The duplication incentive survives every choice of error weights
    6type: theorem
    7---
    8Panoptic Quality is the member `a = b = ½` of the family of metrics
    9
    10ma,b=sn+a ∣FP∣+b ∣FN∣,m_{a,b} = \frac{s}{n + a\,|FP| + b\,|FN|},
    11
    12which weigh false positives by `a` and false negatives by `b`. One might hope
    13that some choice of weights removes the incentive to duplicate matched
    14predictions under all-pairs accumulation. It does not: a duplicate adds one true
    15positive and no error, so the weights never enter the condition, which is the
    16same `v > m_{a,b}` for every `a` and `b`. Under one-to-one matching the duplicate
    17is a false positive, and it lowers the score exactly when false positives carry
    18positive weight; with `a = 0` it leaves the score unchanged, so `0 < a` is the
    19precise hypothesis. The last statement identifies Panoptic Quality as the member
    20`a = b = ½`.
    21-/
    22
    23namespace Lax303562.WeightedFamily
    24
    25open Lax303562.PanopticQuality
    26
    27/-- The weighted denominator: matched pairs count `1`, false positives `a`, false
    28negatives `b`. -/
    29noncomputable def wden (a b : ℝ) (n fp fn : ℕ) : ℝ := (n : ℝ) + a * fp + b * fn
    30
    31/-- The weighted metric: the matched IoU sum over the weighted denominator. -/
    32noncomputable def wm (a b s : ℝ) (n fp fn : ℕ) : ℝ := s / wden a b n fp fn
    33
    34/-- Under all-pairs accumulation a duplicate with IoU `v` raises the weighted
    35metric exactly when `v` exceeds it, for every choice of weights. -/
    36axiom dup_iff (a b s v : ℝ) (n fp fn : ℕ) (hd : 0 < wden a b n fp fn) :
    37 wm a b s n fp fn < wm a b (s + v) (n + 1) fp fn ↔ wm a b s n fp fn < v
    38
    39/-- No choice of weights removes the incentive: for all `a` and `b`, a duplicate
    40better than the current score raises it. -/
    41axiom no_weights_remove_incentive (s v : ℝ) (n fp fn : ℕ) :
    42 ∀ a b : ℝ, 0 < wden a b n fp fn → wm a b s n fp fn < v →
    43 wm a b s n fp fn < wm a b (s + v) (n + 1) fp fn
    44
    45/-- Under one-to-one matching the duplicate is a false positive, which lowers a
    46positive score whenever false positives carry positive weight. -/
    47axiom falsePositive_lt (a b s : ℝ) (n fp fn : ℕ) (ha : 0 < a) (hs : 0 < s)
    48 (hd : 0 < wden a b n fp fn) :
    49 wm a b s n (fp + 1) fn < wm a b s n fp fn
    50
    51/-- With weight `a = 0` on false positives, a false positive leaves the score
    52unchanged: the hypothesis `0 < a` above is exact. -/
    53axiom falsePositive_eq_of_zero_weight (b s : ℝ) (n fp fn : ℕ) :
    54 wm 0 b s n (fp + 1) fn = wm 0 b s n fp fn
    55
    56/-- Both directions at once, for the whole family. -/
    57axiom opposite_directions (a b s v : ℝ) (n fp fn : ℕ)
    58 (ha : 0 < a) (hs : 0 < s) (hd : 0 < wden a b n fp fn)
    59 (hv : wm a b s n fp fn < v) :
    60 wm a b s n fp fn < wm a b (s + v) (n + 1) fp fn ∧
    61 wm a b s n (fp + 1) fn < wm a b s n fp fn
    62
    63/-- Panoptic Quality is the member `a = b = ½` of the family. -/
    64axiom pq_eq_wm_half (s : ℝ) (n fp fn : ℕ) :
    65 pq s n fp fn = wm (1 / 2) (1 / 2) s n fp fn
    66
    67end Lax303562.WeightedFamily
    68
    Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…