Alphabeta Math
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.

✓ 4 results · all verified · 3 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.

Property (*) and Comb Outcomes — Examples

1 · Prerequisites

2 · Summary

These examples check the finite configurations and exponent substitutions that the A page uses repeatedly: the basic comb trigger for property (*), the pure blockade width in the third branch, the square-root rescaling in the Rödl step, and the ϵ5d substitution in the final generalized-nice deduction.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-09-05Open item page →

A four-tooth comb with a special vertex realizes the trigger configuration for property (*)

Example

Let G have vertices

v, a1,a2,a3,a4, bi,j (i,j∈[4])

with edges exactly aibi,j and vbi,j for i,j∈[4]. Put

Bi:={bi,1,bi,2,bi,3,bi,4}

for each i.

Facts & Assumptions

Given: The graph and the blocks displayed in the Example.

[L1]

The item Combs in a graph characterizes an (ℓ,w)-comb by the blockade conditions and the adjacency pattern of the teeth.

[L2]

If a finite family F has property (∗) and G is F‾-free, then an (ℓ,w)-comb with ℓ,w≥4 together with a vertex outside the comb that is complete to the blocks and anticomplete to the teeth is the antecedent of the three-outcome implication in Property (*) for a finite graph family.

Verification

technique · direct
1.1givenL1

The four sets B1,B2,B3,B4 are pairwise disjoint and each has 4 vertices, so (B1,B2,B3,B4) is a (4,4)-blockade.

2.1step 1.1L1

Each tooth ai is adjacent to every vertex of Bi and to no vertex of Bj for j≠i, and the teeth a1,a2,a3,a4 are distinct and lie outside the blocks. Hence ((ai,Bi):i∈[4]) is a (4,4)-comb by [L1].

3.1step 2.1L2∎

The vertex v lies outside the comb, is adjacent to every vertex in ⋃i=14Bi, and is nonadjacent to every ai. Since this comb has ℓ=w=4, the pair consisting of the comb and v realizes the geometric trigger configuration occurring in [L2]. No assertion that an unspecified family has property (∗) is being made.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

The third outcome of property (*) gives a pure four-blockade

Example

Assume the trigger hypothesis of property (∗) holds for a comb of length ℓ=4 and width w. If the third outcome of property (∗) occurs, the resulting blockade is pure with width w/ℓ2.

Facts & Assumptions

Given: A special-vertex comb with ℓ=4 and width w.

[L1]

The third branch in Property (*) for a finite graph family gives a pure (ℓ,w/ℓ2)-blockade.

Verification

technique · direct
1.1L1algebra

Applying [L1] with ℓ=4 yields a pure blockade whose width is wℓ2=w16.

2.1step 1.1L1∎

Since [L1] names the blockade pure rather than complete or anticomplete, this branch keeps exactly the distinction used later on the A page: every pair of blocks is pure, but no stronger global uniformity is asserted.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

A numerical square-root rescaling identity

Example

As a standalone numerical illustration, take

c4:=4,d:=232=58c4,ℓ:=256,k:=ℓ=16,

and assume ∣F∣≥∣G∣.

Facts & Assumptions

Given: The numerical choices in the Example.

[A1]

The sample values satisfy the numerical relation d=58c4. They are not asserted to be the existential constants supplied by the source lemma.

Verification

technique · direct arithmetic
1.1A1algebra

Since k=ℓ, one has ℓ29c4=(k2)29c4=k58c4=kd.

2.1step 1.1algebra

Therefore ∣F∣ℓ29c4=∣F∣kd≥∣G∣kd, using the assumption ∣F∣≥∣G∣.

3.1step 2.1∎

This standalone calculation isolates the square-root renormalization: after replacing ℓ by k=ℓ, the width bound takes exactly the target form ∣G∣/kd when the numerical relation d=58c4 holds.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05Open item page →

The epsilon^(5d) substitution in Claim 4.5.1 and Lemma 4.5

Example

Take

ϵ:=14,c4′:=4,d:=232=58c4′,x:=ϵ5d.

Then the four exponent comparisons in the final property-(*) reduction become explicit.

Facts & Assumptions

Given: The displayed values of ϵ, d, c4′, and x.

[A1]

Since ϵ=14<12, the powers of ϵ decrease as their exponents increase.

Verification

technique · direct arithmetic
1.1A1algebra

The defining substitution gives x=ϵ5d=2−10d<2−d. Together with d=58c4′, this verifies the two parameter inequalities required before applying the Rödl-initialized theorem; its separate graph-order hypothesis must also be checked in any application.

1.2A1algebra

For the restricted-set branch, x23c4′ϵd=ϵ115c4′d+d≥ϵ116c4′d, because 115c4′+1≤116c4′ when c4′=4.

1.3A1algebra

For the clique-or-stable-set branch, x31c4′ϵd=ϵ155c4′d+d≥ϵ156c4′d, because 155c4′+1≤156c4′.

2.1step 1.1A1algebra

If k≥x−1, then ϵd=x1/5≥k−1/5, so ϵdkd≥1k2d. This is exactly the comparison used to turn the complete-or-anticomplete blockade branch into the generalized-nice blockade outcome.

3.1step 1.2step 1.3step 2.1∎

These computations are the concrete numerical version of the four exponent transfers behind the local blockade claim and the final proof of generalized niceness.

Sources