Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05
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.

Leaves of a Lie subalgebra distribution

Example

Let G=GL2(R) and let h be the one-dimensional Lie subalgebra spanned by E12=(0100). The left translates Dg:=d(Lg)I(h) form a rank-1 distribution on G. Its leaves are the left cosets of the subgroup H={I+tE12:tR}.

Facts & Assumptions

Given: The subgroup H={I+tE12:tR} of GL2(R).

[L1]

Through each point of an integrable distribution there is a unique maximal connected integral manifold, its leaf (Existence and uniqueness of maximal connected integral manifolds).

[A1]

Left translation sends h to tangent lines of left cosets of H.

Verification

technique · direct
1.1

The map tI+tE12 is a one-parameter subgroup because [given] E122=0, so (I+sE12)(I+tE12)=I+(s+t)E12. Hence H is a connected immersed Lie subgroup with tangent space TIH=h.

givenalgebra
1.2

For any gG, the left coset gH has tangent line [given] d(Lg)I(h) at the point g. Thus each coset is an integral manifold of the distribution D.

given
2.1

For each gG, the curve cg(t)=g(I+tE12) has image gH and [given] derivative cg(t)=gE12=d(Lcg(t))I(E12), so it is an integral curve of the nowhere-zero rank-1 distribution D. Hence any connected integral manifold through g is locally an open piece of that same integral curve and is contained in gH. Since step 1.2 shows that gH itself is a connected integral manifold through g, [L1] identifies gH as the leaf through g. Varying g gives all leaves.

L1step 1.2given

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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