pith. sign in
module module high

IndisputableMonolith.Relativity.Geometry.DiscreteBridge

show as:
view Lean formalization →

DiscreteBridge defines lattice spacing a = L/N for N sites in a box of side L and assembles the discrete-to-continuum bridge structures. Workers on lattice models in recognition science cite it when linking the phi-ladder to Minkowski geometry. The module is built from sibling definitions and short lemmas that import curvature, metric unification, and Levi-Civita results.

claimLattice spacing is $a = L/N$ for $N$ sites in a box of side $L$. The module supplies the flat chain condition, weak-field bridge, coupling from phi, and the discrete-continuum bridge certificate.

background

The module imports the RS time quantum τ₀ = 1 tick from Constants, basis vectors e_μ from Derivatives, Christoffel symbols from Curvature, and the fundamental theorem of pseudo-Riemannian geometry from LeviCivitaTheorem: on any pseudo-Riemannian manifold (M, g) there exists a unique torsion-free, metric-compatible connection. It further imports MetricUnification, which proves the Minkowski metric derived from the RS forcing chain (RCL → J unique (T5)) is identical to the stack's eta. The setting is the discrete bridge inside the relativity geometry stack.

proof idea

This is a definition module, no proofs. It introduces latticeSpacing and its positivity and zero-limit lemmas, then defines FlatChain, WeakFieldBridge, coupling_from_phi, metric_matrix_invertible_at, ReggeConvergenceHypothesis, DiscreteContinuumBridge, bridge_certificate, and EndToEndChain.

why it matters in Recognition Science

The module feeds the parent Geometry aggregator, which re-exports all geometry components for convenient importing. It supplies the discrete-continuum bridge that connects the RS forcing chain (T5 J-uniqueness, T8 D = 3) to the metric tensor via lattice spacing and the Regge hypothesis.

scope and limits

used by (1)

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

depends on (8)

Lean names referenced from this declaration's body.

declarations in this module (13)