Foundation Active Edge Budget Im Active Edges Per Tick Eq One

The one-edge step

In the Recognition Science framework, a tick is a single discrete step in a record of events. The declaration im_active_edges_per_tick_eq_one is a theorem in the framework's machine-checked library of formal theorems. It states that the number of active edges traversed per tick is exactly one. This is not a postulate or a definitional choice; it is a proved consequence of how the framework's fundamental eight-step cycle is built.

The proof rests on a specific structure: the eight vertices of a three-dimensional cube, arranged in a Gray cycle. In such a cycle, consecutive vertices differ in exactly one coordinate, meaning they are joined by exactly one edge of the cube. The framework's library proves that each of the eight steps in its canonical cycle traverses exactly one such edge. The theorem then shows that any cycle with this property must have a per-tick edge count of one; the number one is the unique cardinality of a one-bit difference between two binary strings of length three.

This result matters because the framework uses this count as a budget for how much activity occurs in each tick. The value one is not an adjustable parameter. The theorem establishes that it is forced by the structure of the cycle itself. The framework's library also shows that this forced value connects to a partition between matter content and a consciousness ceiling, though that connection is a separate theorem built on top of this one.

Importantly, the declaration does not claim that physical reality operates through such a cycle, nor that the number one has any meaning outside the framework's model. It is a statement about the framework's own definitions and their logical consequences. The theorem is proved with zero axioms beyond the standard logical ones, but it is a statement about a formal model, not an empirical observation about the universe.

/-- Same statement on the `IndisputableMonolith.Constants.AlphaDerivation`
side. -/
theorem im_active_edges_per_tick_eq_one :
    IndisputableMonolith.Constants.AlphaDerivation.active_edges_per_tick = 1 := rfl

/-- **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 active-edge budget per tick is uniquely forced to 1.**

Any natural number `n` such that the per-tick edge count under the
canonical 3-bit Gray cycle is constantly `n` must equal 1. This is
the structural forcing of `active_edges_per_tick = 1`: no other value
of `n` is consistent with the Gray-cycle adjacency. -/
theorem per_tick_edge_count_unique (n : ℕ)
    (h : ∀ i : Fin 8,
      edgesTraversed (grayCycle3Path i) (grayCycle3Path (i + 1)) = n) :
    n = 1 := by
  have h0 := h 0
  rw [grayCycle3_per_tick_edge_count 0] at h0
  exact h0.symm

What this page does not claim

The theorem does not claim that physical reality is actually composed of such ticks or edges. The theorem does not claim that the number one has empirical significance outside the framework's model. The theorem does not assert that the Gray cycle is the only possible arrangement of an eight-step cycle.

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: