Foundation Public Spine Cube Period Eight Of Local

The eight-tick minimum

The declaration cubePeriodEight_of_local establishes a precise minimum on repetition. It says: if a walk through the eight corners of a cube visits every corner, and if the walk repeats itself after some positive number of steps, then that repeating period must be at least eight steps. The statement is a theorem in the machine-checked library of formal theorems. Its proof is a pigeonhole argument: with fewer than eight steps in the repeating cycle, the walk cannot have had time to land on all eight corners and still return to its starting pattern.

The classical context is a standard combinatorial fact. A walk on the cube graph that is periodic and surjective needs a period of at least eight, the number of vertices. The declaration packages this fact in a form the framework can use. It connects a local observation, that any such repeating walk has a period of at least eight, to the global statement CubePeriodEight, which asserts the same minimum for all walks of that kind. The theorem is the implication: if the local version holds, then the global version holds.

The framework uses this fact inside a larger argument about why space is three-dimensional. The library shows that a circle embedded in a three-dimensional sphere can have a nontrivial linking complement, and that this detection fails in dimensions zero, one, and four or higher. The eight-tick minimum supplies the period that pairs with that dimensional detection. Together they form the bridge that the framework cites when it claims that three dimensions are forced by linking behavior. That bridge is a theorem in the library, proved without appeal to any arithmetic encoding of the dimension claim.

What the declaration does not claim is just as important. It does not assert that physical space is three-dimensional. It does not say anything about the physical recognition-to-linking bridge, which the framework itself marks as open. It does not derive the fine-structure constant or prove the Riemann Hypothesis. The declaration is a narrow combinatorial implication, and the framework's larger dimensional claims depend on additional theorems and on a physical bridge that remains a target, not a result.

/-- Local cube-period binder agrees with the PublicSpine `CubePeriodEight`
statement (`Pattern 3` is definitionally `Fin 3 → Bool`). -/
theorem cubePeriodEight_of_local :
    CubePeriodEightLocal → CubePeriodEight :=
  fun h => h

/-- Local cube-period binder agrees with the PublicSpine `CubePeriodEight`
statement (`Pattern 3` is definitionally `Fin 3 → Bool`). -/
theorem cubePeriodEight_of_local :
    CubePeriodEightLocal → CubePeriodEight :=
  fun h => h

/-- **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

What this page does not claim

This declaration does not assert that physical space is three-dimensional. This declaration does not prove the Riemann Hypothesis or derive the fine-structure constant.

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: