Konuk, Quillien and Mascarenhas (2026): Plural Causes

Konuk, Quillien and Mascarenhas extend the Necessity–Sufficiency Model of Icard, Kominsky and Knobe from single causes to plural ones, conjunctions of events judged as causes in their own right. Counterfactual worlds are sampled urn by urn, each urn keeping its actual draw with probability s, the stability, and otherwise redrawn from its prior; a cause's score weights its sufficiency by its probability and its necessity by the probability of its absence, the substrate's CausalStrength.score over plural causes.

Experiment 1 is a game won with two colored balls out of three urns, Experiment 2 one won with (A ∧ B) ∨ (C ∧ D). Losses in Experiment 2 are scored against the classical negation of the rule or its homogeneous negation, after the homogeneity of plural predication described by Križ and Spector, on which each winning condition's plural predication is false.

Main statements

• score_twoOrMore_pair: in a two-of-three threshold game a pair scores the probability that its urns agree; intermediate_high_ranked_highest and low_high_outscores_low_intermediate_iff give the pair rankings of Experiment 1 as functions of the stability.
• mem_win_iff_barePlural, mem_homogeneousLoss_iff_barePlural, not_mem_homogeneousLoss_iff_indet: a win is the truth of some condition's plural predication, the homogeneous loss the falsity of each, and the two losses differ where a predication falls in the homogeneity gap.
• same_condition_pair_not_necessary, crossing_pair_necessary, partners_scored_alike, pair_scores_one, idle_urn_not_necessary, triple_positive_abnormal_inflation: the winning rounds of Experiment 2.
• classical_abnormal_deflation, homogeneous_abnormal_inflation, homogeneous_lt_iff, homogeneous_lt_of_ssubset, classical_triple_negative, homogeneousLoss_tripleNegative: the losing rounds.

Implementation notes

• Necessity holds the urns outside the plural at their actual draws, as in the worked example of p. 448, and the score weights by the plural's sampling probability, its prior at s = 0.
• homogeneousLoss negates each winning condition over its urns that are white in the actual round, which gives both of the paper's homogeneous losses, (2) and that of p. 468.
• Two of the paper's claims about the NSM fail in the model: intermediate_high_ranked_highest needs 0 < s, and partners_scored_alike contradicts the abnormal deflation of p. 463.

TODO

• The Counterfactual Effect Size Model of Quillien and Lucas, which p. 451 says ranks the intermediate and high pair highest at every stability.
• The w-weighted mixture of the two losses, a coin drawn in each counterfactual world (p. 465).

References

• [KQM26]
• [IKK17]
• [QL24]
• [KS21b]

Counterfactual sampling

noncomputable def KonukEtAl2026.propensity (s p : ↑unitInterval) (x : Bool) : MeasureTheory.Measure Bool

The propensity of an urn keeps its actual draw x with probability s, the stability, and otherwise redraws it from the prior p.

Equations

• KonukEtAl2026.propensity s p x = unitInterval.toNNReal s • MeasureTheory.Measure.dirac x + unitInterval.toNNReal (unitInterval.symm s) • ProbabilityTheory.bernoulliMeasure true false p

instance KonukEtAl2026.instIsProbabilityMeasureBoolPropensity (s p : ↑unitInterval) (x : Bool) : MeasureTheory.IsProbabilityMeasure (propensity s p x)

theorem KonukEtAl2026.propensity_real_singleton (s p : ↑unitInterval) (x y : Bool) : (propensity s p x).real {y} = (↑s * if x = y then 1 else 0) + (1 - ↑s) * if y = true then ↑p else 1 - ↑p

theorem KonukEtAl2026.propensity_singleton_ne_zero {s p : ↑unitInterval} (hs : s < 1) (hp₀ : 0 < p) (hp₁ : p < 1) (x y : Bool) : (propensity s p x) {y} ≠ 0

noncomputable def KonukEtAl2026.sampling {ι : Type u_1} [Fintype ι] (s : ↑unitInterval) (p : ι → ↑unitInterval) (w₀ : ι → Bool) : MeasureTheory.Measure (ι → Bool)

The counterfactual distribution samples the urns independently, each by its propensity.

Equations

• KonukEtAl2026.sampling s p w₀ = MeasureTheory.Measure.pi fun (i : ι) => KonukEtAl2026.propensity s (p i) (w₀ i)

instance KonukEtAl2026.instIsProbabilityMeasureForallBoolSampling {ι : Type u_1} [Fintype ι] (s : ↑unitInterval) (p : ι → ↑unitInterval) (w₀ : ι → Bool) : MeasureTheory.IsProbabilityMeasure (sampling s p w₀)

