pith. machine review for the scientific record. sign in
def definition def or abbrev high

cube_edges

show as:
view Lean formalization →

cube_edges supplies the closed-form count of edges in a d-dimensional hypercube as d times 2 to the power d-1. Derivations of the fine-structure constant in Recognition Science cite the D=3 case to fix the total at 12 and the passive field edges at 11. The definition is a direct algebraic expression with no lemmas or tactics.

claimThe number of edges in a $d$-dimensional hypercube is $d · 2^{d-1}$.

background

The Alpha Derivation module starts from the cubic ledger Q₃ as the fundamental unit cell forced by the Meta-Principle on Z³. D is fixed at 3 by the upstream forcing chain. Standard hypercube combinatorics then give vertices 2^D, edges d·2^(d-1), and faces 2d. These counts separate active edges (one per recognition tick) from the remaining passive field edges that dress the vacuum geometry.

proof idea

Direct definition that implements the standard hypercube edge formula. No lemmas are invoked and no tactics are applied; the expression is the closed combinatorial form.

why it matters in Recognition Science

The definition anchors the geometric seed 4π·11 and the seam numerator 6·17+1 inside alpha_ingredients_from_D3_cube and eleven_is_forced. Those theorems close the provenance of all numerical constants in the α^{-1} derivation to D=3 cube geometry, consistent with the eight-tick octave and the T8 forcing of three spatial dimensions.

scope and limits

Lean usage

theorem edges_at_D3 : cube_edges D = 12 := by native_decide

formal statement (Lean)

  54def cube_edges (d : ℕ) : ℕ := d * 2^(d - 1)

proof body

Definition body.

  55
  56/-- Number of faces in the D-hypercube: 2D. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.