continuum_limit_certificate
plain-language theorem explainer
Master certificate that the discrete RS ledger continuum limit yields a Lorentzian manifold: signature (−+++), causal trichotomy, light cone at one voxel per tick, J-cost quadratic spatial metric, ADM flat equals Minkowski, lattice Laplacian → ∇², D = 3, and positive weak-field coupling. Gravity and foundations workers cite it as the zero-parameter discrete-to-spacetime bridge. Proof is a structure constructor wiring already-proved component lemmas.
Claim. There is a continuum-limit certificate whose fields hold simultaneously: the Minkowski form $s^2 = -t^2 + x^2 + y^2 + z^2$ has temporal sign negative and spatial signs positive; every displacement is exactly timelike, spacelike, or lightlike; the light cone enforces unit speed; $J$-cost is quadratic to leading order with normalized scale and spatial isotropy; ADM with unit lapse and identity spatial metric recovers Minkowski; the lattice Laplacian converges as spacing $a \to 0$; resolution is achievable; the weak-field flat limit and positive coupling hold; and spatial dimension is $3$.
background
This module builds the zero-parameter bridge from discrete Recognition Science ledger sites to a Lorentzian continuum. The chain runs J-cost lattice → quadratic cost → lattice Laplacian → continuous ∇² → Lorentzian interval → Minkowski flat limit → weak-field curved metric. Unlike the phenomenological ILG time-kernel, every geometric ingredient here is forced: signature by tick/voxel asymmetry, spatial metric by J''(1) = 1, c = ℓ₀/τ₀ by one voxel per tick, κ from ZeroParameterGravity, and D = 3 from DimensionForcing.
The Minkowski form on ℝ^{1,3} is s² = −t² + x² + y² + z². Causal predicates (timelike / spacelike / lightlike) are the sign of that form. Upstream, jcost_quadratic_leading gives |J_log ε − ε²/2| ≤ |ε|⁴/20 for |ε| < 1, the discrete-to-continuous bridge: quadratic lattice costs become Laplacians. continuum_limit_second_order supplies the standard C⁴ finite-difference bound: the second difference over a² equals f''(x) plus O(a²). ADM with lapse 1 and identity spatial metric collapses exactly to Minkowski.
ContinuumLimitCert packages Tier-1 forced Lorentzian signature, causal structure, light cone, J-metric, ADM flatness, Laplacian convergence, weak-field coupling, and dimension into one master record.
proof idea
Term-mode structure instance: each field of ContinuumLimitCert is filled by a named prior lemma. Signature fields use signature_temporal and the three spatial positivity lemmas. Causal structure is causal_trichotomy (trichotomy on the Minkowski form). Light cone is light_cone_speed_limit. Metric content is jcost_quadratic_leading, metric_normalization, and spatial_isotropy. Flat ADM is adm_is_minkowski. Laplacian convergence is a one-line unpack of continuum_limit_second_order: extract the error constant C and drop the nonnegativity witness. Remaining fields are resolution_achievable, weak_field_flat_limit, weak_field_coupling, ZeroParameterGravity.kappa_pos, and spatial_dim_is_3. No new analysis; pure assembly.
why it matters
This is the module's master certificate: the foundational (not phenomenological) claim that N → ∞ ledger dynamics produce Lorentzian spacetime with forced signature, c = 1, J-derived spatial metric, and D = 3. It closes the architecture list in the module doc (items 1–10) and feeds the Foundation-level F-014 continuum-limit certificate, which records quadratic J, CPT, vacuum, Laplacian limit, and Klein-Gordon continuum dynamics.
Framework landmarks: T5 J-uniqueness supplies the cost whose second derivative at 1 normalizes the spatial metric; T8 forces D = 3 (spatial_dim_is_3); the eight-tick octave and voxel/tick asymmetry force the light-cone speed limit. Coupling positivity comes from the derived κ = 8φ⁵ in ZeroParameterGravity. Downstream consumers treat the certificate as a single hypothesis bundle rather than re-proving signature, causality, and Laplacian convergence separately. Open curved strong-field Einstein recovery sits after this flat and weak-field base.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.