noncomputable def KonukEtAl2026.causalStrength {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : ↑unitInterval) (p : ι → ↑unitInterval) (w₀ : ι → Bool) (E : Set (ι → Bool)) (S : Finset ι) : ENNReal

The actual causal strength of the plural S for the outcome E in the round w₀ is its score with the counterfactuals sampled at stability s from the priors p.

Equations

• KonukEtAl2026.causalStrength s p w₀ E S = CausalStrength.score (KonukEtAl2026.sampling s p w₀) w₀ E S

theorem KonukEtAl2026.causalStrength_ne_top {ι : Type u_1} [Fintype ι] {s : ↑unitInterval} {p : ι → ↑unitInterval} {w₀ : ι → Bool} {S : Finset ι} {E : Set (ι → Bool)} [DecidableEq ι] : causalStrength s p w₀ E S ≠ ⊤

theorem KonukEtAl2026.sampling_ne_zero {ι : Type u_1} [Fintype ι] {s : ↑unitInterval} {p : ι → ↑unitInterval} {w₀ : ι → Bool} (hs : s < 1) (hp₀ : ∀ (i : ι), 0 < p i) (hp₁ : ∀ (i : ι), p i < 1) {A : Set (ι → Bool)} (hA : A.Nonempty) : (sampling s p w₀) A ≠ 0

With stability below one and priors strictly between zero and one, every nonempty event has positive probability.

theorem KonukEtAl2026.sampling_cause_lt_one {ι : Type u_1} [Fintype ι] {s : ↑unitInterval} {p : ι → ↑unitInterval} {w₀ v : ι → Bool} {S : Finset ι} [DecidableEq ι] (hs : s < 1) (hp₀ : ∀ (i : ι), 0 < p i) (hp₁ : ∀ (i : ι), p i < 1) (hS : S.Nonempty) : (sampling s p w₀) (CausalStrength.cause v S) < 1

With stability below one and priors strictly between zero and one, a nonempty plural cause may fail.

theorem KonukEtAl2026.sampling_compl_cause_ne_zero {ι : Type u_1} [Fintype ι] {s : ↑unitInterval} {p : ι → ↑unitInterval} {w₀ v : ι → Bool} {S : Finset ι} [DecidableEq ι] (hs : s < 1) (hp₀ : ∀ (i : ι), 0 < p i) (hp₁ : ∀ (i : ι), p i < 1) (hS : S.Nonempty) : (sampling s p w₀) (CausalStrength.cause v S)ᶜ ≠ 0

theorem KonukEtAl2026.causalStrength_cause_lt_of_ssubset {ι : Type u_1} [Fintype ι] {s : ↑unitInterval} {p : ι → ↑unitInterval} {w₀ : ι → Bool} {S T : Finset ι} [DecidableEq ι] (hs : s < 1) (hp₀ : ∀ (i : ι), 0 < p i) (hp₁ : ∀ (i : ι), p i < 1) {S' : Finset ι} (hS : S.Nonempty) (h : S ⊂ S') (hS' : S' ⊆ T) : causalStrength s p w₀ (CausalStrength.cause w₀ T) S < causalStrength s p w₀ (CausalStrength.cause w₀ T) S'

With stability below one and priors strictly between zero and one, when the outcome is that the urns T all show their actual draws, a larger part of T scores higher.

The running example and Experiment 1: threshold games

def KonukEtAl2026.twoOrMore {ι : Type u_1} [Fintype ι] : Set (ι → Bool)

The outcome of a threshold game occurs when two causes or more are present, A + B + C ≥ 2 (p. 450).

Equations

• KonukEtAl2026.twoOrMore = {w : ι → Bool | 2 ≤ {i : ι | w i = true}.card}

theorem KonukEtAl2026.piecewise_mem_twoOrMore_iff {ι : Type u_1} [DecidableEq ι] {X Y : ι} [Fintype ι] (h3 : Fintype.card ι = 3) (hXY : X ≠ Y) (w : ι → Bool) : ({X, Y}.piecewise w fun (x : ι) => true) ∈ twoOrMore ↔ w X = true ∨ w Y = true

With three causes, all present in the actual round, removing two of them leaves the outcome exactly when one of the two stays present.

theorem KonukEtAl2026.setOf_eq_eq_cause_union {ι : Type u_1} [DecidableEq ι] {X Y : ι} : {w : ι → Bool | w X = w Y} = CausalStrength.cause (fun (x : ι) => true) {X, Y} ∪ CausalStrength.cause (fun (x : ι) => false) {X, Y}

Two urns agree when both show a colored ball or both a white one.

