dimensionEightTickOpen_holds
plain-language theorem explainer
The public D=3 and eight-tick targets are definitionally the non-encoding Alexander linking bridge and that bridge conjoined with cube period eight. Cite this when the dual public spine (not the UFC certificate names) is the architecture claim for T7/T8. The proof is two definitional equalities by reflexivity.
Claim. The public spatial-dimension target equals nonemptiness of the Alexander linking bridge, and the public eight-tick target equals the conjunction of that same dimension target with the cube period-eight statement. Both equalities hold as content-typed binders (now closed).
background
PublicSpine is the dual forcing surface of UnifiedForcingChain: a δ-stratified map for papers and loops that mean "what is forced," while UFC names remain certificate/floor witnesses. Contract rules forbid encoding predicates; T7 and T8 must route through the Alexander linking bridge, not a bare sphere-admits-circle-linking predicate.
The structure being inhabited packages two disclosure equalities. The D=3 public target is identified with nonemptiness of the Alexander linking bridge (unknot-complement retract, excision spine, arc-complement acyclicity). The eight-tick public target is identified with that D=3 target together with cube period eight (pigeonhole on the 2^3 octave).
Module doc records campaign P-d3link (2026-07-18): the bridge is fully inhabited in PublicSpineLinkingClosure with zero sorry and only standard classical axioms, so these binders moved from open to theorem while keeping content typing (panel K1).
proof idea
Term-mode structure inhabitation. Each field is discharged by rfl: the left-hand public target abbreviations are definitionally equal to the right-hand bridge and period packages as written in the structure. No lemmas are applied; the equalities are by construction of the named targets.
why it matters
This is the honest public replacement for citing nonemptiness of the old T7 eight-tick and T8 dimension certificates. Framework landmarks: T7 (eight-tick octave, period 2^3) and T8 (D=3 spatial dimensions) in the forcing chain. Downstream used_by is empty here; the value is citation hygiene on the dual surface so papers quote content-typed binders rather than encoding-friendly certificate names.
Together with the linking-closure inhabitation, it marks the D=3 / 8-tick bridge target CLOSED on the public spine. Cost-selection, φ-from-iota, and the δ-only tower remain separate packages in the same module; this declaration only seals the dimension/period disclosure equalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.