Foundation Public Spine Target Eight Tick Of Bridge

The eight-tick bridge

In topology, a circle can be knotted or linked around a sphere only when the sphere sits in three-dimensional space. The Recognition Science framework's machine-checked library of formal theorems proves a precise version of this fact: a circle embedded in a sphere complement with nontrivial winding exists exactly in dimension three. This is the bridge that connects the abstract idea of linking to the concrete number of spatial dimensions.

The declaration target_eight_tick_of_bridge takes that three-dimensional result and adds a purely combinatorial fact about a cube. A walk that moves through the eight corners of a cube, where each step toggles one of three switches. The theorem proves that any such walk that repeats itself with period p and visits all eight corners must have p at least 8. This is a pigeonhole argument: with only three switches, you cannot cycle through all eight states in fewer than eight steps.

Together, the two pieces form a single claim: if linking forces dimension three, and dimension three forces an eight-step period, then the eight-tick cycle is forced. The theorem is fully proved in the framework's library, with no unproved assumptions beyond the standard logical axioms. It does not, however, claim that the physical universe actually has three dimensions; that bridge from the topological theorem to physical recognition is explicitly left open.

What the declaration does not claim is just as important. It does not say that recognition events themselves occur in eight discrete ticks; that would be a physical interpretation, not a proved theorem. It does not derive the fine-structure constant or any other physical constant. And it does not claim that the eight-tick cycle is unique; other cycles with period greater than eight also exist. The theorem is a precise mathematical statement about linking and periodicity, not a claim about the empirical world.

/-- **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 period bound holds** (R0 of campaign P-d3link,
2026-07-17). Periodicity confines the walk's range to its first `p` values,
so surjectivity onto the `2³ = 8` cube corners forces `8 ≤ p` by counting.
Honest pigeonhole content; nothing here touches the D=3 bridge. -/
theorem cubePeriodEight_holds : CubePeriodEight := by
  classical
  intro walk p hp hper hsurj
  have hshift : ∀ k n, walk (n + k * p) = walk n := by
    intro k
    induction k with
    | zero => intro n; simp
    | succ k ih =>
      intro n
      have hsplit : n + (k + 1) * p = (n + k * p) + p := by ring
      rw [hsplit, hper, ih]
  have hmod : ∀ n, walk n = walk (n % p) := by
    intro n
    have h := hshift (n / p) (n % p)
    rwa [Nat.mod_add_div'] at h
  let f : (Fin 3 → Bool) → Fin p := fun x =>
    ⟨(hsurj x).choose % p, Nat.mod_lt _ hp⟩
  have hf : ∀ x, walk ((f x : Fin p) : ℕ) = x := by
    intro x
    exact ((hmod (hsurj x).choose).symm.trans (hsurj x).choose_spec)
  have hinj : Function.Injective f := by
    intro x y hxy
    have hx := hf x
    rw [hxy, hf y] at hx
    exact hx.symm
  have hcard := Fintype.card_le_of_injective f hinj
  simpa using hcard

/-- 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 theorem does not claim that physical recognition events occur in eight discrete ticks. It does not derive any physical constant such as the fine-structure constant. It does not claim that the eight-tick period is unique among all possible cycles.

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: