cross_sector_shift

formal source

  63/-- Cross-sector correction: +E = +12 for down quarks, 0 otherwise.
  64    This accounts for the cost of traversing the edge layer in the
  65    cube partition (the edge layer is owned by the lepton sector). -/
  66noncomputable def cross_sector_shift (sector : Anchor.Sector) : ℤ :=
  67  match sector with
  68  | .DownQuark => 12  -- E = cube_edges(3) = 12
  69  | _          => 0
  70
  71/-- SDGT mass prediction: m = A_s × φ^(r_sdgt - 8 + gap(Z) + shift). -/
  72noncomputable def predict_mass_sdgt (sector : Anchor.Sector) (name : String) : ℝ :=
  73  Anchor.yardstick sector *
  74  Constants.phi ^ (rung_sdgt sector name + gap sector name - 8 + cross_sector_shift sector)
  75
  76structure AnchorPolicy where
  77  lambda : ℝ
  78  kappa  : ℝ
  79
  80/-- Canonical anchor policy: `(λ, κ) = (ln φ, φ)` with coherence energy. -/
  81@[simp] noncomputable def canonicalPolicy : AnchorPolicy :=
  82  { lambda := Real.log Constants.phi
  83  , kappa  := Constants.phi }
  84
  85noncomputable abbrev E_coh : ℝ := Anchor.E_coh
  86noncomputable abbrev yardstick := Anchor.yardstick
  87abbrev Z_index := ChargeIndex.Z
  88abbrev r_lepton := Integers.r_lepton
  89abbrev r_up := Integers.r_up
  90abbrev r_down := Integers.r_down
  91abbrev r_boson := Integers.r_boson
  92
  93structure ResidueLaw where
  94  f : ℝ → ℝ
  95
  96structure SectorLaw where