ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

The flat-bundle foliation from a linear representation

Example

Assume Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $A \in G L (n, R)$ and let $M_{A} = (R \times R^{n}) / Z$ with $k \cdot (t, v) = (t + k, A^{k} v)$ , a suspension of the linear representation $ρ (k) = A^{k}$ over $B = S^{1}$ ; let $F_{A}$ be the suspension foliation of $M_{A}$ . Then:

$M_{A} \to S^{1}$ , $[t, v] \mapsto [t]$ , is a smooth fibre bundle with fibre $R^{n}$ and locally constant transition functions (a flat vector bundle);
if $A v = v$ , then the leaf through $[0, v]$ is a circle and the leaf loop $a (t) = [(t, v)]$ , $t \in [0, 1]$ , has holonomy germ the germ of $A^{- 1}$ at $v$ ; for $A$ diagonal with all eigenvalues different from $1$ , the leaf through the origin is a circle whose holonomy group is generated by the germ of $A^{- 1}$ at $0$ and is nontrivial whenever $A \neq I$ ;
the foliation $F_{A}$ is transverse to the fibres of the bundle projection.

Facts & Assumptions

Given: A matrix $A \in G L (n, R)$ , the quotient $M_{A} = (R \times R^{n}) / Z$ for $k \cdot (t, v) = (t + k, A^{k} v)$ , and the suspension foliation $F_{A}$ of $ρ (k) = A^{k}$ (The suspension foliation of a representation of the fundamental group).

[F1]

In the suspension the leaf through $v$ is $R / K_{v}$ with $K_{v} = {k : A^{k} v = v}$ , $π_{1} (L_{v}) ≅ K_{v}$ , and the holonomy representation is $k \mapsto {germ}_{v} (A^{k})$ , while forward-path holonomy is ${germ}_{v} (A^{- k})$ (Suspension holonomy is the germ of the represented monodromy action).

[F2]

The holonomy group of a leaf is the image of its holonomy representation (The isotropy of the holonomy groupoid is the leaf holonomy group).

[F3]

A smooth fibre bundle is a surjective submersion locally trivialized over a cover of the base, with transition functions between local trivializations that are smooth and compatible on overlaps (Smooth fibre bundles and local trivializations).

[F4]

The circle is the quotient $R / Z$ ; the arc trivializations used below are derived directly from its quotient relation (The circle as $S^{1} = R / Z$ with basepoint $[0]$ ).

Verification

technique · direct

1.1F3F4construct

The bundle structure. Take arcs $U_{i}$ of $R / Z$ which are the images of $I_{1} = (- 1 / 4, 3 / 4)$ and $I_{2} = (1 / 4, 5 / 4)$ . The quotient map restricts injectively on each interval and is open, since the saturation of an open set is the union of its integer translates. Thus each arc has a unique smooth interval representative $t_{i}$ . Define $Φ_{i} : U_{i} \times R^{n} \to M_{A}$ by $Φ_{i} ([t], v) = [t_{i}, v]$ . Every point over $U_{i}$ has exactly one such representative, and local quotient charts of the suspension make $Φ_{i}$ and its inverse smooth. On each overlap component $t_{2} - t_{1}$ is a constant integer (here $0$ or $1$ ), so the change of fibre coordinate is a constant power of $A$ , hence linear and smooth. These trivializations cover $M_{A}$ and make its projection locally the product submersion. Their locally constant linear transitions supply the asserted flat vector bundle.

1.2F1

The leaf through a fixed vector. If $A v = v$ , then $A^{k} v = v$ for every $k$ , so $K_{v} = Z$ and by [F1] the leaf through $[0, v]$ is $R / Z$ , a circle; the leaf loop $a (t) = [(t, v)]$ , $t \in [0, 1]$ , corresponds to the generator of $Z$ , and its holonomy germ is the germ of $A^{- 1}$ at $v$ .

1.3F1F2

The leaf through the origin. Let $A$ be diagonal with all eigenvalues different from $1$ . Then $A^{k} 0 = 0$ for every $k$ , so $K_{0} = Z$ and the leaf through $[0, 0]$ is a circle. By [F1] its holonomy representation is $k \mapsto {germ}_{0} (A^{k})$ , whose image is the cyclic group generated by the germ of $A^{- 1}$ at $0$ ; by [F2] that image is the holonomy group. If $A \neq I$ , then $A^{- 1} \neq I$ ; since $A^{- 1}$ is linear, it cannot agree with the identity on a neighbourhood of $0$ without being the identity, so the germ of $A^{- 1}$ at $0$ is not the identity germ and the holonomy group is nontrivial. If $A = I$ the holonomy is trivial.

2.1F3step 1.2

Transversality to the fibres. The leaves of $F_{A}$ are locally the images of the $R$ -directions $t \mapsto (t, v)$ and the fibres of $M_{A} \to S^{1}$ are locally the images of the $R^{n}$ -directions $v \mapsto (t, v)$ ; these two directions are complementary in $T_{[t, v]} M_{A}$ , of dimensions $1$ and $n$ . Hence $F_{A}$ is transverse to the fibres at every point (Local transversals to a regular foliation).

3.1step 1.1step 1.2step 1.3step 2.1∎

Conclusion. Steps 1.1, 1.2, 1.3 and 2.1 establish claims 1, 2 and 3.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

52 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

Eckhard Meinrenken, Lie Groupoids and Lie Algebroids, lecture notes (University of Toronto MAT1341, Fall 2017) (standard reference, not scraped)
Danny Calegari, Foliations and the Geometry of 3-Manifolds (Oxford Mathematical Monographs) (standard reference, not scraped)