pith. sign in
module module moderate

IndisputableMonolith.Relativity.Geometry.DiscreteBridge

show as:
view Lean formalization →

DiscreteBridge defines lattice spacing for N sites in a box of side L and assembles the discrete-continuum bridge via FlatChain, WeakFieldBridge, and DiscreteContinuumBridge. Researchers connecting the RS forcing chain to relativistic geometry cite these constructions. The module supplies definitions plus short verification lemmas on the imported metric and curvature objects.

claimLattice spacing $a = L/N$. Flat chain condition and weak-field bridge hold under the RS-derived Minkowski metric. Discrete-continuum bridge certificate links lattice parameters to the continuum tensor.

background

The module belongs to the Relativity.Geometry stack inside Recognition Science, which derives spacetime from the forcing chain T0-T8. It imports Constants (defining the fundamental time quantum τ₀ = 1 tick), Derivatives (basis vectors e_μ), Curvature (Christoffel symbols), LeviCivitaTheorem (unique torsion-free metric-compatible connection on any pseudo-Riemannian manifold), and MetricUnification (RS-derived η identical to the IndisputableMonolith metric tensor via the chain RCL → J unique (T5) → J''(1)=1).

proof idea

This is a definition module, no proofs. It introduces latticeSpacing together with positivity, limit-to-zero, and bridge-certificate lemmas that rest directly on the imported metric unification and LeviCivita results.

why it matters in Recognition Science

The module is imported by IndisputableMonolith.Relativity.Geometry, the aggregator that re-exports all geometry components. It supplies the discrete-continuum link that places the RS forcing-chain landmarks (T5 J-uniqueness, T8 D=3) into the relativistic geometry setting.

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)