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

B_pow

show as:
view Lean formalization →

B_pow maps each of the four sectors to an integer exponent drawn from three-dimensional cube edge counts. Mass ladder calculations cite it when forming the yardstick A_s = 2^{B_pow} * E_coh * phi^{r0} for leptons, quarks, and electroweak bosons. The definition is a direct case split on the Sector inductive type that substitutes the precomputed constants E_passive = 11, A = 1, and E_total = 12.

claimThe function $B_ {pow} : Sector → ℤ$ is given by $B_{pow}(Lepton) = -2 × 11$, $B_{pow}(UpQuark) = -1$, $B_{pow}(DownQuark) = 2 × 12 - 1$, $B_{pow}(Electroweak) = 1$, where the integers 11, 1, and 12 are the passive edge count, active edges per tick, and total cube edges in three dimensions.

background

The Masses.Anchor module centralizes parameter-free constants derived from cube geometry at D = 3. E_total is defined as cube_edges D = 12, E_passive as passive_field_edges D = 11, and A as active_edges_per_tick = 1. The Sector inductive type classifies the four cases: Lepton, UpQuark, DownQuark, Electroweak.

proof idea

The definition is a direct pattern match on the four constructors of Sector. Each branch substitutes the corresponding combination of E_passive, A, and E_total, which are themselves abbreviations for the cube edge functions imported from the module.

why it matters in Recognition Science

B_pow supplies the integer exponents required by the downstream yardstick definition and by the four equality theorems B_pow_Lepton_eq, B_pow_UpQuark_eq, B_pow_DownQuark_eq, and B_pow_Electroweak_eq. It encodes the D = 3 cube geometry step of the forcing chain into the mass formulas. The module states that all sector constants are derived from first principles without experimental input.

scope and limits

Lean usage

theorem B_pow_Lepton_eq : B_pow .Lepton = -22 := by simp only [B_pow, E_passive]; norm_num

formal statement (Lean)

  74@[simp] def B_pow : Sector → ℤ
  75  | .Lepton      => -(2 * (E_passive : ℤ))     -- = -(2 × 11) = -22
  76  | .UpQuark     => -(A : ℤ)                    -- = -1
  77  | .DownQuark   => 2 * (E_total : ℤ) - 1       -- = 2 × 12 - 1 = 23
  78  | .Electroweak => (A : ℤ)                     -- = 1
  79
  80/-- Derived φ-exponent offsets per sector.
  81    These are NOT arbitrary—they come from wallpaper + cube geometry. -/

used by (19)

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

depends on (14)

Lean names referenced from this declaration's body.