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 · 2 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. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Mixed effects and longitudinal models — Examples

1 · Prerequisites

2 · Summary

Examples

A random intercept yields an intraclass correlation when the total variance is positive. Two visits can leave random-slope and residual covariance parameters aliased even with a full-rank fixed design. A finite random-intercept model can also have an outcome-dependent dropout mechanism, showing that the complete-data covariance structure alone does not make dropout MAR.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Random-intercept covariance and intraclass correlation

Example

For a subject j measured at two distinct visits, let Yji=μ+bj+εji, where Ebj=0, Var⁡(bj)=τ2≥0, the residuals have mean zero and variance σ2≥0, the residuals are independent of each other, and bj is independent of the residual vector (εj1,εj2). If τ2+σ2>0, the marginal correlation between the two observations is Corr⁡(Yj1,Yj2)=τ2τ2+σ2. This is the random-intercept intraclass correlation (ICC).

Facts & Assumptions

Given: The two-visit random-intercept special case of Finite-dimensional linear mixed model with explicit longitudinal roles with the moment and independence assumptions in the Example.

[F1]

The mixed-model marginal covariance is ZGZT+R and does not require Gaussianity. Marginal covariance of the linear mixed model.

[F2]

Variance and covariance are centered second moments. Moments, variance, and covariance on a probability space.

[A1]

τ2,σ2≥0 and τ2+σ2>0.

[A2]

For square-integrable real random variables U,W with positive variances, use the convention Corr⁡(U,W):=Cov⁡(U,W)/Var⁡(U)Var⁡(W). Correlation is undefined if either variance is zero.

Verification

Given: The model in the Example.

1.1F1F2A1

For either visit, the random part is bj+εji, so its variance is τ2+σ2 because the two terms are independent and centered. Equivalently, in the marginal-covariance formula use random-intercept design row 1, G=[τ2], and residual diagonal entry σ2.

1.2F1A1

For the two distinct visits, both observations contain the same bj. The covariance formula gives Cov⁡(Yj1,Yj2)=τ2; the residual cross-covariance is zero by the assumed independence.

2.1A2step 1.1step 1.2A1algebra∎

By [A1], both marginal variances are positive. Dividing the covariance from step 1.2 by the square root of the product of the two equal variances from step 1.1 gives τ2/(τ2+σ2) by [A2]. If τ2=0<σ2 the ICC is 0; if σ2=0<τ2 it is 1; if both are zero the correlation is undefined.

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

Two visits can alias random-slope and residual variance components

Statement refuted

It is false that two visits at times 0 and 1, together with a full-rank fixed design, always identify the random-intercept/random-slope covariance matrix and the residual variance in a Gaussian longitudinal mixed model.

Facts & Assumptions

Given: One subject has observations at t=0,1, with fixed and random design X=Z=(1011), and the Gaussian branch of Finite-dimensional linear mixed model with explicit longitudinal roles.

[F1]

The marginal covariance is ZGZT+R. Marginal covariance of the linear mixed model.

[F2]

In the Gaussian model, covariance-parameter identifiability is equivalent to injectivity of θ↦V(θ). Gaussian variance-component identifiability is covariance-map injectivity.

[F3]

Under AC, the Gaussian branch gives jointly normal latent and residual vectors; scalar normal characteristic functions, the affine transformation rule, and uniqueness of characteristic functions identify the resulting multivariate-normal response law from its mean and covariance. Gaussian branch of the linear mixed model, Multivariate normal law, including singular covariance, Characteristic function of a normal law, Characteristic functions under affine maps and independent sums, Characteristic function of a multivariate normal law, Uniqueness of a law from its characteristic function.

[F4]

A real square matrix is invertible exactly when its determinant is nonzero. A finite square real matrix is invertible if and only if its determinant is nonzero.

[A1]

Construction

Set R1=I2 and G1=I2. For a second parameter tuple set G2=(4/51/51/53/5),R2=65I2. Use the same fixed parameter β for both models.

Verification

Given: The parameter tuples and design in the Counterexample.

1.1F4givenalgebra

