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

A

show as:
view Lean formalization →

The constant for the active edge count per fundamental tick is set to the integer 1. Researchers on phi-power identities at three dimensions cite this assignment to simplify the balance phi to the power of (active edges minus gap) times phi to the gap. It is supplied as a direct definition.

claimThe active edge count per fundamental tick equals the integer 1.

background

The Integration Gap module examines the integer D squared times (D plus 2), called the integration gap. At D equals 3 this product is 45, formed from the parity count of 9 and the configuration dimension of 5. Upstream work in Gap45.Derivation fixes the gap at 45 as the product of closure and Fibonacci factors, while the anchor construction identifies the active edge count per tick as the unit that enters phi-power expressions.

proof idea

The declaration is a direct definition that assigns the integer 1. No lemmas or tactics are applied.

why it matters in Recognition Science

This constant supplies the active edge count used in the action theorems on energy conservation and Noether symmetries for space and time translations. It closes the phi-power balance identity at D equals 3, consistent with the forcing chain that selects three spatial dimensions and the eight-tick octave. The placement ties the edge count to the integration gap of 45, enabling the coprimality argument that forces odd D.

scope and limits

formal statement (Lean)

 105def A : ℤ := 1

proof body

Definition body.

 106
 107/-- The φ-power balance identity at `D = 3`:
 108    `φ^(A − gap) · φ^gap = φ`, equivalently `φ^(−44) · φ^45 = φ`. -/

used by (40)

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

… and 10 more

depends on (9)

Lean names referenced from this declaration's body.