Foundation T7 Cycle Realization Gray Cycle3 Closed Walk Hamiltonian

The Gray cycle walk

A Gray code is a way to list every binary pattern of a fixed length so that consecutive entries differ in exactly one bit. For three bits, one such list runs 000, 001, 011, 010, 110, 111, 101, 100, and then wraps back to 000. Read as a closed walk on the corners of a cube, this list visits all eight vertices exactly once and takes one edge per step. That is a Hamiltonian cycle: a round trip through every vertex with no repeats.

The machine-checked library of formal theorems proves that this particular 3-bit Gray cycle is Hamiltonian. The proof is direct: the walk's path function is bijective, meaning it hits each of the eight patterns exactly once, and the consecutive-step property comes from the Gray-cycle adjacency field. A second theorem confirms the walk is edge-distinct, so each step really does flip exactly one bit. Together these two facts make the walk's image a combinatorial circle.

In Recognition Science, the framework models the T7 recognition cycle as a graph-shaped closed walk and records what shape that walk realizes. The declaration grayCycle3ClosedWalk_hamiltonian supplies the concrete instance: the canonical 3-bit Gray cycle is the Hamiltonian walk that the general T7 realization theorem needs. Specializing that theorem shows the realized defect of this walk is the circle, and no closed walk on a cube realizes a sphere of dimension two or higher.

What the declaration does not claim is just as important. It does not prove that every Hamiltonian closed walk is edge-distinct; that statement is false on this carrier, and the library explicitly records its deletion. It does not construct the circle as a continuous topological object. The realization as a circle remains a definitional choice at the cellular-completion layer, not a theorem about actual covering spaces. The walk's image is a combinatorial circle, and the higher-sphere exclusion is a statement about the predicate layer, not about all possible geometric embeddings.

/-- The explicit Gray walk is Hamiltonian. -/
theorem grayCycle3ClosedWalk_hamiltonian :
    Hamiltonian grayCycle3ClosedWalk := by
  simpa [Hamiltonian, grayCycle3ClosedWalk] using Patterns.grayCycle3_bijective

/-- The explicit Gray walk has combinatorial circle image. -/
theorem grayCycle3ClosedWalk_image_is_circle :
    ImageIsCircle grayCycle3ClosedWalk :=
  closed_walk_image_is_circle grayCycle3ClosedWalk
    grayCycle3ClosedWalk_hamiltonian grayCycle3ClosedWalk_edge_distinct

/-- Part (iv): no closed walk in a graph-shaped cube realizes a higher sphere. -/
theorem no_higher_sphere_from_closed_walk
    {D : ℕ} (W : ClosedWalkOnCube D) (p : ℕ) (hp : 2 ≤ p) :
    ¬ ImageIsSpherePofDim W p := by
  intro hp1
  dsimp [ImageIsSpherePofDim] at hp1
  subst p
  omega

What this page does not claim

Every Hamiltonian closed walk on a cube is edge-distinct; the library explicitly deletes that false claim. The circle is realized as a continuous topological object; that remains a definitional choice. The higher-sphere exclusion applies to all geometric embeddings, not just the predicate layer.

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: