Alphabeta Math
CounterexampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-14
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 same intrinsic planar strip can have different extrinsic curvature after bending

False claim

The induced Riemannian metric of a Euclidean surface determines its second fundamental form, up to transport by intrinsic isometries.

Counterexample

Assume ACω and let r>0. On U=(0,πr)×R, define two embeddings into Euclidean R3 by

F(u,v)=(u,v,0),G(u,v)=(rcos(u/r),rsin(u/r),v).

Both pull back the Euclidean metric to du2+dv2, so GF1 is an intrinsic isometry from a planar strip to an open half-cylinder and both induced metrics are flat. Nevertheless, for the displayed normals,

IIF=0,IIG(u,u)=1rNG0.

Thus the two isometric surfaces have different second fundamental forms, and the false claim fails. The countable-choice assumption is inherited exactly from the general second-fundamental-form construction.

Facts & Assumptions

Given: ACω, r>0, U, the two displayed embeddings, and the standard Euclidean metric.

[F1]

Countable choice permits a choice from every sequence of nonempty sets, and pullback by an immersion gives its induced Riemannian metric. The Axiom of Countable Choice (ACω), Pullback of a riemannian metric is riemannian exactly for immersions.

[F2]

Under ACω, the second fundamental form is the normal component II(X,Y)=(XY). Induced connection and second fundamental form.

[F3]

The metric Christoffel formula and connection Leibniz rule identify Euclidean covariant derivatives with ordinary Cartesian derivatives. Christoffel formula for the levi civita connection, Connection laws in directional form.

[F4]

A Riemannian manifold is flat exactly when it is locally isometric to Euclidean space. A Riemannian manifold is flat iff it is locally isometric to Euclidean space.

Verification

technique · explicit counterexample
1.1

The plane derivatives are Fu=(1,0,0) and Fv=(0,1,0). For θ=u/r, the cylinder derivatives are Gu=(sinθ,cosθ,0) and Gv=(0,0,1). Each pair is orthonormal, so both differentials are injective and [F1] gives FgE=GgE=du2+dv2.

F1givenalgebra
2.1

The interval 0<u<πr makes θ(cosθ,sinθ) injective with positive second coordinate, so F and G identify U diffeomorphically with the planar strip and open upper half-cylinder, respectively. Step 1.1 then shows directly that GF1 preserves the metric. Since (U,du2+dv2) is locally Euclidean, [F4] also makes both induced metrics flat.

F4step 1.1algebra
2.2

The constant unit normal NF=(0,0,1) and every second derivative of F are zero. The Cartesian Euclidean symbols vanish by [F3], so [F2] gives IIF(i,j)=0 for every i,j.

F2F3step 1.1algebra
2.3

The outward unit cylinder normal is NG=(cosθ,sinθ,0). Here Guu=(1/r)NG is already normal, while Guv=Gvv=0. Thus [F2]–[F3] give IIG(u,u)=(1/r)NG0 and zero for the other coordinate pairs.

F2F3step 1.1algebra
3.1

The isometry in step 2.1 identifies the same intrinsic metric on the two strips, but steps 2.2–2.3 exhibit a tangent pair for which one second fundamental form is zero and the other is nonzero. Hence no transport by that intrinsic isometry can identify the two forms, which is the promised concrete failure of the false claim.

step 2.1step 2.2step 2.3algebra
4.1

The domain and both images are nonempty fixed two-manifolds, so zero- and one-dimensional cases are inapplicable. The condition r>0 makes the interval nonempty, the embeddings immersive, and 1/r defined; r=0 is the excluded collapsed cylinder. The open interval omits both seam endpoints, and the images have no manifold boundary. The embeddings, normals, and isometry are explicit. The only choice assumption is the stated ACω inherited through [F2], and the calculations add none. The item refutes a universal determination claim by one witness rather than asserting a biconditional.

F1F2F3F4step 1.1step 2.1step 2.2step 2.3step 3.1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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