 236/-- If the linearization hypothesis holds, the Regge sum also vanishes
 237    on the flat vacuum. This is a nontrivial *consistency check* on
 238    any discharge of the hypothesis — it pins down the overall constant. -/
 239theorem regge_sum_flat_under_linearization
 240    {n : ℕ} (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
 241    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n)
 242    (hLin : ReggeDeficitLinearizationHypothesis D a ha hinges G) :
 243    regge_sum D (conformal_edge_length_field a ha (fun _ => (0 : ℝ))) hinges = 0 := by
 244  have h := hLin (fun _ => (0 : ℝ))
 245  rw [h, laplacian_action_flat]
 246  ring
 247
 248/-! ## §5. The recognition-potential dictionary
 249
 250A thin convenience: the map from `ψ : Fin n → ℝ₊` to `ε : Fin n → ℝ` via
 251the logarithm, with the property that flat `ψ ≡ 1` gives flat `ε ≡ 0`. -/
 252
 253/-- Log-potential from a strictly positive recognition-potential assignment. -/
 254def logPotentialOf {n : ℕ} (ψ : Fin n → ℝ) : LogPotential n :=
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.