258theorem logPotentialOf_flat {n : ℕ} : 259 logPotentialOf (fun (_ : Fin n) => (1 : ℝ)) = fun _ => (0 : ℝ) := by
proof body
Term-mode proof.
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`. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.