Pure Harness

Section 1

Classical setting

Work on the Riemann sphere. The pure carrier is the meromorphic 1-form ω₀ = dz/z with residues +1 at 0 and −1 at ∞. For g ∈ PSL(2,ℂ) set ω_g = g* ω₀. A dual-residue pair is the ordered pair of residues of ω_g at a point and at its inverse; the global residue theorem enforces exact balance of the full residue divisor.

• provedpure_carrier_balancetheorem

  Residues of ω₀ = dz/z sum to zero: 1 + (−1) = 0.

• provedpure_residual_vanishestheorem

  Equal magnitudes on the pure pair force R = 0.

• provedresidualLogCoord_of_eq_magtheorem

  log |a| − log |a| = 0 on the real carrier.

theorem pure_carrier_balance : (1 : Int) + (-1) = 0 :=
  Kernel.pureCarrier_balance

theorem residualLogCoord_of_eq_mag (p : DualResiduePair)
    (h : p.magA = p.magIota) :
    residualLogCoord p = 0 := by
  simp [residualLogCoord, h]
  exact realLog_sub_self p.magIota