Mixed Derivative Bounds for Bordered Regularity in a Lorentzian Simplicial Model
We construct complete mixed-derivative enclosures for a fixed boundary-capped Lorentzian simplicial action and apply them to regularity around two identified nonzero stationary endpoints. The source retains nine four-simplices, eighteen independently varied Lorentz links, moving boundary returns, and all 114 stationary equations. A two-family arithmetic bounds D_N^2 D_Y A and D_N D_Y^2 A in arbitrary independent complex directions. Factorial-normalized product rules, ordered matrix operations and complete infinite matrix-function tails give the operators required by the augmented border and normal residual. A separately arranged unnormalized implementation supplies a second complete enclosure of the same source; the two implementations share the physical graph and primitive value disks. At the actual endpoints d = 48τ, with τ = 2^-61, the operator bounds are L_B < 7,310,587 and L_F < 14,897,632,321. On the fixed radius-384τ neighborhood, the unchanged main inverse ceiling β_D = 169984/1799 gives an augmented-border defect q < 1.15036 × 10^-7, whereas the preceding unrestricted sufficient estimate gives 1992/1799 > 1. Complete residual and parameter bounds yield an off-shell regular chart with positive reach 432τ and uniform augmented inverse below 94.488060. The inherited regular-chart construction is refined by the mixed-operator enclosure and complete source application. The supporting stationary chain through 5τ, 6τ and 48τ is documented separately. Stationary coverage remains 48τ; the latest interval [3τ, 48τ] uses the exact predictor anchored at 6τ, with unchanged normalized error below 8.345679 × 10^-18. Boundary t is not physical time. Source semantics, analytic membership and runtime enclosure responsibilities remain explicit. Historical numerical executions and certificate replays support these conditional conclusions. Accepted returned Lean 4.19.0 evidence covers a supporting subset of 81 theorems and 42 definitions, with complete readable type/axiom reports for all 123 declarations and five intended negative-control failures. This does not establish end-to-end formalization of the physical source, runtime enclosures or full analytic existence argument. A consolidated review in a separate AI session supports the declared scope; its required editorial correction was closed in the internal v0.2 manuscript. The four attachments are the 30-page manuscript PDF, editable LaTeX, numerical supplement and formal supplement. The supplements preserve scientific and proof content and provide identified documentary distribution copies with original/public hash ledgers. This publication preparation changes no mathematical claim and performs no new source evaluation, certificate replay or Lean execution. Author-owned text, documentation and mathematical data use CC BY 4.0; author-owned software uses MIT, with more-specific and third-party notices preserved.
Authors
- Qingchun Zhang (ORCID: https://orcid.org/0009-0008-0389-1474)
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2026-10-29
- DOI
- https://doi.org/10.5281/zenodo.23778077
- Primary Topic
- Relativity and Gravitational Theory
- Type
- preprint