RecognizedDefect
plain-language theorem explainer
Enumeration of topological shapes a realized defect may take: the circle, a p-sphere for natural p, or an unclassified residual. The T7 cycle-realization surface cites it when recording that a cube closed walk realizes as S¹ rather than a higher sphere. Pure inductive definition with decidable equality; no proof content.
Claim. A recognized defect is one of three alternatives: the circle $S^1$, a sphere $S^p$ for some $p \in \mathbb{N}$, or an unknown residual shape.
background
The module 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$ with $p \ge 2$. Smooth-topology content stays predicate-level; the file proves elementary finite-dimensional arithmetic and exposes the names the forcing chain needs.
Upstream, the defect functional is the cost $J$ on positive reals (zero at unity). Here "recognized defect" is not that scalar cost, but a discrete tag for the topological type of the shape that a cellular completion of a cube closed walk is said to realize.
Sibling notions include closed walks on the cube graph, Hamiltonian and edge-distinct walks, and image-is-circle / image-is-sphere predicates used by the realization theorems.
proof idea
Inductive type with three constructors (circle, sphere carrying a natural dimension, unknown) and a derived DecidableEq instance. No proof body and no axioms; it is pure data for the realization surface.
why it matters
Feeds the local constants Circle (the circle tag) and RealizedDefect (which, for any cellular completion and cube closed walk, returns the circle tag). Those definitions underwrite the paper-facing claim that the T7 graph-shaped cycle realizes as $S^1$ and that no cube closed walk realizes $S^p$ for $p \ge 2$.
In the forcing chain this is the shape vocabulary for T7 (eight-tick octave, period $2^3$) on the way to T8 ($D = 3$ spatial dimensions). The module deliberately matches the existing Alexander-duality discipline: names and arithmetic now, full CW/covering-dimension formalization later.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.