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

E_passive

show as:
view Lean formalization →

E_passive supplies the integer count of passive field edges in the cubic ledger Q3. Mass anchor and alpha derivations cite this count to fix the geometric seed factor and lepton sector exponents. The definition is a direct specialization of passive_field_edges to dimension 3.

claimThe number of passive (field-dressing) edges of the cubic ledger $Q_3$ is defined by $E_ {passive} := 11$.

background

The T9 module constructs the refined ledger fraction for the electron mass shift from Q3 geometry. Passive edges are the cube edges that dress the interaction, obtained by subtracting the single active edge per tick from the total cube edges. The upstream passive_field_edges definition computes this difference for any dimension d, while the sibling abbrev in Anchor specializes it to general D.

proof idea

One-line definition that applies passive_field_edges to the concrete argument 3.

why it matters in Recognition Science

This supplies the integer 11 that enters the geometric seed factor and the B_pow lepton exponent. It is invoked by geometric_seed_factor_eq_11, passive_edges_at_D3, B_pow, and the lepton rung theorems. The count follows from the D=3 topology fixed by the forcing chain.

scope and limits

Lean usage

theorem passive_edges_at_D3 : passive_field_edges 3 = 11 := by simp [E_passive]

formal statement (Lean)

  45def E_passive : ℕ := passive_field_edges 3

proof body

Definition body.

  46
  47/-- Wallpaper groups (Face symmetries). -/

used by (40)

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

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.