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

g2FromLoops

show as:
view Lean formalization →

g2FromLoops supplies the structural expression for the muon g-2 anomaly in terms of the Recognition Science bridge geometry. Researchers deriving particle constants from the phi-ladder and loop structures would reference it to obtain the canonical result 1/phi^5. The definition reduces directly to the reciprocal of phi raised to the loopOrder integer carried by the RSBridge record.

claim$g_2(B, phi) = 1 / phi^{B.loopOrder}$ where $B$ is an RSBridge instance over ledger $L$ and $phi$ is a real parameter.

background

The Bridge Derivation module extracts canonical CKM mixing angles and the g-2 anomaly from RSBridge geometry. RSBridge carries a structural loopOrder field (default 5) together with cycle and defect data. Upstream, L is the unit ledger with debit and credit both equal to 1, while canonicalRSBridge constructs the default bridge instance used in the downstream theorems.

proof idea

One-line definition that directly returns the reciprocal of phi raised to the power of the bridge's loopOrder field.

why it matters in Recognition Science

The definition is invoked by canonical_g2FromLoops and g2FromLoops_canonical to prove that the canonical bridge yields g-2 = 1/phi^5. It supplies the g-2 step inside the Bridge Derivation module, linking the loop-order integer to the phi fixed point of the forcing chain and the eight-tick octave.

scope and limits

formal statement (Lean)

  48def g2FromLoops (B : RSBridge L) (φ : ℝ) : ℝ :=

proof body

Definition body.

  49  1 / (φ ^ B.loopOrder)
  50
  51/-- For the canonical bridge, V_cb = 1/24. -/

used by (2)

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

depends on (9)

Lean names referenced from this declaration's body.