Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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 shared missed region in a finite funnel-shaped target

Example

This finite funnel-shaped model has state space E={n}∪B with the discrete sigma-algebra, where n=(0,0) is the narrow state and B={(v,x):v∈{1,2,3,4}, x∈{−2,−1,1,2}} is the broad region. Let π(n)=1/2 and give each state in B mass 1/32. Let K fix n and cycle through the 16 states of B in lexicographic order, beginning at (1,−2). Let Π be the independent-refresh kernel Π(x,{y})=π(y) and put P=.99K+.01Π. Start four chains at (1,−2) and use independent transition randomness. On an event of probability .99124, all 124 transitions use K. Every chain then misses the narrow state, even though it has target mass 1/2. On that event the rank-normalized folded split R^ for each coordinate is 15/16<1.

Facts & Assumptions

Given: The finite state space, probability vector π, kernels K,Π,P, four chains started at (1,−2), and the algorithm Rank-normalized folded split R-hat.

[A1]

The full Axiom of Choice assumed by the general time-homogeneous chain and rank-score interfaces. The Axiom of Choice

[F1]

A transition matrix on a countable discrete space has probability rows p(x,y)=K(x,{y}) summing to one. Transition matrices and n-step probabilities

[F2]

A probability measure π is invariant for K when ∫K(x,A) π(dx)=π(A) for every measurable A. Invariant and stationary distribution for a Markov kernel

[F3]

A probability measure has total mass one. Probability measures and probability spaces

[F4]

The algorithm returns the maximum of rank-normalized split R^ on the draws and on their absolute deviations from the pooled median. Rank-normalized folded split R-hat

[F5]

A time-homogeneous chain has one-step conditional transition law given by its probability kernel relative to the stated filtration. Time-homogeneous Markov chain with transition kernel

Verification

Given: The finite model and event specified in the Example.

1.1givenF1F2F3algebra

The masses of π sum to 1/2+16(1/32)=1, so π is a probability measure by [F3]. The maps K and Π have probability rows by construction, so their convex mixture P is also a transition matrix by [F1]. The kernel K fixes the narrow state and permutes sixteen equally weighted broad states, hence πK=π. Every row of Π is π, hence πΠ=π; linearity gives πP=.99πK+.01πΠ=π.

1.2A1givenF1F5algebra

By [F5], these are time-homogeneous chains with transition rule P. Each has 31 transitions. The independent transition choices all select K with probability .994⋅31. On this event each chain completes two cycles through B and never visits n, despite π({n})=1/2.

1.3A1givenF4algebra

Each original chain has length 32 and traverses the same 16-state cycle twice. Splitting gives eight identical length-16 chains. For either coordinate, the rank-normalized split sequences are identical and nonconstant, so B=0 and W>0. The pooled medians are 2.5 for v and 0 for x; the folded deviations each have at least two distinct values, so their split sequences are also identical and nonconstant.

2.1A1step 1.3F4algebra∎

With split length N=16 and B=0, the split formula gives V^+=(15/16)W for the rank-normalized and folded draws of both coordinates. Each statistic is 15/16, so [F4] returns R^=15/16<1. These values do not reveal the common missed state.

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