theorem KonukEtAl2026.score_twoOrMore_pair {ι : Type u_1} [DecidableEq ι] {X Y : ι} [Fintype ι] {ν : ι → MeasureTheory.Measure Bool} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)] (h3 : Fintype.card ι = 3) (hXY : X ≠ Y) (hc : (MeasureTheory.Measure.pi ν) ((CausalStrength.cause (fun (x : ι) => true) {X, Y})ᶜ ∩ twoOrMoreᶜ) ≠ 0) : CausalStrength.score (MeasureTheory.Measure.pi ν) (fun (x : ι) => true) twoOrMore {X, Y} = (MeasureTheory.Measure.pi ν) {w : ι → Bool | w X = w Y}

In a two-of-three threshold game won with all three causes, a pair scores the probability that its two causes agree, since it is fully sufficient and is necessary where both its causes are absent.

theorem KonukEtAl2026.causalStrength_twoOrMore_pair_toReal {ι : Type u_1} [DecidableEq ι] {X Y : ι} [Fintype ι] (h3 : Fintype.card ι = 3) (hXY : X ≠ Y) {s : ↑unitInterval} (hs : s < 1) {p : ι → ↑unitInterval} (hp₀ : ∀ (i : ι), 0 < p i) (hp₁ : ∀ (i : ι), p i < 1) : (causalStrength s p (fun (x : ι) => true) twoOrMore {X, Y}).toReal = (↑s + (1 - ↑s) * ↑(p X)) * (↑s + (1 - ↑s) * ↑(p Y)) + (1 - ↑s) * (1 - ↑(p X)) * ((1 - ↑s) * (1 - ↑(p Y)))

The probability that two urns agree under the paper's sampling, the round all colored.

inductive KonukEtAl2026.Dish : Type

Dish lists the dishes of the running example of p. 448.

• cheese : Dish
• cake : Dish
• pie : Dish

@[instance_reducible]

instance KonukEtAl2026.instDecidableEqDish : DecidableEq Dish

Equations

• KonukEtAl2026.instDecidableEqDish x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance KonukEtAl2026.instFintypeDish : Fintype Dish

Equations

• KonukEtAl2026.instFintypeDish = { elems := { val := ↑KonukEtAl2026.Dish.enumList, nodup := KonukEtAl2026.Dish.enumList_nodup }, complete := KonukEtAl2026.instFintypeDish._proof_1 }

noncomputable def KonukEtAl2026.dishPrior : Dish → ↑unitInterval

dishPrior gives the probability of eating each dish (p. 448).

Equations

• KonukEtAl2026.dishPrior KonukEtAl2026.Dish.cheese = ⟨1 / 2, KonukEtAl2026.dishPrior._proof_2⟩
• KonukEtAl2026.dishPrior KonukEtAl2026.Dish.cake = ⟨4 / 5, KonukEtAl2026.dishPrior._proof_11⟩
• KonukEtAl2026.dishPrior KonukEtAl2026.Dish.pie = ⟨1 / 10, KonukEtAl2026.dishPrior._proof_13⟩

inductive KonukEtAl2026.Urn₁ : Type

Urn₁ names the urns of Experiment 1 by their probability of a colored ball.

• low : Urn₁
• intermediate : Urn₁
• high : Urn₁

@[instance_reducible]

instance KonukEtAl2026.instDecidableEqUrn₁ : DecidableEq Urn₁

Equations

• KonukEtAl2026.instDecidableEqUrn₁ x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance KonukEtAl2026.instFintypeUrn₁ : Fintype Urn₁

Equations

• KonukEtAl2026.instFintypeUrn₁ = { elems := { val := ↑KonukEtAl2026.Urn₁.enumList, nodup := KonukEtAl2026.Urn₁.enumList_nodup }, complete := KonukEtAl2026.instFintypeUrn₁._proof_1 }

noncomputable def KonukEtAl2026.prior₁ : Urn₁ → ↑unitInterval

prior₁ gives each urn's probability of a colored ball in Experiment 1.

Equations

• KonukEtAl2026.prior₁ KonukEtAl2026.Urn₁.low = ⟨1 / 20, KonukEtAl2026.prior₁._proof_2⟩
• KonukEtAl2026.prior₁ KonukEtAl2026.Urn₁.intermediate = ⟨1 / 2, KonukEtAl2026.dishPrior._proof_2⟩
• KonukEtAl2026.prior₁ KonukEtAl2026.Urn₁.high = ⟨19 / 20, KonukEtAl2026.prior₁._proof_8⟩

theorem KonukEtAl2026.intermediate_high_ranked_highest {s : ↑unitInterval} (hs : s < 1) : (causalStrength s prior₁ (fun (x : Urn₁) => true) twoOrMore {Urn₁.low, Urn₁.intermediate} < causalStrength s prior₁ (fun (x : Urn₁) => true) twoOrMore {Urn₁.intermediate, Urn₁.high} ↔ 0 < s) ∧ causalStrength s prior₁ (fun (x : Urn₁) => true) twoOrMore {Urn₁.low, Urn₁.high} < causalStrength s prior₁ (fun (x : Urn₁) => true) twoOrMore {Urn₁.intermediate, Urn₁.high}

