Foundation T7 Cycle Realization Gray Cycle3 Realizes Circle

The Gray cycle and the circle

A Gray code is a sequence of binary strings in which each consecutive pair differs in exactly one bit. The canonical 3-bit Gray code runs 000, 001, 011, 010, 110, 111, 101, 100, then back to 000, and every one of the eight possible 3-bit strings appears exactly once. This is a Hamiltonian cycle on the cube graph, the graph whose vertices are the eight strings and whose edges connect strings differing in one bit.

The Recognition Science framework's machine-checked library of formal theorems contains a declaration, grayCycle3_realizes_circle, that takes this classical object and attaches a geometric meaning to it. The framework models a ledger, a discrete record of events, as a walk on a cube of bit patterns. The theorem states that when the canonical 3-bit Gray cycle is read as such a walk, its realized defect is a circle. The proof is by definitional reduction: the library defines the realized defect of any closed walk in a cellular completion to be the circle, so the result holds by unfolding definitions.

The declaration also proves a negative claim: the same Gray cycle does not realize as a sphere of dimension 2 or higher. The library defines the sphere dimension of a graph-shaped closed walk image to be exactly 1, so no closed walk on a cube graph can realize S^p for p ≥ 2. This is a combinatorial fact about the cube graph, not a statement about physical space. The framework's separate claim that three spatial dimensions are forced by linking is a different theorem, and the physical bridge from recognition to linking remains open.

What the declaration does not claim is as important as what it proves. It does not claim that the circle is a physical object in three-dimensional space. It does not claim that the Gray cycle is the only cycle that realizes as a circle. And it does not claim that the full CW or covering space realization of the walk as a circle has been constructed; that remains a model, a definitional choice in the library, not a proved theorem. The declaration is a precise statement about a combinatorial object and its assigned geometric image, and it is proved in full.

/-- Specialization of the realization theorem to the canonical 3-bit Gray cycle. -/
theorem grayCycle3_realizes_circle
    (cell : SubstrateAxioms.CellularCompletion 3) :
    RealizedDefect cell grayCycle3ClosedWalk = Circle := by
  exact t7_cycle_realizes_circle 3 (by decide) cell
    grayCycle3ClosedWalk grayCycle3ClosedWalk_hamiltonian

/-- The canonical 3-bit Gray cycle does not realize as `S^p` for any `p ≥ 2`. -/
theorem grayCycle3_no_higher_sphere (p : ℕ) (hp : 2 ≤ p) :
    ¬ ImageIsSpherePofDim grayCycle3ClosedWalk p :=
  no_higher_sphere_from_closed_walk grayCycle3ClosedWalk p hp

What this page does not claim

The circle is a physical object in three-dimensional space. The Gray cycle is the only closed walk that realizes as a circle. The full CW or covering space realization of the walk as a circle has been constructed.

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/T7CycleRealization.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: