pith. machine review for the scientific record. sign in
theorem scaffolding sorry stub

is

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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`. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (36)

Lean names referenced from this declaration's body.

… and 6 more