Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablePipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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.

First-return times and induced transformations

Definition

Let (X,A,μ,T) preserve finite measure and let EA satisfy μ(E)>0. For xE define the first-return time

rE(x)=min{n1:TnxE},min=.

A nonempty set of return times has a least element by The well-ordering principle. Define the infinitely returning core

E=EN1nNTnE.

This is the set-limsup convention of Limit superior and limit inferior of a sequence of sets. It is measurable by Sigma-algebras are closed under countable intersections, differences, symmetric differences, and set limits, and Poincare recurrence for finite measure-preserving systems gives μ(EE)=0. Define the induced transformation and normalized measure by

TE:EE,TE(x)=TrE(x)x,μE(B)=μ(B)μ(E),BAE.

Here the trace is as in The trace of a sigma-algebra on a subset. Since E is measurable, the trace equals {BA:BE}: each intersection with E is measurable and each such B equals BE. Its closure under relative complement and countable union follows directly from these same operations in A; no sequence of ambient representatives needs to be chosen. This supplies the measurable-subset instance of The trace of a sigma-algebra is a sigma-algebra on the traced subset locally.

For xE, rE(x) is finite, and the infinitely many visits after rE(x) are exactly positive visits of TE(x), so TE(x)E. Restricting countable additivity of μ and dividing by the positive finite number μ(E) makes μE a measure; its total mass is μ(E)/μ(E)=1. The value is allowed for rE on EE, but is never used as an iterate in TE. No choice axiom enters this construction.

Depends on

Used by

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