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

E

show as:
view Lean formalization →

The definition computes the number of edges in the D-dimensional hypercube via the formula D times 2 to the power D minus 1. Researchers deriving the 48 chiral fermionic states and SU(3) x SU(2) x U(1) content from the Q3 cube in Recognition Science cite this count when closing the combinatorial loop from T8. It is a direct algebraic definition with no lemmas or tactics required.

claimThe number of edges in the D-dimensional hypercube is given by $D$ times $2^{D-1}$.

background

The Spectral Emergence module starts from the forced datum D equals 3 in the T8 step of the unified forcing chain and examines the binary cube Q3 with eight vertices. This cube's edge count enters the derivation of the automorphism group order 48, which matches the total chiral fermion degrees of freedom in the Standard Model. Upstream structures supply the J-cost minimization (strictly convex with unique minimum at argument 1) from PhiForcingDerived and the ledger factorization from DAlembert.LedgerFactorization.

proof idea

The declaration is a direct definition implementing the standard combinatorial formula for hypercube edges. No lemmas are applied and no tactics are used; the body simply multiplies dimension by the number of parallel classes per direction.

why it matters in Recognition Science

This supplies the edge count that supports the Q3 structure forcing SU(3) times SU(2) times U(1) gauge content, three generations from face-pair count, and the 48 fermionic states matching the automorphism order, as described in the module documentation. It is referenced by downstream results including geodesicEquationHolds in EulerLagrange, hamilton_equations_from_EL and totalEnergy in Hamiltonian, and phi_energy_rung_zero in PhotobiomodulationDevice. The definition closes part of the self-consistency loop from T8 to the fermion spectrum.

scope and limits

formal statement (Lean)

  85def E (D : ℕ) : ℕ := D * 2 ^ (D - 1)

proof body

Definition body.

  86
  87/-- 2-faces (squares) of the D-cube: each pair of coordinate axes gives
  88    a family of 2^(D-2) parallel squares. Total = C(D,2) × 2^(D-2). -/

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.