Foundation Active Edge Budget One Bit Diff Iff Hamming One

The one-bit edge

In the geometry of binary strings, a natural question is when two strings of zeros and ones should count as neighbors. The classical answer, used across coding theory and computer science, is the Hamming distance: the number of positions in which the two strings differ. Two strings of length three, for instance, are adjacent in the three-dimensional cube exactly when their Hamming distance is one. The declaration oneBitDiff_iff_hamming_one states this identification as a formal theorem: a pair of binary patterns differs in exactly one bit if and only if their Hamming distance is one.

The proof is a direct unpacking of definitions. The framework defines an edge between two vertices of a cube as the condition that their Hamming distance equals one. The theorem then shows this matches the predicate OneBitDiff, which asserts the two patterns differ in exactly one coordinate. The proof is immediate from the definitions, with no additional assumptions. It is a machine-checked result in the framework's library of formal theorems, meaning a computer program has verified every step of the reasoning.

This one-bit identification is not an isolated curiosity. It underpins a budget calculation in the Recognition Science framework, where the framework models a discrete record of events called a ledger. In the framework's canonical eight-tick cycle, consecutive postings to the ledger traverse exactly one edge of the three-dimensional cube. The theorem oneBitDiff_iff_hamming_one is the bridge that lets the framework count those edges: each step changes exactly one bit, so each step crosses exactly one edge. From this, the framework derives that the number of active edges per tick is forced to be one, not chosen as a postulate.

What the theorem does not claim is broader. It does not assert that the physical universe operates on a ledger, nor that recognition events occur. Those are modeling choices within the framework, not consequences of this theorem. The theorem itself is purely combinatorial: it concerns binary strings and a distance function, with no physics attached. It also does not claim that every pair of binary strings with Hamming distance one is a meaningful transition in any particular process; it only states the equivalence between the two definitions of adjacency.

/-- `OneBitDiff p q` (consecutive Gray-cycle postings differ in
exactly one bit) is equivalent to `hammingDist p q = 1`. -/
theorem oneBitDiff_iff_hamming_one {d : ℕ} (p q : Pattern d) :
    OneBitDiff p q ↔ hammingDist p q = 1 := by
  classical
  unfold OneBitDiff hammingDist
  refine ⟨?_, ?_⟩
  · rintro ⟨k, hk_ne, hk_uniq⟩
    -- ExistsUnique gives us: the filter set is exactly {k}.
    have hset : (Finset.univ.filter (fun j : Fin d => p j ≠ q j)) = {k} := by
      ext j
      simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_singleton]
      refine ⟨?_, ?_⟩
      · intro hj_ne; exact hk_uniq j hj_ne
      · rintro rfl; exact hk_ne
    rw [hset]; simp
  · intro hcard
    -- Filter set has cardinality 1, so it is a singleton {k}.
    have hne : (Finset.univ.filter (fun j : Fin d => p j ≠ q j)).Nonempty :=
      Finset.card_pos.mp (by rw [hcard]; exact Nat.one_pos)
    obtain ⟨k, hk_mem⟩ := hne
    have hk_ne : p k ≠ q k := by
      simpa using (Finset.mem_filter.mp hk_mem).2
    refine ⟨k, hk_ne, ?_⟩
    intro j hj_ne
    -- Cardinality 1 + k ∈ set + j ∈ set ⇒ j = k.
    have hj_mem : j ∈ Finset.univ.filter (fun j : Fin d => p j ≠ q j) := by
      simp [hj_ne]
    have hsubset : ({j, k} : Finset (Fin d)) ⊆
        Finset.univ.filter (fun j : Fin d => p j ≠ q j) := by
      intro x hx
      simp only [Finset.mem_insert, Finset.mem_singleton] at hx
      rcases hx with rfl | rfl
      · exact hj_mem
      · exact hk_mem
    by_contra hne
    have hcard2 : ({j, k} : Finset (Fin d)).card = 2 := by
      rw [Finset.card_insert_of_notMem (by simp [hne]), Finset.card_singleton]
    have : 2 ≤ (Finset.univ.filter (fun j : Fin d => p j ≠ q j)).card :=
      hcard2 ▸ Finset.card_le_card hsubset
    omega

/-- **CONSEQUENCE.** Consecutive postings in the canonical 3-bit
Gray cycle traverse exactly one cube edge. -/
theorem grayCycle3_per_tick_edge_count (i : Fin 8) :
    edgesTraversed (grayCycle3Path i) (grayCycle3Path (i + 1)) = 1 := by
  unfold edgesTraversed
  exact (oneBitDiff_iff_hamming_one _ _).mp (grayCycle3_oneBit_step i)

/-- The downstream definition equals 1 (`rfl`-level), and 1 is the
unique value forced by `oneBit_step` (`per_tick_edge_count_unique`).
Together: the postulate is correctly chosen. -/
theorem active_edges_per_tick_eq_one_and_forced :
    Constants.AlphaDerivation.active_edges_per_tick = 1 ∧
    (∀ n : ℕ,
       (∀ i : Fin 8,
         edgesTraversed (grayCycle3Path i) (grayCycle3Path (i + 1)) = n) →
       n = 1) := by
  refine ⟨rfl, per_tick_edge_count_unique⟩

What this page does not claim

The theorem does not assert that the physical universe operates on a ledger. The theorem does not claim that recognition events occur in nature. The theorem does not state that every one-bit difference corresponds to a meaningful transition in any process.

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