logPotentialOf_flat

formal source

 255  fun i => Real.log (ψ i)
 256
 257/-- Flat potential `ψ ≡ 1` maps to flat log-potential `ε ≡ 0`. -/
 258theorem logPotentialOf_flat {n : ℕ} :
 259    logPotentialOf (fun (_ : Fin n) => (1 : ℝ)) = fun _ => (0 : ℝ) := by
 260  funext i
 261  unfold logPotentialOf
 262  exact Real.log_one
 263
 264/-! ## §5b. Coupling calibration: κ = 8 φ⁵ = κ_Einstein
 265
 266The constant `jcost_to_regge_factor := 8 · φ⁵` that appears in the bridge
 267identity is the *same* constant as `Constants.kappa_einstein` in RS-native
 268units. This is not a free normalization choice; it is forced by
 269`kappa_einstein_eq`, which derives `κ_Einstein = 8πG/c⁴ = 8 φ⁵` from the
 270RS-native definitions `G = λ_rec² c³ / (π ℏ)`, `ℏ = φ⁻⁵`, `λ_rec = c = 1`.
 271
 272We record this as an equational theorem so that downstream modules can
 273substitute one for the other. -/
 274
 275/-- **THEOREM.** The J-cost to Regge normalization factor equals
 276    `Constants.kappa_einstein` in RS-native units. Both evaluate to
 277    `8 · φ⁵`; the identity is that `phi ^ (5 : ℕ) = phi ^ (5 : ℝ)`
 278    via `Real.rpow_natCast`. -/
 279theorem jcost_to_regge_factor_eq_kappa_einstein :
 280    jcost_to_regge_factor = Constants.kappa_einstein := by
 281  rw [jcost_to_regge_factor_eq, Constants.kappa_einstein_eq]
 282  congr 1
 283  rw [show ((5 : ℝ)) = ((5 : ℕ) : ℝ) from by norm_num, Real.rpow_natCast]
 284
 285/-- **COROLLARY.** The bridge normalization and the Einstein gravitational
 286    coupling coincide. The paper's claim "κ is derived, not fitted" is
 287    this identification: the Regge-side normalization that makes the
 288    bridge theorem exact equals the Einstein coupling that appears in