pith. machine review for the scientific record. sign in
theorem proved term proof high

gap_factor_pos

show as:
view Lean formalization →

The gap-1332 resonance factor, defined as the reciprocal of 1332 times the golden ratio phi, is shown to be strictly positive. Researchers deriving the Recognition Science account of the muon g-2 anomaly would cite this result to fix the sign of the counter-term. The proof is a direct reduction via unfolding and the division-positivity lemma, using only the known positivity of phi.

claimThe gap-1332 resonance factor satisfies $1/(1332 phi) > 0$, where $phi$ is the self-similar fixed point of the forcing chain.

background

The EA-001 module derives the muon g-2 anomaly resolution via phi-ladder calibration of the RS counter-term. The gap-1332 factor is the resonance term introduced as the reciprocal of 1332 times phi. This positivity theorem rests on the explicit definition of that factor together with the positivity of phi supplied by the universal forcing self-reference structure.

proof idea

Unfold the definition of the gap-1332 factor to obtain the reciprocal form. Apply the div_pos lemma to reduce the claim to positivity of the denominator. The numerator 1 is immediate by norm_num; the denominator positivity follows by nlinarith on the known positivity of phi.

why it matters in Recognition Science

This result is EA-001.3 and supplies the sign needed for the EA-001 certificate and the positivity of the RS counter-term. It anchors the gap contribution inside the phi-ladder calibration of the muon anomaly, consistent with the T6 fixed-point step of the forcing chain. No open scaffolding questions are addressed here.

scope and limits

formal statement (Lean)

  46theorem gap_factor_pos : gap_1332_factor > 0 := by

proof body

Term-mode proof.

  47  unfold gap_1332_factor
  48  apply div_pos
  49  · norm_num
  50  · nlinarith [phi_pos]
  51
  52/-- The RS counter-term for muon g-2. -/

used by (2)

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

depends on (2)

Lean names referenced from this declaration's body.