The matrix G2 is positive definite because for every (x,y)≠(0,0), (xy)G2(xy)=45(x+14y)2+1120y2>0. Also G1=I2 and R1=I2 are positive definite, while R2=(6/5)I2 is positive definite since 6/5>0. The design has determinant 1, so [F4] makes it invertible and therefore full rank.

1.2F1givenalgebra

For the first tuple, V1=ZG1ZT+R1=(1112)+I2=(2113).

2.1F1givenstep 1.1algebra

Direct multiplication gives ZG2ZT=(4/5119/5),V2=ZG2ZT+R2=(2113)=V1. The covariance parameter tuples are distinct, so the covariance map is not injective.

3.1A1F2F3givenstep 2.1∎

Under either Gaussian tuple, Y−Xβ has every scalar projection normal: in direction u, the coefficient vector on (b,ε) is (ZTu,u) and its variance is uTViu. Since V1=V2, these projections have identical characteristic functions, so [F3] gives equal response laws. The covariance-component tuples are distinct, so the parameter is not identifiable.

Remarks

The witness keeps G2 and both residual covariance matrices positive definite. It shows an exact covariance alias at two visits; more replication of the same two-visit design preserves the same alias.

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

A mixed-model covariance does not imply MAR dropout

Statement refuted

It is false that a correct random-intercept covariance model for a complete two-visit response vector implies dropout after the first visit is missing at random (MAR).

Facts & Assumptions

Given: A finite probability space with independent signs b,ε1,ε2∈{−1,1}, each taking its two values with probability 1/2.

[F1]

The finite-dimensional mixed model requires finite second moments, zero means, and the stated covariance and independence conditions; it imposes no Gaussianity. Finite-dimensional linear mixed model with explicit longitudinal roles.

[F2]

The marginal covariance is ZGZT+R. Marginal covariance of the linear mixed model.

[F3]

MAR requires the observation-pattern probability to depend on the full response only through the coordinates observed under that pattern. Longitudinal observation patterns and missingness mechanisms.

[F4]

A deterministic observation mechanism is a measurable map from the full state to the recorded observation; a stochastic mechanism is a probability kernel with measurable event probabilities. Scientific statistical model contracts.

[A1]

There is one subject, two scheduled visits, no observed covariates (equivalently, the covariate space is a singleton), X=02×1, Z=(1,1)T, b has variance 1, and ε=(ε1,ε2)T has covariance I2.

Construction

Let μ=0 and set Y1=b+ε1,Y2=b+ε2. Observe Y1 for every subject. Let M2=1 mean the second visit is observed, and specify the observation mechanism M2=1{Y2=2}.

Verification

Given: The finite model and observation mechanism in the Counterexample.

1.1F1F2A1

The signs are centered, square-integrable, and independent; b is independent of ε. Thus this is a moment-only random-intercept mixed model with G=[1] and R=I2. By [F2], its complete-response covariance is Cov⁡(Y1Y2)=(1111)+I2=(2112).

1.2F4givenalgebra

Let the pattern space be R={0,1}2 with its power-set σ-algebra, and define the full observation-pattern map O(y1,y2)=(1,1{y2=2}). It is Borel measurable because its first coordinate is constant and its second is the indicator of a Borel set. The induced kernel K(y,A)=1{O(y)∈A} is the point mass at O(y) for each y; for every A⊆R, y↦K(y,A) is measurable as the indicator of the Borel set O−1(A). Thus [F4] applies. Each sign triple has probability 1/8. The two supported states (1,−1,−1) and (1,−1,1) both give observed first-visit value Y1=0, but their second-visit values are Y2=0 and Y2=2, respectively; their patterns are (1,0) and (1,1).

2.1F3step 1.1step 1.2∎

For the missing-visit pattern r=(1,0), the mechanism probability is 1 at (Y1,Y2)=(0,0) and 0 at (0,2). These supported full-data points have the same observed coordinates Yobs(r)=Y1=0, so this pattern probability cannot depend only on the observed data for r. By [F3], the mechanism is not MAR, despite the correct random-intercept covariance in step 1.1.

Remarks

The example declares the full response law and the dropout kernel separately, as required by Scientific statistical model contracts. The covariance identity constrains only the response law.

Sources