WeakFieldData
plain-language theorem explainer
Packages a C⁴ real scalar field h with uniform bound strictly below 1, so the factor 1+h stays positive. Anyone proving weak-field Regge-to-Einstein convergence, lattice Laplacian limits, or existence of refined cubic lattices cites this as geometric input. Pure structure definition: no proof body.
Claim. A weak-field datum is a function $h:\mathbb{R}\to\mathbb{R}$ of class $C^4$, together with a real bound $b$ satisfying $0<b<1$ and $|h(x)|\le b$ for every $x$, ensuring the perturbed metric factor $1+h$ remains strictly positive.
background
The module packages the deformed-cubic-lattice / curved-manifold correspondence in the linearized regime: given a smooth weak metric perturbation, a sequence of cubic lattices with spacing $a_N\to 0$ has prescribed edge lengths $L_e=a\sqrt{1+h(x_e)}$ whose Regge action and equations converge to the linearized Einstein–Hilbert action and vacuum EFE.
The geometric input is a 1D representative field $h$ along one axis (the full 3D case is componentwise via the three-term lattice Laplacian). Smoothness is $C^4$ so second derivatives and $O(a^2)$ finite-difference remainders are controlled. The bound $0<b<1$ with $|h|\le b$ forces $1-b\le 1+h\le 1+b<2$, keeping the metric Riemannian (or weak-field Lorentzian) and edge lengths real and positive.
Upstream smoothness abbreviations from the Aczél/cost development supply the $C^\infty$ vocabulary; positivity conventions from the primitive recognition calculus and Bremermann bound appear only as shared naming patterns for the bound fields.
proof idea
No proof: this is a structure declaration. Fields are the perturbation $h$, a ContDiff ℝ 4 witness, a numeric bound, and the three inequalities $b>0$, $b<1$, and pointwise $|h|\le b$. Downstream lemmas read these fields directly (e.g. W.h, W.smooth, W.h_bounded).
why it matters
This is the geometric input type for the unified lattice–manifold certificate. Downstream, latticeLaplacian_to_continuum and discreteRegge_to_linearizedEFE take a weak-field datum and prove that the scaled lattice Laplacian converges at $O(a^2)$ to $\nabla^2 h$, so discrete Regge EL equations imply the linearized vacuum EFE in harmonic gauge. exists_lattice_refinement_for_weak_field quantifies over every such datum and box length $L>0$ to produce a refinement and a full correspondence certificate (prescribed edges, action error $O(a^2)$, coupling identity $\kappa_{\mathrm{Regge}}=8\varphi^5=\kappa_{\mathrm{Einstein}}$).
Sibling lemmas one_plus_h_pos and one_plus_h_lt_two discharge positivity and upper bounds used by prescribedEdgeLength. The same type appears in the forcing-chain bridge T5Regge_To_ContinuumLimit_Bridge, linking J-cost uniqueness (T5) through nonlinear Regge to continuum completion. Regime is strictly weak-field ($|h|\ll 1$): solar-system, galactic, GW, and cosmological perturbation physics; nonlinear $|h|\sim O(1)$ is a separate conditional certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.