Alphabeta Math
Pipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 3 results · all verified · 3 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 3 also cleared it.

SCM, DAGs, adjustment — Examples

1 · Prerequisites

2 · Summary

Finite examples compute a confounded observational association and the backdoor-adjusted target, show how conditioning on a collider creates dependence, verify a front-door formula with overlapping mediator support, and exhibit two Markovian SCMs with the same observed law but different intervention laws. Each conclusion is conditional on the stated SCM and its graph; none treats the model assumptions as empirical facts.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A confounder and a conditioned collider

Example

Consider first a confounding SCM with independent U∼Bernoulli(1/2) and E∼Bernoulli(1/4), observed A=UxorE, and observed Y=U. Its DAG is U→A and U→Y. The only path between A and Y is the backdoor path A←U→Y.

For collider conditioning, let independent B,C∼Bernoulli(1/2), and set D=B∨C. Its DAG is B→D←C.

Facts & Assumptions

Given: The finite-valued recursive models and mutually independent Bernoulli exogenous variables specified above.

[F1]

Mutual independence gives the product joint law for each finite exogenous family. Independent random elements, Independent random elements have product joint law

[F2]

A noncollider conditioned on blocks a path, while conditioning on a collider activates it. Paths, active paths, and d-separation in a finite DAG

[F3]

The causal response is obtained by replacing only the treatment equation. Recursive structural causal models on finite DAGs

Verification

technique · calculate the two finite joint laws and compare their conditional probabilities

Given: [F1]–[F3] and the two models in the Example.

1.1F1F2F3algebra

In the confounding model, P(A=1)=P(U=0,E=1)+P(U=1,E=0)=12⋅14+12⋅34=12. Also P(U=1,A=1)=12⋅34=38 and P(U=1,A=0)=12⋅14=18. Thus P(Y=1∣A=1)=3/4 and P(Y=1∣A=0)=1/4, although under do(A=a) the variable Y=U remains Bernoulli(1/2). The difference between the observational conditionals and the intervention law is caused by the open backdoor path through U; conditioning on U blocks that path and the adjusted mean is ∑u∈{0,1}P(Y=1∣A=a,U=u)P(U=u)=1/2.

2.1F1F2algebra∎

For the collider model, P(B=1,C=1)=1/4=P(B=1)P(C=1) by [F1], so the variables are independent before conditioning. But D=1 on exactly the three equiprobable pairs (1,1),(1,0),(0,1). Hence P(B=1∣D=1)=P(C=1∣D=1)=2/3 while P(B=1,C=1∣D=1)=1/3≠4/9. Conditioning on the collider D therefore creates dependence, exactly as the active-path rule [F2] predicts.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

The same observed law can have different intervention laws

Example

Let U∼Bernoulli(1/2). In SCM 1 set A=U and Y=A; its graph is U→A→Y. In SCM 2 set A=U and Y=U; its graph is U→A and U→Y. Degenerate independent exogenous errors at A and Y complete both Markovian SCMs.

Facts & Assumptions

Given: The two binary SCMs in the Example.

[F1]

Observational equivalence means equality of the induced sampling laws. Parametric statistical models, Observational equivalence

[F2]

An estimand is identifiable only if it is constant over parameter values with the same observed law. Estimands on a statistical model, Identifiability of an estimand

[F3]

Under an intervention only the named structural equation is replaced. Recursive structural causal models on finite DAGs

Verification

technique · compare the finite observational laws and then compute both truncated structural systems

Given: [F1]–[F3] and the two SCMs in the Example.

1.1givenF1algebra

In either model, A=Y=U, so the observed joint law assigns probability 1/2 to (A,Y)=(0,0) and 1/2 to (A,Y)=(1,1), and zero to the other pairs. The parameter values representing the two SCMs are observationally equivalent by [F1].

2.1step 1.1F2F3algebra∎

Under do(A=a) in SCM 1, the equation Y=A remains and gives Y=a with probability one. Under do(A=a) in SCM 2, the equation Y=U remains and U is unchanged, so Y is Bernoulli(1/2). Thus for a=0 the interventional success probabilities are respectively 0 and 1/2; the intervention-law estimand is not constant on the observational-equivalence class in step 1.1. It is therefore not identifiable on the two-model statistical model by [F2].

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A binary SCM where front-door adjustment works

Example

Let U∼Bernoulli(1/2), EA∼Bernoulli(1/4), and EM∼Bernoulli(1/5) be mutually independent. Set A=UxorEA,M=AxorEM,Y=M∨U. The full graph is U→A, U→Y, A→M, M→Y. The only directed A-to-Y path passes through M. The path A←U→Y←M is blocked by its collider Y, so A and M are d-separated by the empty set in GA‾. The path M←A←U→Y is blocked by A when checking the other front-door condition. Both mediator values have positive probability conditional on either treatment value, so the nested conditional laws have the required support.

Facts & Assumptions

Given: The finite SCM and independent Bernoulli laws in the Example.

[F1]
[F2]

The front-door theorem states the observed functional and its graph and support hypotheses. Front-door adjustment identifies an interventional mean

[F3]

Interventions replace only the named structural equation. Recursive structural causal models on finite DAGs

Verification

technique · evaluate the observed front-door functional and the interventional model directly

Given: [F1]–[F3] and the SCM in the Example.

1.1F1F2algebra

Since P(A=1)=1/2, Bayes' rule gives P(U=1∣A=1)=3/4 and P(U=1∣A=0)=1/4. Since EM is independent of (U,A), P(M=1∣A=1)=4/5 and P(M=1∣A=0)=1/5. Thus for each a∈{0,1} both mediator outcomes have positive conditional probability; the nested-law support condition in [F2] holds.

2.1step 1.1F1F2algebra

If M=1, then Y=1. If M=0, then Y=U, so E(Y∣M=0,A=1)=3/4 and E(Y∣M=0,A=0)=1/4. Averaging over the marginal law of A gives ∫E(Y∣M=0,A=a′)PA(da′)=1/2, while the same inner average for M=1 is 1. The front-door formula [F2] therefore gives 45⋅1+15⋅12=910.

3.1F1F3step 1.1step 2.1algebra∎

Under do(A=1), M=1 with probability 4/5 and M=0 with probability 1/5. The exogenous U remains Bernoulli(1/2) and independent of EM, so E(Y∣do(A=1),M=1)=1 and E(Y∣do(A=1),M=0)=1/2. Hence E[Y1]=45⋅1+15⋅12=9/10, agreeing with the observed functional.

Sources