LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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 Whitney framing extends over a clean disk in the stable range

Statement

Assume ${A C}_{ω}$ . Let $W$ be a clean embedded Whitney bigon for complementary sheet neighbourhoods $A^{a}, B^{b}$ along its boundary arcs, $a, b \geq 3$ , with local orientations and opposite corner signs in an oriented disk tube. Then $W$ admits an admissible normal framing after an allowed correction in one sheet-normal summand, supported away from its fixed corner collars. Thus every clean disk under these hypotheses can be framed, and clean framed disks exist when the Whitney circle is nullhomotopic and the clean-disk existence hypotheses hold. The disk normal rank is $N = m - 2$ . Relative to a global oriented disk-normal frame the obstruction of a chosen admissible full boundary frame is its loop class in $π_{1} (S O (N))$ . A correction within a rank- $(a - 1)$ or rank- $(b - 1)$ summand realizes its inverse. This is existence of an extendible admissible choice; an arbitrary prescribed full frame need not extend. The rounded circle has normal rank $m - 1$ , which is not the obstruction rank. Global orientation of $X, A, B$ is unnecessary; the globally oriented closed-sheet case is a special case.

Facts & Assumptions

[F1]

Opposite signs in locally oriented sheet collars give compatible adjustable admissible partial boundary frames. Opposite local signs give the compatible Whitney-circle framing

[F2]

For $N > r \geq 2$ , the block inclusion $S O (r) \to S O (N)$ is onto on fundamental groups. A normal summand of rank at least two realizes every framing-loop obstruction

[F3]

Under Countable Choice, continuous manifold-valued maps smooth near a closed set can be smoothed through a homotopy fixed near that set. Relative Whitney approximation for manifold-valued maps

[F4]

Gram–Schmidt orthonormalizes a finite independent list and preserves its successive spans. Gram–Schmidt turns every finite independent list into an orthonormal list with the same successive spans

[F5]

Part (i) gives choice-free Stiefel connectivity through complement rank minus one; part (ii) extends an admissible partial frame before choosing its orthogonal complement. Frame fields with prescribed boundary conditions along a clean Whitney disk

Proof

Given: The clean bigon, oriented local sheet collars with opposite corner signs, countable choice, and any initially chosen admissible boundary frame.

1.1givenconstructF1

The compatible-framing lemma constructs an admissible boundary splitting and frames and gives a global rank- $(m - 2)$ disk-normal trivialization by explicit radial projection transport. Compare the boundary frame with this global frame, matching its orientation. The comparison is a based loop in $S O (m - 2)$ after a constant frame change at one corner. The loop extends over the disk exactly when its class is trivial: an extension gives a nullhomotopy and a nullhomotopy gives a disk extension.

2.1step 1.1constructF2F3F4

Apply the earlier normal-summand surjection with $N = m - 2$ and $r = a - 1 \geq 2$ . Here $N - r = b - 1 \geq 2$ , and in particular $N > r$ . Choose a based loop within that summand mapping to the inverse full-frame loop class. Reparametrize it to be supported in the interior of one sheet arc, keeping its endpoint collars constant. Multiplication within the summand preserves its subspace and sheet tangency while fixing every corner value, and kills the full-frame obstruction. The corrected loop extends over the disk. Smooth that extension relative to the boundary collar and apply orthonormalization, yielding a smooth admissible disk-normal frame.

3.1step 2.1constructF5∎

Alternatively the preceding frame-fields lemma extends the admissible partial $E$ frame first in $V_{a - 1} (R^{m - 2})$ and then chooses $H$ in its orthogonal complement; it supplies an extendible admissible choice directly. Both routes permit choosing the full boundary class, and neither asserts extension of every previously fixed class. The extra inward tangent-to-disk line belongs to the rounded circle-normal bundle and is not included in the disk-normal loop comparison. The constructions use only the tube and arc orientations, so the locally oriented formulation and its global specialization follow.

Depends on

Used by

Whitney disjunction removes algebraically cancelling double points Proposition
The high-dimensional Whitney trick Theorem

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

Andrew Ranicki, Algebraic and Geometric Surgery (Oxford Mathematical Monographs, Oxford University Press 2002; complete electronic copy) (standard reference, not scraped)
John Milnor, Lectures on the h-Cobordism Theorem (notes by L. Siebenmann and J. Sondow, Princeton University Press 1965; scanned edition with searchable text layer) (standard reference, not scraped)