Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass
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.

Eliminating the middle vertex creates structural fill

Example

Work over Q, which is a field, and take

A=(2−10−12−10−12)

with vertices {0,1,2} and elimination order (1,0,2). The initial structural graph is the path 0−1−2. Eliminating its middle vertex creates the edge {0,2}, and the first Schur complement has a nonzero entry in that position. The pivots in the full order are nonzero, so the ordered elimination is defined throughout.

Facts & Assumptions

Given: The displayed symmetric matrix over Q, the vertex labels, and the elimination order (1,0,2).

[L1]

Structural graphs and ordered symmetric elimination: a pivot's remaining neighbors are joined pairwise when that pivot is eliminated.

[L2]

The rationals form a field: the rational numbers with their standard operations form a field.

[A1]

Use the Schur-update convention S0=A: at stage k, set pk=Svkvkk and, if pk≠0, define Sijk+1=Sijk−SivkkSvkjk/pk for the remaining vertices i,j. Each update is defined after its current pivot has been checked.

[L4]

The filled graph contains every off-diagonal Schur-complement nonzero: for a symmetric matrix over a field and a fixed ordering, if every pivot in the Schur updates is nonzero, every nonzero off-diagonal entry of each Schur complement is an edge of the corresponding filled graph.

Verification

1.1givenA1L1L2algebra

The off-diagonal nonzero entries of A are exactly A01=A10=−1 and A12=A21=−1, so the initial structural graph is the path with edges {0,1} and {1,2}. The first pivot is p0=A11=2≠0, so [A1] defines S1=(3/2−1/2−1/23/2) on the remaining labels (0,2). Now p1=S001=3/2≠0, so the next update is defined and gives S222=3/2−(−1/2)2/(3/2)=4/3. Hence p2=4/3≠0, and its update leaves the empty matrix. Thus all three pivots are nonzero and every stage is defined.

2.1givenL1L2L4step 1.1algebra

The first eliminated vertex is v0=1, whose later-neighbor set is {0,2}. By [L1] its elimination adds the previously absent edge {0,2}; the computed S021=−1/2 is nonzero. Since A is symmetric over the field Q and step 1.1 verifies all pivots, [L4] applies to these Schur complements. After the first elimination only two vertices remain, so later eliminations cannot join a new pair. Thus this ordering creates exactly one fill edge, realized by a numerical nonzero.

3.1step 1.1step 2.1∎

This ordering creates one structural fill edge. The computation gives a finite example only and supplies no general fill bound.

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