Circle
plain-language theorem explainer
Names the circle as a recognized defect shape in the T7 realization surface. Anyone citing the claim that a cube closed walk realizes as S¹, or feeding Alexander duality and circle-covering arguments, uses this tag. The body is a one-constructor abbreviation of the RecognizedDefect inductive.
Claim. Write $\mathsf{Circle}$ for the circle case of a recognized defect shape (as opposed to a higher sphere $S^p$ or an unknown shape).
background
The module T7CycleRealization supplies a theorem surface for the strengthened T7/T8 dimension route: the T7 closed cycle is graph-shaped, so its realized defect is a circle $S^1$, and no closed walk in the cube graph realizes a higher sphere $S^p$ for $p \ge 2$. Smooth-topology content stays predicate-level; the module proves elementary finite-dimensional arithmetic and exposes the names the forcing chain needs.
RecognizedDefect is the small inductive of shapes used by that surface: circle, sphere of dimension $p$, or unknown. The defect functional itself (from LawOfExistence) equals the J-cost $J$ on positive reals; here the concern is geometric shape of the realized defect, not the scalar cost. Upstream forcing-chain material ties the eight-tick period to $D=3$.
proof idea
One-line definitional abbreviation: Circle is exactly the circle constructor of the RecognizedDefect inductive. No tactics, no lemmas.
why it matters
Gives a stable name for the circle defect that downstream T7/T8 and duality code cite. AlexanderDuality uses it in the reduced-cohomology characterization $\tilde H^k(S^1;\mathbb{Z})$ nontrivial iff $k=1$, in the predicate that $S^D$ admits nontrivial circle linking (via Alexander duality, Hatcher 3.44), and in the forward theorem that $D=3$ admits circle linking. CircleCovering transports Mathlib's circle covering and homeomorphism onto the metric unit-circle carrier. In the Recognition forcing chain this is the shape side of T7 (eight-tick octave) feeding the T8 claim $D=3$: the graph cycle realizes as $S^1$, not a higher sphere. Full CW/covering-dimension formalization is deferred.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.