RealizedDefect
plain-language theorem explainer
Any closed walk on the D-cube, relative to a cellular completion of the cube graph, is assigned the circle defect as its realized shape. The T7 realization theorems and the forcing-chain bridge to S¹ cite this assignment. The body is a constant definition returning the circle constructor of the recognized-defect type.
Claim. For every dimension $D\in\mathbb{N}$, every cellular completion of the $D$-cube graph, and every closed walk $W$ on that cube, the realized defect of $W$ is the circle defect (the $S^1$ case of the recognized-defect classification).
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 on the cube graph realizes a higher sphere $S^p$ with $p\ge 2$. Topology stays predicate-level; only elementary finite-dimensional arithmetic is proved, matching the AlexanderDuality discipline.
A closed walk on the $D$-cube is a phase-indexed path through the $D$-bit pattern space (length $2^D$). A cellular completion (T7.5a) packages three structural clauses used in the dimension paper: a closed orientable smooth $D$-manifold substrate, a tame cube-graph embedding, and a retraction back to the cube graph; those fields are presently proof placeholders (True).
Recognized defects are an inductive classification with three shapes: circle, sphere of dimension $p$, or unknown. The circle constructor is the value this definition always returns. Upstream dimension constants fix spatial $D=3$ via T8/T9, but the definition itself is parametric in $D$.
proof idea
Constant definition, not a proof. The body ignores both the cellular-completion witness and the closed walk and returns the circle constructor of RecognizedDefect. Downstream equalities such as the main T7 realization statement are therefore rfl.
why it matters
This is the API hinge for T7 cycle realization in the forcing chain. The main theorem states that, for $D\ge 2$, a Hamiltonian closed walk in a cellular completion has realized defect equal to the circle; that proof is rfl against this definition. The 3-bit Gray-cycle specialization and the UnifiedForcingChain bridge T7_To_Realization_Bridge both demand that the canonical $D=3$ Gray cycle realizes as a circle in any T7.5a completion.
In the primer landmarks this sits at T7 (eight-tick octave, period $2^3$) feeding the T8 $D=3$ spatial-dimension step: a graph-shaped cycle must realize as $S^1$, not a higher sphere. Spine-audit certificates record explicitly that the assignment is definitional (RealizedDefect is always Circle), so the present surface encodes the paper conclusion at predicate level rather than discharging smooth topology. Full CW/covering-dimension formalization is reserved for a later Mathlib-backed pass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.