The holistic NSM rates the intermediate and high pair highest (p. 451), above the low and high pair at every stability below one, and above the low and intermediate pair, by 9/10 · s(1 - s), exactly when the counterfactuals are anchored to the actual round.

theorem KonukEtAl2026.low_high_outscores_low_intermediate_iff {s : ↑unitInterval} (hs : s < 1) : causalStrength s prior₁ (fun (x : Urn₁) => true) twoOrMore {Urn₁.low, Urn₁.intermediate} < causalStrength s prior₁ (fun (x : Urn₁) => true) twoOrMore {Urn₁.low, Urn₁.high} ↔ 9 / 19 < ↑s

The NSM rates the low and high pair above the low and intermediate pair, the prediction from which the participants deviated (p. 453), only for stabilities above 9/19.

Wins and losses under a disjunctive rule

def KonukEtAl2026.win {ι : Type u_1} (rule : Finset (Finset ι)) : Set (ι → Bool)

A rule lists sufficient conditions for a win, each a set of urns; the player wins when every urn of some condition gives a colored ball.

Equations

• KonukEtAl2026.win rule = {w : ι → Bool | ∃ D ∈ rule, ∀ i ∈ D, w i = true}

def KonukEtAl2026.homogeneousLoss {ι : Type u_1} (rule : Finset (Finset ι)) (w₀ : ι → Bool) : Set (ι → Bool)

The homogeneous loss in the losing round w₀ negates each winning condition as a plural over its urns that are white in w₀, so that none of them gives a colored ball.

Equations

• KonukEtAl2026.homogeneousLoss rule w₀ = {w : ι → Bool | ∀ D ∈ rule, ∀ i ∈ D, w₀ i = false → w i = false}

@[instance_reducible]

instance KonukEtAl2026.instDecidablePredForallBoolMemSetWinOfDecidableEq {ι : Type u_1} (rule : Finset (Finset ι)) [DecidableEq ι] : DecidablePred fun (x : ι → Bool) => x ∈ win rule

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance KonukEtAl2026.instDecidablePredForallBoolMemSetHomogeneousLossOfDecidableEq {ι : Type u_1} (rule : Finset (Finset ι)) [DecidableEq ι] (w₀ : ι → Bool) : DecidablePred fun (x : ι → Bool) => x ∈ homogeneousLoss rule w₀

Equations

• One or more equations did not get rendered due to their size.

theorem KonukEtAl2026.mem_win_iff_barePlural {ι : Type u_1} {rule : Finset (Finset ι)} {w : ι → Bool} : w ∈ win rule ↔ ∃ D ∈ rule, Homogeneity.barePlural (fun (i : ι) (w : ι → Bool) => w i = true) D w = 1

A win is the truth of some condition's plural predication, "the urns of the condition gave colored balls".

theorem KonukEtAl2026.mem_homogeneousLoss_iff_barePlural {ι : Type u_1} {rule : Finset (Finset ι)} {w w₀ : ι → Bool} (h : w₀ ∉ win rule) : w ∈ homogeneousLoss rule w₀ ↔ ∀ D ∈ rule, Homogeneity.barePlural (fun (i : ι) (w : ι → Bool) => w i = true) ({x ∈ D | w₀ x = false}) w = -1

In a losing round, the homogeneous loss is the falsity of each condition's plural predication over its urns that are white in the round, the homogeneous negation of the rule (pp. 459, 468).

theorem KonukEtAl2026.not_mem_homogeneousLoss_iff_indet {ι : Type u_1} {rule : Finset (Finset ι)} {w : ι → Bool} (hw : w ∉ win rule) : (w ∉ homogeneousLoss rule fun (x : ι) => false) ↔ ∃ D ∈ rule, Homogeneity.barePlural (fun (i : ι) (w : ι → Bool) => w i = true) D w = 0

A loss falls short of the homogeneous loss of the round where every urn is white exactly when some condition's plural predication falls in the homogeneity gap.

theorem KonukEtAl2026.homogeneousLoss_subset_compl_win {ι : Type u_1} {rule : Finset (Finset ι)} {w₀ : ι → Bool} (h : w₀ ∉ win rule) : homogeneousLoss rule w₀ ⊆ (win rule)ᶜ

In a losing round the homogeneous loss is a loss.

