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 Sierpinski gasket computed by hand
Example
Assume the Axiom of Countable Choice. Let and
Then and . No exact critical measure is asserted.
Facts & Assumptions
Given: The objects, conventions, and hypotheses in the statement above.
Under the standing Countable Choice hypothesis, a finite Borel measure with outer mass on positive and small-set diameter bound yields . The mass distribution principle
Finite positive -measure identifies dimension . Hausdorff dimension is the unique critical exponent
Geometric series with ratio have tails . For , , and for the series diverges
Under the standing Countable Choice hypothesis, a half-open interval has Lebesgue measure its length. A box in with parameters is Lebesgue measurable of measure , whichever of its faces are included
Pointwise limits of measurable functions are measurable. Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable
Verification
Every length- word gives a lower-left corner and a containing closed square . There are words, giving distinct grid squares because each coordinate prefix has a unique length- binary code. Their diameters are ; hence their -cost is . The series converge coordinatewise by geometric tails, and these covers at arbitrarily small scales give .
For define , identify these three values with the listed members of , and put . Each coordinate is a limit of Borel step functions, hence Borel measurable. The vector map is Borel since preimages of open rational rectangles are Borel and those rectangles form a countable basis. Define for Borel , with preimages taken in . Disjoint Borel preimages prove countable additivity; thus is a Borel probability.
Every ternary prefix event is a half-open interval of length , hence has probability . Its image lies in the corresponding square. Also , so every Borel superset of has -measure one and ; no measurability claim about an arbitrary image is needed.
For nonempty of diameter with , each coordinate projection lies in an interval of length at most . Such an interval meets at most four closed grid intervals of side , allowing all boundary contacts. Thus meets at most sixteen level- grid squares. Let be the closed coordinate bounding rectangle of ; its coordinate side lengths are at most , so it meets at most sixteen squares. Every with has its own prefix square meeting , so .
For a singleton use its coordinate point rectangle at arbitrarily fine levels; at most four squares contain the point, so its mass is at most . Empty sets have zero mass. The diameter estimate therefore holds also at zero. Apply mass distribution with constant sixteen and outer mass one to obtain . Combined with the finite upper bound, this gives .
Depends on
- The mass distribution principle
- Hausdorff dimension is the unique critical exponent
- For $|r| < 1$, $\sum_{k \ge 0} r^k = 1/(1-r)$, and for $|r| \ge 1$ the series diverges
- A box in $\mathbb{R}^n$ with parameters $a_i\le b_i$ is Lebesgue measurable of measure $\prod_{i<n}(b_i-a_i)$, whichever of its faces are included
- Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
35 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
- Bishop–Peres Example 1.3.4 pp.15–16 (standard reference, not scraped)