ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)

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.

Checkerboard permeability and the explicit contrast factor

Statement

Assume Countable Choice.

On a $2 \times 2$ checkerboard of equal squares, split each square into two affine triangles and set scalar permeability $K = 1$ on one color and $K = 10^{6}$ on the other. Then $κ_{\min} = 1$ , $κ_{\max} = 10^{6}$ , the weighted energy assigns coefficients $1$ and $10^{- 6}$ to the two regions, and the RT0/P0 graph-norm error constants include $α_{*}^{- 1} = 10^{6}$ and $M_{a} / α_{*} = 10^{6}$ .

Facts & Assumptions

Given: The checkerboard mesh and piecewise-constant scalar permeability just defined.

[A1]

Countable Choice is inherited through the mixed error theorem. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F1]

The weighted flux energy is $∥ v ∥_{K^{- 1}}^{2} = \int_{D} K^{- 1} ∣ v ∣^{2}$ and the coefficient bounds determine $M_{a} = κ_{\min}^{}$ and $α_{*} = κ_{\max}^{}$ . (No-flow mixed Darcy problem and coefficient norms, RT0/P0 Darcy stability and flux/pressure error bound)

[F2]

The stable RT0/P0 inf-sup factor depends on the mesh/domain lift constant $C_{R}$ , while the explicit error formula also contains $α_{*}^{- 1}$ and $M_{a}$ . (RT0/P0 Darcy stability and flux/pressure error bound)

Proof

1.1givenF1algebra

The two positive scalar values are $1$ and $10^{6}$ , so their minimum and maximum are exactly $κ_{\min} = 1$ and $κ_{\max} = 10^{6}$ . Their reciprocals in $K^{- 1}$ are $1$ and $10^{- 6}$ ; substituting into the energy definition gives $∥ v ∥_{K^{- 1}}^{2} = \int_{D_{1}} ∣ v ∣^{2} + 10^{- 6} \int_{D_{10^{6}}} ∣ v ∣^{2}$ .

2.1A1F1F2step 1.1algebra∎

The error theorem constants are $M_{a} = 1$ , $α_{*} = 10^{- 6}$ , so $α_{*}^{- 1} = 10^{6}$ and $M_{a} / α_{*} = 10^{6}$ . The inf-sup lower bound $\hat{β} = (1 + C_{R}^{2})^{- 1 / 2}$ has no permeability parameter because the divergence lift is geometric; this example therefore records an explicit contrast dependence and supplies no contrast-independent error claim.

Checkerboard mesh

The four unit squares are coefficient regions, each split into two triangles along the drawn diagonal. Blue squares have permeability $1$ , orange squares have permeability $10^{6}$ ; each label applies to both triangles in that square. The figure shows the alternating arrangement only; the proof substitutes the exact values into the constants.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jean-Luc Guermond, MATH 661 Fall 2025, Part XI Chapter 49: Well-posedness for PDEs in mixed form (standard reference, not scraped)
Daniele Boffi, Franco Brezzi and Michel Fortin, Mixed Finite Element Methods and Applications (standard reference, not scraped)