theorem KonukEtAl2026.homogeneousLoss_eq_cause {ι : Type u_1} {rule : Finset (Finset ι)} {w₀ : ι → Bool} [Fintype ι] (hcover : ∀ (i : ι), ∃ D ∈ rule, i ∈ D) : homogeneousLoss rule w₀ = CausalStrength.cause w₀ {x : ι | w₀ x = false}

When every urn appears in some condition, the homogeneous loss of a round is the plural cause of all its white balls.

Single causes under a rule of two conditions

theorem KonukEtAl2026.mem_win_pair_iff {ι : Type u_1} [DecidableEq ι] {rule : Finset (Finset ι)} {X Y : ι} {R : Finset ι} (hrule : rule = {{X, Y}, R}) {w : ι → Bool} : w ∈ win rule ↔ w X = true ∧ w Y = true ∨ w ∈ CausalStrength.cause (fun (x : ι) => true) R

theorem KonukEtAl2026.preimage_update_true_win {ι : Type u_1} [DecidableEq ι] {rule : Finset (Finset ι)} {X Y : ι} {R : Finset ι} (hrule : rule = {{X, Y}, R}) (hXY : X ≠ Y) (hXR : X ∉ R) : (fun (x : ι → Bool) => Function.update x X true) ⁻¹' win rule = CausalStrength.cause (fun (x : ι) => true) {Y} ∪ CausalStrength.cause (fun (x : ι) => true) R

Under the rule X and Y, or all of R, giving X a colored ball wins exactly when Y has one or all of R do.

theorem KonukEtAl2026.preimage_update_false_win {ι : Type u_1} [DecidableEq ι] {rule : Finset (Finset ι)} {X Y : ι} {R : Finset ι} (hrule : rule = {{X, Y}, R}) (hXR : X ∉ R) : (fun (x : ι → Bool) => Function.update x X false) ⁻¹' win rule = CausalStrength.cause (fun (x : ι) => true) R

Under the rule X and Y, or all of R, giving X a white ball wins exactly when all of R give colored balls.

