`gap`

definition

show as: view math explainer →

module: IndisputableMonolith.RSBridge.Anchor
domain: RSBridge
line: 73 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RSBridge.Anchor on GitHub at line 73.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  70    - F(24)   ≈ 5.74   (down quarks, q̃ = -2)
  71    - F(276)  ≈ 10.69  (up quarks, q̃ = +4)
  72    - F(1332) ≈ 13.95  (leptons, q̃ = -6) -/
  73noncomputable def gap (Z : ℤ) : ℝ :=
  74  (Real.log (1 + (Z : ℝ) / (Constants.phi))) / (Real.log (Constants.phi))
  75
  76notation "𝓕(" Z ")" => gap Z
  77
  78/-- The residue at the anchor for a fermion species.
  79
  80    This is the **definitional** (closed-form) residue: `F(Z_i) = gap(ZOf f)`.
  81
  82    **Relation to the axiom `f_residue`**: The physics claim (stated as an axiom in
  83    `AnchorPolicy.lean`) is that the RG-transport residue equals this value:
  84      `f_residue f μ⋆ = residueAtAnchor f`
  85    This is verified numerically by external tools. -/
  86noncomputable def residueAtAnchor (f : Fermion) : ℝ := gap (ZOf f)
  87
  88theorem anchorEquality (f : Fermion) : residueAtAnchor f = gap (ZOf f) := by rfl
  89
  90theorem equalZ_residue (f g : Fermion) (hZ : ZOf f = ZOf g) :
  91  residueAtAnchor f = residueAtAnchor g := by
  92  simp [residueAtAnchor, hZ]
  93
  94noncomputable def rung : Fermion → ℤ
  95| .e   => 2   | .mu  => 13  | .tau => 19
  96| .u   => 4   | .c   => 15  | .t   => 21
  97| .d   => 4   | .s   => 15  | .b   => 21
  98| .nu1 => 0   | .nu2 => 11  | .nu3 => 19
  99
 100def M0 : ℝ := 1
 101@[simp] theorem M0_pos : 0 < M0 := by
 102  dsimp [M0]; norm_num
 103

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.