Randomization Bridge

Abstract

Randomization identifies conditional outcome laws with potential and do laws.

Definition 1.1 (Treatment event).

Lean statement: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.treatmentEvent

Formalization. D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.treatmentEvent (✓ std3).

Source. Repository-derived.

Commentary.

The event contains exactly the sample points whose factual treatment equals the queried value.

Definition 1.2 (Factual outcome).

Lean statement: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.factualOutcome

Formalization. D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.factualOutcome (✓ std3).

Source. Repository-derived.

Commentary.

The factual outcome evaluates the shared mechanism at the assigned treatment.

Definition 1.3 (Potential outcome).

Lean statement: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.potentialOutcome

Formalization. D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.potentialOutcome (✓ std3).

Source. Repository-derived.

Commentary.

The potential outcome fixes the mechanism’s treatment argument while retaining the sampled exogenous state.

Definition 1.4 (Perfect-intervention outcome).

Lean statement: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.doOutcome

Formalization. D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.doOutcome (✓ std3).

Source. Repository-derived.

Commentary.

A perfect do intervention fixes the same structural treatment argument as the corresponding potential outcome.

Definition 1.5 (Random assignment).

Lean statement: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.RandomAssignment

Formalization. D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.RandomAssignment (✓ std3).

Source. Repository-derived.

Commentary.

Treatment is independent of the complete function-valued potential outcome process, not merely of one selected coordinate.

Definition 1.6 (Treatment positivity).

Lean statement: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.TreatmentPositivity

Formalization. D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.TreatmentPositivity (✓ std3).

Source. Repository-derived.

Commentary.

Positivity requires the queried treatment fiber to have strictly positive measure.

Definition 1.7 (Conditional factual law).

Lean statement: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.conditionalOutcomeLaw

Formalization. D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.conditionalOutcomeLaw (✓ std3).

Source. Repository-derived.

Commentary.

This law pushes the treatment-conditioned sample measure through the factual outcome.

Definition 1.8 (Potential-outcome law).

Lean statement: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.potentialOutcomeLaw

Formalization. D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.potentialOutcomeLaw (✓ std3).

Source. Repository-derived.

Commentary.

This law pushes the ambient sample measure through one fixed potential outcome coordinate.

Definition 1.9 (Perfect-intervention law).

Lean statement: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.doOutcomeLaw

Formalization. D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.doOutcomeLaw (✓ std3).

Source. Repository-derived.

Commentary.

The do law is generated by the perfect-intervention outcome under the same exogenous measure.

Lemma 1.10 (Consistency lifts to conditioned laws).

$co n d i t i o na lO u t co m e L a w (m u, X, Y, x) = ma p (p o t e n t ia lO u t co m e (Y, x), co n d (m u, t re a t m e n tE v e n t (X, x)))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.conditional_factual_law_eq_conditional_potential_law (✓ std3). ∎

Source. Repository-derived.

Commentary.

On the treatment fiber, the imported pointwise consistency theorem identifies factual and matching potential outcomes.

Conditional almost-everywhere equality and pushforward congruence then identify their complete conditioned laws.

Lemma 1.11 (Random assignment removes conditioning).

$(R an d o m A ss i g nm e n t (m u, X, Y) \land T re a t m e n tP os i t i v i t y (m u, X, x)) \Rightarrow ma p (p o t e n t ia lO u t co m e (Y, x), co n d (m u, t re a t m e n tE v e n t (X, x))) = p o t e n t ia lO u t co m e L a w (m u, Y, x)$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.random_assignment_preserves_potential_law (✓ std3). ∎

Source. Repository-derived.

Commentary.

Independence of treatment from the full potential process descends to the selected coordinate by measurable projection.

The intersection factorization cancels the finite positive treatment mass in the definition of the conditional measure.

Lemma 1.12 (Potential law is the do law).

$p o t e n t ia lO u t co m e L a w (m u, Y, x) = d o O u t co m e L a w (m u, Y, x)$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.potential_outcome_law_eq_do_outcome_law (✓ std3). ∎

Source. Repository-derived.

Commentary.

Both laws evaluate the same shared structural mechanism at the imposed treatment and push forward the same exogenous measure.

Theorem 1.13 (Randomization bridge).

