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

passive_field_edges

show as:
view Lean formalization →

Passive field edges count the non-transition edges in a d-dimensional hypercube that dress the recognition interaction. Researchers deriving the fine-structure constant from cubic ledger geometry cite this to isolate the factor of 11 at D=3. The definition is a direct subtraction of the fixed active edge count of one from the closed-form hypercube edge total.

claimThe passive field edge count is given by $E(d) := d · 2^{d-1} - 1$, subtracting the single active edge traversed per atomic tick from the total hypercube edges.

background

The Alpha Derivation module constructs α^{-1} from the geometry of the unit cube Q_3 in the discrete ledger. For D=3 the cube has 12 edges total. One edge is traversed per atomic tick, leaving the passive field edges to mediate the coupling to the vacuum. The module doc states that these passive edges dress the interaction and supply the factor 11 to the geometric seed 4π × 11.

proof idea

One-line definition that subtracts the constant active_edges_per_tick from the result of cube_edges d.

why it matters in Recognition Science

This supplies the integer 11 that multiplies the solid angle in the geometric seed, feeding directly into alpha_seed_structural and geometric_seed_factor. It is invoked in mass anchor theorems such as B_pow_Lepton_eq and E_passive. The definition realizes the active/passive split required by the eight-tick octave and D=3 in the Recognition Science forcing chain.

scope and limits

Lean usage

theorem passive_edges_at_D3 : passive_field_edges D = 11 := by native_decide

formal statement (Lean)

  75def passive_field_edges (d : ℕ) : ℕ := cube_edges d - active_edges_per_tick

proof body

Definition body.

  76
  77/-- The key number: for D=3, passive edges = 11. -/

used by (40)

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

… and 10 more

depends on (3)

Lean names referenced from this declaration's body.