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 with the discrete sigma-algebra, where is the narrow state and is the broad region. Let and give each state in mass . Let fix and cycle through the 16 states of in lexicographic order, beginning at . Let be the independent-refresh kernel and put . Start four chains at and use independent transition randomness. On an event of probability , all 124 transitions use . Every chain then misses the narrow state, even though it has target mass . On that event the rank-normalized folded split for each coordinate is .
Facts & Assumptions
Given: The finite state space, probability vector , kernels , four chains started at , and the algorithm Rank-normalized folded split R-hat.
The full Axiom of Choice assumed by the general time-homogeneous chain and rank-score interfaces. The Axiom of Choice
A transition matrix on a countable discrete space has probability rows summing to one. Transition matrices and n-step probabilities
A probability measure is invariant for when for every measurable . Invariant and stationary distribution for a Markov kernel
A probability measure has total mass one. Probability measures and probability spaces
The algorithm returns the maximum of rank-normalized split on the draws and on their absolute deviations from the pooled median. Rank-normalized folded split R-hat
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.
The masses of sum to , so is a probability measure by [F3]. The maps and have probability rows by construction, so their convex mixture is also a transition matrix by [F1]. The kernel fixes the narrow state and permutes sixteen equally weighted broad states, hence . Every row of is , hence ; linearity gives .
By [F5], these are time-homogeneous chains with transition rule . Each has 31 transitions. The independent transition choices all select with probability . On this event each chain completes two cycles through and never visits , despite .
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 and . The pooled medians are for and for ; the folded deviations each have at least two distinct values, so their split sequences are also identical and nonconstant.
With split length and , the split formula gives for the rank-normalized and folded draws of both coordinates. Each statistic is , so [F4] returns . 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
- Aki Vehtari et al., Rank-normalization, folding, and localization, §§1.1 and 5.2 (standard reference, not scraped)
- Art B. Owen, Monte Carlo Theory, Methods and Examples, Chapter 11, §11.11 (standard reference, not scraped)