Mechanism.NoisyOr: Noisy-OR Parameterization (V2)

Migrates the parameter struct from the old Core/Causal/BayesNet.lean into the new Mechanism framework. A NoisyOrParams describes a single inhibitory link's parameters: background rate P(C | ¬A) and causal power P(C | A) − P(C | ¬A).

Phase A scope: only the parameter struct + single-parent mechanism constructor. Multi-parent noisy-OR (combining n independent links) is deferred to Phase B+ when consumers need it.

The old BayesNet.WorldState (joint distribution over two binary variables) is NOT migrated here — it's an output distribution, not a mechanism. If consumers need it, a separate Core/Causal/Distribution.lean is the right home.

structure Core.Causal.Mechanism.NoisyOrParams : Type

Noisy-OR parameters for a single inhibitory link. Migrated from Core.Causal.BayesNet.NoisyOR.

• background : ℚ

  Background rate: P(effect | ¬cause).

• power : ℚ

  Causal power: P(effect | cause) − P(effect | ¬cause).

@[implicit_reducible]

instance Core.Causal.Mechanism.instReprNoisyOrParams : Repr NoisyOrParams

Equations

• Core.Causal.Mechanism.instReprNoisyOrParams = { reprPrec := Core.Causal.Mechanism.instReprNoisyOrParams.repr }

def Core.Causal.Mechanism.instReprNoisyOrParams.repr : NoisyOrParams → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Causal.Mechanism.instDecidableEqNoisyOrParams : DecidableEq NoisyOrParams

Equations

• Core.Causal.Mechanism.instDecidableEqNoisyOrParams = Core.Causal.Mechanism.instDecidableEqNoisyOrParams.decEq

def Core.Causal.Mechanism.instDecidableEqNoisyOrParams.decEq (x✝ x✝¹ : NoisyOrParams) : Decidable (x✝ = x✝¹)

Equations

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

def Core.Causal.Mechanism.NoisyOrParams.pEffectGivenCause (n : NoisyOrParams) : ℚ

P(effect | cause).

Equations

• n.pEffectGivenCause = n.background + n.power

def Core.Causal.Mechanism.NoisyOrParams.pEffectGivenNotCause (n : NoisyOrParams) : ℚ

P(effect | ¬cause).

Equations

• n.pEffectGivenNotCause = n.background

def Core.Causal.Mechanism.NoisyOrParams.isValid (n : NoisyOrParams) : Prop

Validity: both conditional probabilities lie in [0, 1].

Equations

• n.isValid = (0 ≤ n.background ∧ n.background ≤ 1 ∧ 0 ≤ n.background + n.power ∧ n.background + n.power ≤ 1)

@[implicit_reducible]

instance Core.Causal.Mechanism.NoisyOrParams.instDecidableIsValid (n : NoisyOrParams) : Decidable n.isValid

Equations

• n.instDecidableIsValid = Core.Causal.Mechanism.NoisyOrParams.instDecidableIsValid._aux_1 n

def Core.Causal.Mechanism.NoisyOrParams.ofDeterministic : NoisyOrParams

Deterministic cause: P(effect|cause) = 1, P(effect|¬cause) = 0.

Equations

• Core.Causal.Mechanism.NoisyOrParams.ofDeterministic = { background := 0, power := 1 }

def Core.Causal.Mechanism.NoisyOrParams.noEffect : NoisyOrParams

No effect: P(effect|cause) = P(effect|¬cause) = 0.

Equations

• Core.Causal.Mechanism.NoisyOrParams.noEffect = { background := 0, power := 0 }

def Core.Causal.Mechanism.NoisyOrParams.alwaysOn : NoisyOrParams

Always-on: P(effect|cause) = P(effect|¬cause) = 1.

Equations

• Core.Causal.Mechanism.NoisyOrParams.alwaysOn = { background := 1, power := 0 }