`is`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
domain: Foundation
line: 36 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi on GitHub at line 36.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

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

papers checked against this theorem

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