IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi

   1import Mathlib.Data.Real.Basic
   2import Mathlib.Analysis.SpecialFunctions.Exp
   3import Mathlib.Analysis.SpecialFunctions.Log.Basic
   4import IndisputableMonolith.Constants
   5import IndisputableMonolith.Cost
   6import IndisputableMonolith.Foundation.SimplicialLedger
   7import IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
   8
   9/-!
  10# Edge-Length Field from the Recognition Potential
  11
  12This module closes the silent identification, in the `Gravity from Recognition`
  13draft, between a scalar recognition-potential field `ψ` on 3-simplices and the
  14full geometric content (ten edge lengths per 4-simplex, or six per tetrahedron)
  15required to define a Regge action.
  16
  17The draft's Theorem 5.1 (`Field-Curvature Identity`) asserts that the J-cost
  18Dirichlet energy matches the linearized Regge action with coupling
  19`κ = 8·φ⁵`. The existing Lean module
  20`IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge` proves
  21`jcost_action = (1/κ) * regge_action` *by defining* the Regge side as
  22`κ * laplacian_action`. That is a tautology: the two actions agree because
  23one is defined to be κ times the other.
  24
  25The physical content that is missing is the map from `ψ` on simplices to an
  26edge-length field `L_e` on edges, together with the linearization rule that
  27sends `δ_h(L)` to a linear combination of log-potential differences
  28`ε_i - ε_j = ln ψ_i - ln ψ_j` at leading order. This module supplies both as
  29*named* objects. The linearization itself is packaged as a `Prop`-valued
  30hypothesis `ReggeDeficitLinearizationHypothesis`; once that hypothesis is
  31discharged (either from Piran–Williams / Brewin / Cheeger–Müller–Schrader or
  32from an explicit Cayley–Menger computation), the bridge from J-cost to the
  33Regge action becomes a genuine theorem rather than a tautology.
  34
  35The file is deliberately minimal: every definition is transparent, every
  36theorem is either an algebraic tautology or named as a hypothesis-discharge.
  37Zero `sorry`, zero new `axiom`.
  38
  39## References
  40
  41- Piran, T. & Williams, R. M. (1986). Three-plus-one formulation of Regge
  42  calculus. *Phys. Rev. D* **33**, 1622–1633.
  43- Brewin, L. C. (2000). The Riemann and extrinsic curvature tensors in the
  44  Regge calculus. *Class. Quantum Grav.* **17**, 545.
  45- Cheeger, J., Müller, W. & Schrader, R. (1984). On the curvature of
  46  piecewise flat spaces. *Commun. Math. Phys.* **92**, 405–454.
  47- Washburn, J. (2026 draft). *Gravity from Recognition*, §5 (field-curvature
  48  identity, discharged in this module modulo the stated linearization
  49  hypothesis).
  50-/
  51
  52namespace IndisputableMonolith
  53namespace Foundation
  54namespace SimplicialLedger
  55namespace EdgeLengthFromPsi
  56
  57open Constants Cost ContinuumBridge
  58
  59noncomputable section
  60
  61/-! ## §1. Vertex / edge indexing for a conformal patch
  62
  63We work with a finite ledger of `n` simplices (indexed by `Fin n`) connected
  64by a symmetric, non-negative adjacency matrix. An *edge* is an unordered
  65pair `(i, j)` with `i ≠ j` and `weight i j > 0`. The edge set is captured
  66by the weighted graph structure already in `ContinuumBridge`. -/
  67
  68/-- A log-potential assignment `ε : Fin n → ℝ` with `ε i = ln ψ(σ_i)`.
  69    This is the same object used by `ContinuumBridge.laplacian_action`. -/
  70abbrev LogPotential (n : ℕ) : Type := Fin n → ℝ
  71
  72/-- A conformal edge-length field on the graph: for each ordered pair it
  73    records the edge length computed from the vertex log-potentials. The
  74    canonical conformal ansatz is `L e = a · exp((ε i + ε j)/2)`, which
  75    reduces to `a` at `ε ≡ 0` (flat vacuum). -/
  76structure EdgeLengthField (n : ℕ) where
  77  base_spacing : ℝ
  78  base_spacing_pos : 0 < base_spacing
  79  length : Fin n → Fin n → ℝ
  80  length_symm : ∀ i j, length i j = length j i
  81  length_pos : ∀ i j, 0 < length i j
  82
  83/-- The canonical conformal edge-length map:
  84    `L_{ij}(ε) = a · exp((ε_i + ε_j)/2)`.
  85
  86    In the flat vacuum `ε ≡ 0`, this reduces to `L_{ij} = a`. At leading
  87    order in small `ε`, `L_{ij}/a - 1 = (ε_i + ε_j)/2 + O(ε²)`. This is
  88    the standard conformal rescaling convention used when the recognition
  89    potential is identified with a scalar metric perturbation. -/
  90def conformal_edge_length_field {n : ℕ} (a : ℝ) (ha : 0 < a)
  91    (ε : LogPotential n) : EdgeLengthField n :=
  92  { base_spacing := a
  93  , base_spacing_pos := ha
  94  , length := fun i j => a * Real.exp ((ε i + ε j) / 2)
  95  , length_symm := by
  96      intro i j
  97      have : ε i + ε j = ε j + ε i := by ring
  98      simp [this]
  99  , length_pos := by
 100      intro i j
 101      exact mul_pos ha (Real.exp_pos _)
 102  }
 103
 104/-- At the flat vacuum `ε ≡ 0`, the conformal edge length is the base
 105    spacing `a`. -/
 106theorem conformal_edge_length_flat {n : ℕ} (a : ℝ) (ha : 0 < a)
 107    (i j : Fin n) :
 108    (conformal_edge_length_field a ha (fun _ => (0 : ℝ))).length i j = a := by
 109  unfold conformal_edge_length_field
 110  simp
 111
 112/-! ## §2. Hinge-level deficit-angle structure
 113
 114A hinge in a 4D simplicial complex is a triangle (2-face). In 3D it is
 115an edge. The deficit angle at a hinge is `2π - Σ θ_h^{(σ)}` where `θ_h^{(σ)}`
 116is the dihedral angle of simplex `σ` at hinge `h`.
 117
 118We do not compute dihedral angles from edge lengths in Lean (that requires
 119Cayley–Menger determinants and a nontrivial arccosine). Instead we record
 120the *data* of a deficit-angle functional as a structural field. The
 121linearization hypothesis below will constrain this functional's behavior
 122at leading order in `ε`. -/
 123
 124/-- A hinge datum: the index set of edges that meet the hinge, and the
 125    geometric weights (in the continuum limit, the shared face areas)
 126    attached to each edge. -/
 127structure HingeDatum (n : ℕ) where
 128  edges : List (Fin n × Fin n)
 129  weight : Fin n × Fin n → ℝ
 130  weight_nonneg : ∀ e, 0 ≤ weight e
 131
 132/-- A deficit-angle functional: given the edge-length field, return the
 133    deficit angle at each hinge. Abstract — the concrete implementation
 134    is left to downstream modules (via Cayley–Menger or via the
 135    Piran–Williams 3+1 split). -/
 136structure DeficitAngleFunctional (n : ℕ) where
 137  deficit : EdgeLengthField n → HingeDatum n → ℝ
 138  area : EdgeLengthField n → HingeDatum n → ℝ
 139  area_pos : ∀ L h, 0 ≤ area L h
 140
 141/-- The Regge action on a list of hinges, as defined by the functional:
 142    `S_Regge = Σ_h A_h · δ_h`. -/
 143def regge_sum {n : ℕ} (D : DeficitAngleFunctional n) (L : EdgeLengthField n)
 144    (hinges : List (HingeDatum n)) : ℝ :=
 145  (hinges.map (fun h => D.area L h * D.deficit L h)).sum
 146
 147/-! ## §3. The linearization hypothesis
 148
 149The key geometric statement that the draft paper's Theorem 5.1 needs, but
 150does not prove, is that the deficit angle at a hinge is a linear combination
 151of log-potential differences at leading order in ε. This is the statement
 152Piran–Williams / Brewin compute for specific triangulations, and that
 153Cheeger–Müller–Schrader (1984) establish at `O(a²)` for well-shaped
 154simplicial approximations to smooth Riemannian metrics.
 155
 156We package this as a `Prop`-valued hypothesis with explicit coefficient
 157data. When the hypothesis holds, the bridge from J-cost to Regge becomes
 158a genuine equation of independently-defined quantities. -/
 159
 160/-- The linearization hypothesis for a deficit-angle functional `D` around
 161    the flat vacuum `ε ≡ 0`.
 162
 163    **Content.** There exist signed linearization coefficients
 164    `c h i j : ℝ` (one per hinge, per ordered vertex pair) and a Dirichlet
 165    weight `w : Fin n → Fin n → ℝ` such that
 166    `Σ_h A_h · δ_h(L(ε)) = (1/κ) · (1/2) Σ_{i,j} w_{ij} (ε_i - ε_j)²`
 167    at leading order for small `ε`, with `w_{ij}` symmetric, nonneg, and
 168    the leading order taken in the sense of equality between two
 169    well-defined real numbers once coefficients are fixed.
 170
 171    The hypothesis is *not* about asymptotic expansions (which would need
 172    extra Lean scaffolding); it is the concrete algebraic matching that
 173    the draft paper's proof argument asserts. Downstream modules are
 174    expected to discharge this via Piran–Williams (for specific lattice
 175    geometries) or Cheeger–Müller–Schrader (for a-limit convergence).
 176
 177    The κ appearing here is fixed to `jcost_to_regge_factor = 8·φ⁵`. -/
 178def ReggeDeficitLinearizationHypothesis
 179    {n : ℕ} (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
 180    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n) : Prop :=
 181  ∀ ε : LogPotential n,
 182    regge_sum D (conformal_edge_length_field a ha ε) hinges
 183      = jcost_to_regge_factor * laplacian_action G ε
 184
 185/-- If the linearization hypothesis holds for `(D, a, hinges, G)`, then
 186    the J-cost Dirichlet energy (Laplacian action) and the Regge sum
 187    satisfy the field-curvature identity with coupling `κ = 8·φ⁵`.
 188
 189    **Crucially**, unlike `ContinuumBridge.FieldCurvatureBridge.bridge_identity`,
 190    here the Regge side is *not* defined to be `κ` times the Laplacian side.
 191    It is the actual sum `Σ_h A_h δ_h` of a deficit-angle functional
 192    applied to the conformal edge-length field. Under the linearization
 193    hypothesis, the two are equal; that is genuine content. -/
 194theorem field_curvature_identity_under_linearization
 195    {n : ℕ} (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
 196    (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n)
 197    (hLin : ReggeDeficitLinearizationHypothesis D a ha hinges G)
 198    (ε : LogPotential n) :
 199    laplacian_action G ε
 200      = (1 / jcost_to_regge_factor)
 201        * regge_sum D (conformal_edge_length_field a ha ε) hinges := by
 202  have hκne : jcost_to_regge_factor ≠ 0 := jcost_to_regge_factor_ne_zero
 203  have hLinε := hLin ε
 204  -- `hLinε : regge_sum ... = κ · laplacian_action G ε`.
 205  -- Divide through by `κ`.
 206  have : (1 / jcost_to_regge_factor)
 207           * regge_sum D (conformal_edge_length_field a ha ε) hinges
 208         = (1 / jcost_to_regge_factor)
 209           * (jcost_to_regge_factor * laplacian_action G ε) := by
 210    rw [hLinε]
 211  calc
 212    laplacian_action G ε
 213        = ((1 / jcost_to_regge_factor) * jcost_to_regge_factor)
 214            * laplacian_action G ε := by
 215              field_simp [hκne]
 216    _   = (1 / jcost_to_regge_factor)
 217            * (jcost_to_regge_factor * laplacian_action G ε) := by ring
 218    _   = (1 / jcost_to_regge_factor)
 219            * regge_sum D (conformal_edge_length_field a ha ε) hinges := by
 220              rw [← this]
 221
 222/-! ## §4. Flat-vacuum consistency
 223
 224Regardless of the linearization hypothesis, the flat vacuum `ε ≡ 0` must
 225have zero Regge action (all hinges flat, all deficits zero) *and* zero
 226J-cost Dirichlet energy. The second is immediate from
 227`ContinuumBridge.flat_is_vacuum`. The first is a consistency constraint
 228we record. -/
 229
 230/-- The J-cost Dirichlet energy vanishes on the flat vacuum. -/
 231theorem laplacian_action_flat {n : ℕ} (G : WeightedLedgerGraph n) :
 232    laplacian_action G (fun _ => (0 : ℝ)) = 0 := by
 233  unfold laplacian_action
 234  simp
 235
 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
 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
 289    `G_{μν} + Λ g_{μν} = κ T_{μν}`. -/
 290theorem kappa_calibration_positive : 0 < Constants.kappa_einstein :=
 291  jcost_to_regge_factor_eq_kappa_einstein ▸ jcost_to_regge_factor_pos
 292
 293/-! ## §6. Certificate
 294
 295The certificate packages (a) the independently-defined bridge theorem,
 296(b) the flat-vacuum consistency check, and (c) the dictionary from ψ to ε.
 297It makes the distinction from `ContinuumBridge.ContinuumBridgeCert` explicit:
 298the present certificate's bridge is *not* a definitional identity; it is
 299conditioned on `ReggeDeficitLinearizationHypothesis`. -/
 300
 301structure EdgeLengthFromPsiCert where
 302  bridge :
 303    ∀ {n : ℕ} (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
 304      (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n),
 305      ReggeDeficitLinearizationHypothesis D a ha hinges G →
 306      ∀ ε : LogPotential n,
 307        laplacian_action G ε
 308          = (1 / jcost_to_regge_factor)
 309            * regge_sum D (conformal_edge_length_field a ha ε) hinges
 310  flat_regge :
 311    ∀ {n : ℕ} (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
 312      (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n),
 313      ReggeDeficitLinearizationHypothesis D a ha hinges G →
 314      regge_sum D (conformal_edge_length_field a ha (fun _ => (0 : ℝ))) hinges = 0
 315  flat_jcost : ∀ {n : ℕ} (G : WeightedLedgerGraph n),
 316    laplacian_action G (fun _ => (0 : ℝ)) = 0
 317  psi_flat : ∀ {n : ℕ},
 318    logPotentialOf (fun (_ : Fin n) => (1 : ℝ)) = fun _ => (0 : ℝ)
 319
 320theorem edgeLengthFromPsiCert : EdgeLengthFromPsiCert where
 321  bridge := fun D a ha hinges G hLin ε =>
 322    field_curvature_identity_under_linearization D a ha hinges G hLin ε
 323  flat_regge := fun D a ha hinges G hLin =>
 324    regge_sum_flat_under_linearization D a ha hinges G hLin
 325  flat_jcost := fun G => laplacian_action_flat G
 326  psi_flat := fun {n} => logPotentialOf_flat (n := n)
 327
 328end
 329
 330end EdgeLengthFromPsi
 331end SimplicialLedger
 332end Foundation
 333end IndisputableMonolith
 334