$(R an d o m A ss i g nm e n t (m u, X, Y) \land T re a t m e n tP os i t i v i t y (m u, X, x)) \Rightarrow (co n d i t i o na lO u t co m e L a w (m u, X, Y, x) = p o t e n t ia lO u t co m e L a w (m u, Y, x) \land p o t e n t ia lO u t co m e L a w (m u, Y, x) = d o O u t co m e L a w (m u, Y, x))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.randomization_bridge (✓ std3). ∎

Source. Repository-derived.

Commentary.

Consistency first replaces the factual outcome by its matching potential outcome inside the treatment-conditioned law.

Random assignment removes that conditioning, and perfect-intervention semantics supplies the second equality.

Theorem 1.14 (Positive treatment mass is necessary).

$R an d o m A ss i g nm e n t (m u B oo l, co n s tF a l se, co n s tF a l se P rocess) \land ((\neg T re a t m e n tP os i t i v i t y (m u B oo l, co n s tF a l se, t r u e)) \land (\neg co n d i t i o na lO u t co m e L a w (m u B oo l, co n s tF a l se, co n s tF a l se P rocess, t r u e) = p o t e n t ia lO u t co m e L a w (m u B oo l, co n s tF a l se P rocess, t r u e)))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.positive_treatment_probability_is_necessary (✓ std3). ∎

Source. Repository-derived.

Commentary.

Take a fair Boolean sample, constant-false treatment, and a constant-false outcome mechanism, then query treatment true.

The treatment event has zero mass. Mathlib’s conditional measure is therefore zero, while the potential law has total mass one.

Theorem 1.15 (Finite treatment mass is necessary).

$m e a s u re (m u I n f, u ni v) = t o p \land (R an d o m A ss i g nm e n t (m u I n f, co n s t U ni t, co n s t U ni tP rocess) \land (T re a t m e n tP os i t i v i t y (m u I n f, co n s t U ni t, u ni t) \land (\neg co n d i t i o na lO u t co m e L a w (m u I n f, co n s t U ni t, co n s t U ni tP rocess, u ni t) = p o t e n t ia lO u t co m e L a w (m u I n f, co n s t U ni tP rocess, u ni t))))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.finite_measure_is_necessary (✓ std3). ∎

Source. Repository-derived.

Commentary.

Scale the Dirac law on Unit by infinite ENNReal mass, with constant treatment and outcome mechanism.

Random assignment and strict positivity still hold. Conditioning on the infinite-mass fiber is mathlib’s zero measure, while the potential law retains infinite mass.

Theorem 1.16 (Random assignment is necessary).

$T re a t m e n tP os i t i v i t y (m u B oo l, i d, t r u e) \land ((\neg R an d o m A ss i g nm e n t (m u B oo l, i d, co p y P rocess)) \land (\neg co n d i t i o na lO u t co m e L a w (m u B oo l, i d, co p y P rocess, t r u e) = p o t e n t ia lO u t co m e L a w (m u B oo l, co p y P rocess, t r u e)))$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.random_assignment_is_necessary (✓ std3). ∎

Source. Repository-derived.

Commentary.

On a fair Boolean sample, let treatment and every potential outcome equal the sampled bit.

The true-treatment fiber is positive, but its conditional outcome law assigns zero mass to false while the potential law assigns one half. Hence random assignment fails and is indispensable.

References

Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.RandomAssignment
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.TreatmentPositivity
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.conditionalOutcomeLaw
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.conditional_factual_law_eq_conditional_potential_law
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.doOutcome
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.doOutcomeLaw
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.factualOutcome
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.finite_measure_is_necessary
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.positive_treatment_probability_is_necessary
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.potentialOutcome
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.potentialOutcomeLaw
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.potential_outcome_law_eq_do_outcome_law
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.random_assignment_is_necessary
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.random_assignment_preserves_potential_law
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.randomization_bridge
Truth anchor: D5/S3/ConceptDynamics/InterventionsExchange/RandomizationBridge.treatmentEvent
Dependency: D5/S3/ConceptDynamics/InterventionsExchange/FactualInterventionConsistency

Keyboard shortcuts

trureturing Blueprint

Randomization Bridge

Abstract

References