Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge 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.

A conforming P1 Dirichlet discretization gives a first Ritz upper bound

Example

Let Ω=(0,1)2 and put z0=(0,0), z1=(1/2,0), z2=(1,0), z3=(1,1/2), z4=(1,1), z5=(1/2,1), z6=(0,1), z7=(0,1/2) in counterclockwise order; these divide each side into two boundary edges. Let c=(1/2,1/2). The eight triangles Kj=conv⁡{c,zj,zj+1}, with indices modulo 8, form a matching affine triangulation. Let ϕ be the continuous piecewise-linear hat with value 1 at c and value 0 at each zj. Its trace vanishes on the boundary. The one-dimensional conforming Ritz space Vh=span⁡{ϕ} has first Ritz value 24; hence the exact Dirichlet ground-state eigenvalue satisfies λ1≤24.

Facts & Assumptions

Given: Countable Choice and the Axiom of Choice; the square, the eight triangles, the hat function ϕ, and the Dirichlet Laplacian forms a(u,v)=∫Ω∇u⋅∇v‾ and b(u,v)=∫Ωuv‾.

[F2]

The exact symmetric Dirichlet spectrum has a nondecreasing eigenvalue list, and its first eigenvalue is the attained minimum of the Rayleigh quotient (the Courant–Fischer theorem assumes both Choice and Countable Choice) (Discrete spectrum of a symmetric elliptic Dirichlet operator, The Courant-Fischer min-max principle for elliptic eigenvalues).

Proof

technique · direct

Given: The conforming mesh, nodal hat ϕ, and the continuous and discrete Dirichlet Rayleigh quotients.

1.1F1givenalgebra

Adjacent triangles share the same endpoint values of ϕ, so their linear traces agree on each interior edge. The boundary edges have zero values at both endpoints, so their linear traces vanish identically. Thus [F1] places ϕ in H01(Ω). It is nonzero because ϕ(c)=1. Each triangle has base length 1/2, height 1/2 and area 1/8; the hat changes from 1 at c to 0 across height 1/2, so ∣∇ϕ∣=2 on each cell. Therefore a(ϕ,ϕ)=8⋅18⋅22=4.

1.2givenalgebra

On a triangle, ϕ is the barycentric coordinate of c. On the reference triangle {(x,y):x>0,y>0,x+y<1}, direct integration gives ∫01∫01−xx2 dy dx=112=16(12). An affine change of variables preserves the ratio of this integral to the triangle area, so ∫Kjϕ2=∣Kj∣/6=1/48. Summing the eight cells gives b(ϕ,ϕ)=1/6.

2.1F1F2step 1.1step 1.2algebra∎

Because Vh is one-dimensional, its sole Ritz value is its Rayleigh quotient, λh,1=a(ϕ,ϕ)/b(ϕ,ϕ)=4/(1/6)=24. By [F2], the continuous first eigenvalue minimizes the same quotient over all nonzero H01 functions. Since ϕ is an admissible nonzero function by step 1.1, λ1≤a(ϕ,ϕ)/b(ϕ,ϕ)=24=λh,1.

Remarks

This exact calculation verifies the fixed-index conforming upper bound for one mesh. It does not check the small best-approximation-gap premise needed for the quadratic error estimate on this particular coarse space.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 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