Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-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.

A mass-stiffness pencil has real B-orthogonal modes and a residual enclosure

Example

Let the stiffness and mass matrices be K=(4−2−23),M=(2001). The generalized eigenvalues are 1 and 4, with M-orthogonal modes. The trial pair (x,μ)=(e1,2) also illustrates a B-metric residual enclosure.

Facts & Assumptions

Given: The displayed real symmetric stiffness and mass matrices.

[F1]

A Hermitian-definite pencil has a real spectrum and a B-orthonormal eigenbasis: a symmetric K and positive-definite M have real generalized eigenvalues and an M-orthonormal eigenbasis.

[F2]

A B-dual residual bounds distance to the spectrum of a Hermitian-definite pencil: a nonzero trial vector and real trial value have spectral distance bounded by the M-dual residual norm divided by the M-norm of the vector.

[F3]

Regular matrix pencils and homogeneous generalized eigenvalues: the pencil is regular when its determinant polynomial is nonzero.

Verification

1.1givenF3algebra

The matrix M is positive definite because uTMu=2u12+u22>0 for u≠0. Also uTKu=2u12+2(u1−u2)2+u22>0 for u≠0. The determinant polynomial is det⁡(K−λM)=(4−2λ)(3−λ)−4=2(λ−1)(λ−4), so the pencil is regular and its eigenvalues are 1,4.

2.1step 1.1F1algebra

For x1=(1,1)T, Kx1=(2,1)T=Mx1. For x2=(1,−2)T, Kx2=(8,−8)T=4Mx2. Their mass inner product is x1TMx2=2−2=0. Thus they are distinct generalized eigenmodes and are M-orthogonal; [F1] gives the general real-spectrum and orthogonal-basis conclusion for this pencil.

3.1F2step 1.1algebra∎

For x=e1 and μ=2, the residual is r=Kx−μMx=(0,−2)T. Hence ∥x∥M=2 and, since M−1=diag⁡(1/2,1), ∥r∥M−1=2. The theorem [F2] therefore bounds the distance from 2 to {1,4} by 2/2=2; indeed that distance is 1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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