theorem KonukEtAl2026.sufficiency_singleton_win {ι : Type u_1} [DecidableEq ι] {rule : Finset (Finset ι)} {X Y : ι} {R : Finset ι} {w₀ : ι → Bool} [Fintype ι] {ν : ι → MeasureTheory.Measure Bool} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)] (hrule : rule = {{X, Y}, R}) (hXY : X ≠ Y) (hXR : X ∉ R) (hYR : Y ∉ R) (hX : w₀ X = true) (hX' : (ν X) {false} ≠ 0) (hR : (MeasureTheory.Measure.pi ν) (CausalStrength.cause (fun (x : ι) => true) R)ᶜ ≠ 0) : CausalStrength.sufficiency (MeasureTheory.Measure.pi ν) w₀ (win rule) {X} = (ν Y) {true}

Under the rule X and Y, or all of R, the sufficiency of a colored ball from X for the win is the probability that Y gives a colored ball.

theorem KonukEtAl2026.sufficiency_singleton_compl_win {ι : Type u_1} [DecidableEq ι] {rule : Finset (Finset ι)} {X Y : ι} {R : Finset ι} {w₀ : ι → Bool} [Fintype ι] {ν : ι → MeasureTheory.Measure Bool} [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)] (hrule : rule = {{X, Y}, R}) (hXY : X ≠ Y) (hXR : X ∉ R) (hYR : Y ∉ R) (hX : w₀ X = false) (hX' : (ν X) {true} ≠ 0) : CausalStrength.sufficiency (MeasureTheory.Measure.pi ν) w₀ (win rule)ᶜ {X} = (ν Y) {true} * (MeasureTheory.Measure.pi ν) (CausalStrength.cause (fun (x : ι) => true) R)ᶜ / (MeasureTheory.Measure.pi ν) (CausalStrength.cause (fun (x : ι) => true) {Y} ∪ CausalStrength.cause (fun (x : ι) => true) R)

Under the rule X and Y, or all of R, the sufficiency of a white ball from X for the classical loss is the probability that Y gives a colored ball and R not all of them, given that Y does or all of R do.

Experiment 2: the disjunctive rule

inductive KonukEtAl2026.Urn₂ : Type

In Experiment 2 the urns a and b share one color and the urns c and d the other.

• a : Urn₂
• b : Urn₂
• c : Urn₂
• d : Urn₂

@[instance_reducible]

instance KonukEtAl2026.instDecidableEqUrn₂ : DecidableEq Urn₂

Equations

• KonukEtAl2026.instDecidableEqUrn₂ x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance KonukEtAl2026.instFintypeUrn₂ : Fintype Urn₂

Equations

• KonukEtAl2026.instFintypeUrn₂ = { elems := { val := ↑KonukEtAl2026.Urn₂.enumList, nodup := KonukEtAl2026.Urn₂.enumList_nodup }, complete := KonukEtAl2026.instFintypeUrn₂._proof_1 }

def KonukEtAl2026.conditions : Finset (Finset Urn₂)

Under the rule of Experiment 2, (1), the player wins with two balls of one color, from a and b or from c and d.

Equations

• KonukEtAl2026.conditions = {{KonukEtAl2026.Urn₂.a, KonukEtAl2026.Urn₂.b}, {KonukEtAl2026.Urn₂.c, KonukEtAl2026.Urn₂.d}}

noncomputable def KonukEtAl2026.prior₂ : Urn₂ → ↑unitInterval

prior₂ gives each urn's probability of a colored ball in Experiment 2, from its 14, 2, 4 or 19 colored balls out of 20.

Equations

• KonukEtAl2026.prior₂ KonukEtAl2026.Urn₂.a = ⟨7 / 10, KonukEtAl2026.prior₂._proof_2⟩
• KonukEtAl2026.prior₂ KonukEtAl2026.Urn₂.b = ⟨1 / 10, KonukEtAl2026.dishPrior._proof_13⟩
• KonukEtAl2026.prior₂ KonukEtAl2026.Urn₂.c = ⟨1 / 5, KonukEtAl2026.prior₂._proof_9⟩
• KonukEtAl2026.prior₂ KonukEtAl2026.Urn₂.d = ⟨9 / 10, KonukEtAl2026.prior₂._proof_11⟩

theorem KonukEtAl2026.prior₂_pos (i : Urn₂) : 0 < prior₂ i

theorem KonukEtAl2026.prior₂_lt_one (i : Urn₂) : prior₂ i < 1

def KonukEtAl2026.triplePositive : Urn₂ → Bool

triplePositive is the round with colored balls from a, b and d, won through a and b.

Equations

• KonukEtAl2026.triplePositive KonukEtAl2026.Urn₂.c = false
• KonukEtAl2026.triplePositive x✝ = true

def KonukEtAl2026.tripleNegative : Urn₂ → Bool

tripleNegative is the round with a colored ball from c only, lost.

Equations

• KonukEtAl2026.tripleNegative KonukEtAl2026.Urn₂.c = true
• KonukEtAl2026.tripleNegative x✝ = false

def KonukEtAl2026.partner : Urn₂ → Urn₂

partner X is the other urn of X's color.

Equations

• KonukEtAl2026.partner KonukEtAl2026.Urn₂.a = KonukEtAl2026.Urn₂.b
• KonukEtAl2026.partner KonukEtAl2026.Urn₂.b = KonukEtAl2026.Urn₂.a
• KonukEtAl2026.partner KonukEtAl2026.Urn₂.c = KonukEtAl2026.Urn₂.d
• KonukEtAl2026.partner KonukEtAl2026.Urn₂.d = KonukEtAl2026.Urn₂.c

def KonukEtAl2026.otherColor : Urn₂ → Finset Urn₂

otherColor X is the pair of urns of the color X does not have.

Equations

• KonukEtAl2026.otherColor KonukEtAl2026.Urn₂.a = {KonukEtAl2026.Urn₂.c, KonukEtAl2026.Urn₂.d}
• KonukEtAl2026.otherColor KonukEtAl2026.Urn₂.b = {KonukEtAl2026.Urn₂.c, KonukEtAl2026.Urn₂.d}
• KonukEtAl2026.otherColor KonukEtAl2026.Urn₂.c = {KonukEtAl2026.Urn₂.a, KonukEtAl2026.Urn₂.b}
• KonukEtAl2026.otherColor KonukEtAl2026.Urn₂.d = {KonukEtAl2026.Urn₂.a, KonukEtAl2026.Urn₂.b}

theorem KonukEtAl2026.conditions_eq_partner (X : Urn₂) : conditions = {{X, partner X}, otherColor X} ∧ X ≠ partner X ∧ X ∉ otherColor X ∧ partner X ∉ otherColor X

Each urn wins with its partner, or the urns of the other color win, (1).

theorem KonukEtAl2026.causalStrength_singleton_win {s : ↑unitInterval} (hs : s < 1) (X : Urn₂) {w₀ : Urn₂ → Bool} (hX : w₀ X = true) : causalStrength s prior₂ w₀ (win conditions) {X} = (propensity s (prior₂ X) true) {true} * (propensity s (prior₂ (partner X)) (w₀ (partner X))) {true} + if Function.update w₀ X false ∈ win conditions then 0 else (propensity s (prior₂ X) true) {false}

In a round where X gave a colored ball, its score is P(X) times the probability of a colored ball from its partner, plus the probability of its absence when the win depends on it.

The winning rounds

theorem KonukEtAl2026.same_condition_pair_not_necessary (μ : MeasureTheory.Measure (Urn₂ → Bool)) : CausalStrength.necessity μ (fun (x : Urn₂) => true) (win conditions) {Urn₂.a, Urn₂.b} = 0 ∧ CausalStrength.necessity μ (fun (x : Urn₂) => true) (win conditions) {Urn₂.c, Urn₂.d} = 0

In the round where every urn gave a colored ball, neither winning condition is necessary, since the other still holds (p. 462).

theorem KonukEtAl2026.crossing_pair_necessary {s : ↑unitInterval} (hs : s < 1) {X Y : Urn₂} (hX : X ∈ {Urn₂.a, Urn₂.b}) (hY : Y ∈ {Urn₂.c, Urn₂.d}) : 0 < CausalStrength.necessity (sampling s prior₂ fun (x : Urn₂) => true) (fun (x : Urn₂) => true) (win conditions) {X, Y}

In the round where every urn gave a colored ball, a pair across the two conditions is necessary to a positive degree, since without both its balls neither condition holds (p. 462).

theorem KonukEtAl2026.partners_scored_alike {s : ↑unitInterval} (hs : s < 1) : causalStrength s prior₂ (fun (x : Urn₂) => true) (win conditions) {Urn₂.a} = causalStrength s prior₂ (fun (x : Urn₂) => true) (win conditions) {Urn₂.b} ∧ causalStrength s prior₂ (fun (x : Urn₂) => true) (win conditions) {Urn₂.c} = causalStrength s prior₂ (fun (x : Urn₂) => true) (win conditions) {Urn₂.d}

In the round where every urn gave a colored ball, the model scores the two urns of a color alike, against the abnormal deflation the paper reports for it (p. 463).

theorem KonukEtAl2026.pair_scores_one {s : ↑unitInterval} (hs : s < 1) : causalStrength s prior₂ triplePositive (win conditions) {Urn₂.a, Urn₂.b} = 1

In the round won through a and b, with a white ball from c, the pair of a and b is fully sufficient and fully necessary and scores one, at the ceiling where the participants put it (p. 465).

theorem KonukEtAl2026.idle_urn_not_necessary (μ : MeasureTheory.Measure (Urn₂ → Bool)) : CausalStrength.necessity μ triplePositive (win conditions) {Urn₂.d} = 0

In the round won through a and b, the colored ball from d is idle, since removing it never removes the win (p. 464).

theorem KonukEtAl2026.triple_positive_abnormal_inflation {s : ↑unitInterval} (hs : s < 1) : causalStrength s prior₂ triplePositive (win conditions) {Urn₂.a} < causalStrength s prior₂ triplePositive (win conditions) {Urn₂.b}

In the round won through a and b, the rarer colored ball, from b, outscores the commoner one, from a, an abnormal inflation in line with the participants (p. 465).

The losing rounds

theorem KonukEtAl2026.white_ball_redundant (μ : MeasureTheory.Measure (Urn₂ → Bool)) (i : Urn₂) : CausalStrength.necessity μ (fun (x : Urn₂) => false) (win conditions)ᶜ {i} = 0

In the round where every urn gave a white ball, no single white ball is necessary for the classical loss, since the other white ball of its color still blocks its condition (p. 467).

theorem KonukEtAl2026.white_ball_indispensable {s : ↑unitInterval} (hs : s < 1) (i : Urn₂) : CausalStrength.necessity (sampling s prior₂ fun (x : Urn₂) => false) (fun (x : Urn₂) => false) (homogeneousLoss conditions fun (x : Urn₂) => false) {i} = 1

In the round where every urn gave a white ball, every white ball is necessary for the homogeneous loss (p. 467).

theorem KonukEtAl2026.causalStrength_singleton_compl_win_toReal {s : ↑unitInterval} (hs : s < 1) (X : Urn₂) : have q := fun (i : Urn₂) => (propensity s (prior₂ i) false).real {true}; have K := ∏ i ∈ otherColor X, q i; (causalStrength s prior₂ (fun (x : Urn₂) => false) (win conditions)ᶜ {X}).toReal = (1 - q X) * (q (partner X) * (1 - K) / (q (partner X) + K - q (partner X) * K))

In the round where every urn gave a white ball, the score of a white ball from X for the classical loss, with q the probability of a colored ball, Y the partner of X and K the probability that the other color wins.

theorem KonukEtAl2026.classical_abnormal_deflation {s : ↑unitInterval} (hs : s < 1) : causalStrength s prior₂ (fun (x : Urn₂) => false) (win conditions)ᶜ {Urn₂.a} < causalStrength s prior₂ (fun (x : Urn₂) => false) (win conditions)ᶜ {Urn₂.b} ∧ causalStrength s prior₂ (fun (x : Urn₂) => false) (win conditions)ᶜ {Urn₂.d} < causalStrength s prior₂ (fun (x : Urn₂) => false) (win conditions)ᶜ {Urn₂.c}

Under the classical loss, the white ball an urn is likelier to give scores higher, b over a and c over d, an abnormal deflation contrary to the participants (p. 466).

theorem KonukEtAl2026.homogeneousLoss_conditions (w₀ : Urn₂ → Bool) : homogeneousLoss conditions w₀ = CausalStrength.cause w₀ {x : Urn₂ | w₀ x = false}

In every losing round of Experiment 2 the homogeneous loss is the plural cause of the round's white balls.

theorem KonukEtAl2026.homogeneous_lt_iff {s : ↑unitInterval} (hs : s < 1) {w₀ : Urn₂ → Bool} {S S' : Finset Urn₂} (hS : ∀ i ∈ S, w₀ i = false) (hS' : ∀ i ∈ S', w₀ i = false) (hne : S.Nonempty) (hne' : S'.Nonempty) : causalStrength s prior₂ w₀ (homogeneousLoss conditions w₀) S < causalStrength s prior₂ w₀ (homogeneousLoss conditions w₀) S' ↔ ∏ i ∈ S', (propensity s (prior₂ i) false).real {false} < ∏ i ∈ S, (propensity s (prior₂ i) false).real {false}

Under the homogeneous loss, of two pluralities of white balls the less likely scores higher.

theorem KonukEtAl2026.homogeneous_lt_of_ssubset {s : ↑unitInterval} (hs : s < 1) {w₀ : Urn₂ → Bool} {S S' : Finset Urn₂} (hS : S.Nonempty) (h : S ⊂ S') (hS' : ∀ i ∈ S', w₀ i = false) : causalStrength s prior₂ w₀ (homogeneousLoss conditions w₀) S < causalStrength s prior₂ w₀ (homogeneousLoss conditions w₀) S'

Under the homogeneous loss, a plurality of white balls scores higher than any part of it, as the participants rated triples above pairs and pairs above their single balls (pp. 467, 469).

theorem KonukEtAl2026.homogeneous_abnormal_inflation {s : ↑unitInterval} (hs : s < 1) : (causalStrength s prior₂ (fun (x : Urn₂) => false) (homogeneousLoss conditions fun (x : Urn₂) => false) {Urn₂.b} < causalStrength s prior₂ (fun (x : Urn₂) => false) (homogeneousLoss conditions fun (x : Urn₂) => false) {Urn₂.a} ∧ causalStrength s prior₂ (fun (x : Urn₂) => false) (homogeneousLoss conditions fun (x : Urn₂) => false) {Urn₂.c} < causalStrength s prior₂ (fun (x : Urn₂) => false) (homogeneousLoss conditions fun (x : Urn₂) => false) {Urn₂.d}) ∧ causalStrength s prior₂ tripleNegative (homogeneousLoss conditions tripleNegative) {Urn₂.b} < causalStrength s prior₂ tripleNegative (homogeneousLoss conditions tripleNegative) {Urn₂.a} ∧ causalStrength s prior₂ tripleNegative (homogeneousLoss conditions tripleNegative) {Urn₂.b, Urn₂.d} < causalStrength s prior₂ tripleNegative (homogeneousLoss conditions tripleNegative) {Urn₂.a, Urn₂.d}

Under the homogeneous loss, the white balls an urn is less likely to give score higher, a over b and d over c when every urn gave a white ball (p. 466), and a over b, alone and with d, when c gave a colored one (p. 468).

theorem KonukEtAl2026.classical_triple_negative {s : ↑unitInterval} (hs : s < 1) : CausalStrength.necessity (sampling s prior₂ tripleNegative) tripleNegative (win conditions)ᶜ {Urn₂.d} = 1 ∧ CausalStrength.necessity (sampling s prior₂ tripleNegative) tripleNegative (win conditions)ᶜ {Urn₂.a} = 0 ∧ CausalStrength.necessity (sampling s prior₂ tripleNegative) tripleNegative (win conditions)ᶜ {Urn₂.b} = 0

In the round with a colored ball from c only, the white ball from d is indispensable for the classical loss, and those from a and b are redundant with one another (p. 468).

theorem KonukEtAl2026.homogeneousLoss_tripleNegative : homogeneousLoss conditions tripleNegative = {w : Urn₂ → Bool | w Urn₂.a = false ∧ w Urn₂.b = false ∧ w Urn₂.d = false}

The homogeneous loss of the round with a colored ball from c only is ¬A ∧ ¬B ∧ ¬D, the rule negated as homogeneously as the facts allow (p. 468).