Foundation Public Spine Dimension Eight Tick Open Holds

The open dimension target

The declaration dimensionEightTickOpen_holds is a formal record inside the Recognition Science framework's machine-checked library of formal theorems. It states that a certain target proposition, called DimensionEightTickOpen, is inhabited: that is, the target is a well-formed statement that the library can name and manipulate. The target itself is a conjunction of two equalities. The first says that the goal of deriving three spatial dimensions from a non-encoding linking condition is the same as the existence of a bridge object called AlexanderLinkingBridge. The second says that the goal of deriving an eight-step cycle from three dimensions is the same as having both that bridge and a separate combinatorial fact called CubePeriodEight.

What the declaration does not do is prove either of those goals. The name "Open" is not decorative: the library treats the bridge and the period fact as targets to be reached, not as theorems already established. The declaration is a definitional scaffold, a way of saying precisely what would count as a derivation, and a way of holding the two goals linked so that progress on one is progress on the other. It is a statement about the shape of the problem, not a solution to it.

To see the shape, consider the two ingredients. The first is the claim that three dimensions are forced by a certain kind of linking: a circle embedded in a sphere in such a way that its complement has nontrivial homology. The library proves that such linking is detected in dimension three, and that it vanishes in dimensions zero and one. The second ingredient is a purely combinatorial statement: any periodic walk on the eight vertices of a cube that visits all of them must have period at least eight. The declaration ties these together: if the bridge exists, then the eight-tick target follows. But the bridge itself is not yet inhabited in the library, and so the eight-tick claim remains open.

This is an honest and deliberate posture. The framework's public surface refuses to attach a THEOREM badge to a claim that has not been proved. The declaration is a way of making the open status explicit, of naming the exact condition that would close it, and of preventing a future proof from being smuggled in through an encoding trick. It is a piece of bookkeeping that keeps the library honest about what has been derived and what has not.

For a reader, the practical consequence is this: the declaration is a target marker, not a result. It tells you what the framework aims to show, and it tells you that the aim has not been met. The three-dimensional forcing theorem itself is proved elsewhere in the library, but the step from that theorem to an eight-step cycle is a stated goal, with its conditions precisely recorded, and with no claim that the goal has been reached.

theorem dimensionEightTickOpen_holds : DimensionEightTickOpen where
  d3_is_bridge := rfl
  eight_is_bridge_and_period := rfl

/-- Disclosure: the D=3 / eight-tick public targets are exactly the content-typed
binders above (both now proved; see `PublicSpineLinkingClosure`). Citing this is
the honest replacement for `Nonempty T7_EightTick_Forced` /
`Nonempty T8_Dimension_Forced`. -/
structure DimensionEightTickOpen : Prop where
  d3_is_bridge :
    target_D3_from_nonencoding_linking = Nonempty AlexanderLinkingBridge
  eight_is_bridge_and_period :
    target_eight_tick_from_D3 =
      (target_D3_from_nonencoding_linking ∧ CubePeriodEight)

theorem dimensionEightTickOpen_holds : DimensionEightTickOpen where
  d3_is_bridge := rfl
  eight_is_bridge_and_period := rfl

/-- **The detection half is proved** (R2 of campaign P-d3link, 2026-07-17):
the flat unknot `z ↦ (z,0,0)` embeds S¹ in S³, and its complement retracts
onto the core circle `(0,0,w)`, so `H₁(S¹;ℤ) ≅ ℤ` (proved,
`circleH1ZIsoInt_holds`) is a retract of the complement's first homology,
which therefore is not zero. Real Mathlib singular homology throughout; no
arithmetic encoding anywhere in the proof
(`Foundation/UnknotComplementRetract.lean`). -/
theorem detectsNontrivialLinking_three : DetectsNontrivialLinking 3 :=
  ⟨UnknotComplementRetract.unknot, UnknotComplementRetract.unknot_isEmbedding,
    UnknotComplementRetract.unknotComplementH1_ne_zero
      CircleWindingChain.circleH1ZIsoInt_holds⟩

/-- **Vanishing at D = 0** (R3a of campaign P-d3link): every subspace of the
two-point S⁰ is totally disconnected, so complement H₁ vanishes for any map. -/
theorem not_detectsNontrivialLinking_zero : ¬ DetectsNontrivialLinking 0 :=
  LinkingVanishingLowDim.not_detects_zero

/-- **Vanishing at D = 1** (R3a of campaign P-d3link): an embedded circle in
S¹ is surjective (stereographic projection + connectedness), so the complement
is empty and its H₁ vanishes. -/
theorem not_detectsNontrivialLinking_one : ¬ DetectsNontrivialLinking 1 :=
  LinkingVanishingLowDim.not_detects_one

/-- The eight-tick target reduces to the D=3 bridge alone: the period half is
proved. -/
theorem target_eight_tick_of_bridge
    (h : target_D3_from_nonencoding_linking) : target_eight_tick_from_D3 :=
  ⟨h, cubePeriodEight_holds⟩

What this page does not claim

The declaration does not claim that three spatial dimensions are derived from linking; that is a separate theorem. The declaration does not claim that an eight-tick recognition cycle is derived or forced; it remains an open target. The declaration does not claim that the bridge object AlexanderLinkingBridge exists in the library; it only names the condition under which the target would be closed.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PublicSpine.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: