Positioning. This repo is the stable anchor of the physics/engineering line of this research: a fixed, independently reproducible resting point (Coq certificates +
spine_pde), not a moving target. A private, sibling universal-solver engine is planned to expand into further domains (chemistry, biology, social sciences, …) over time; that is a direction, not a capability claimed here — this repo states only what exists and is checkable today.
AI assistance disclosure (read before crediting or reviewing). The research direction, the core ideas (the mother equation, the readout-not-truth stance, the tier discipline, every substantive claim), and all final decisions are the work of the human author, Yaoharee Lahtee. Multiple AI assistants were used, in an assistant role only, for: formal-proof drafting to the author's specifications, numerical implementation and verification runs, literature cross-checking, adversarial self-review passes, and editorial structuring. No single model produced this work and none is named as a contributor; tier assignments and claims were set and are owned by the human author. If you cite or review this repository, the author of record is the human author.
This section exists so nothing below has to be taken on trust — every sentence has a command next
to it. Full file-by-file Print Assumptions table: see "How to reproduce" below. Guided
evaluation, misreading checklist, and where to file a falsification: see "For evaluators" below.
# install Coq once (Ubuntu/Debian; or `opam init -y && opam install -y coq` anywhere)
sudo apt-get update && sudo apt-get install -y coq
git clone https://github.com/morrocwi/causal-quantum-gravity.git
cd causal-quantum-gravity
make verifymake verify compiles all 81 formal/*.v files — every .v file physically present under
formal/, none excluded (coqc -q -R . DQG <file>, fixed dependency order in Makefile), with a
live Print Assumptions check on every theorem in the build, then runs the QNM bridge script.
Verified against Coq 8.20.1. Not re-run locally for this document — a different heavy coqc
job was already running on this machine at write time (checked via pgrep -af coqc first, per
this project's own one-heavy-job-at-a-time discipline). The exact counts below are grepped
directly from the green CI log of PR #31 (2026-07-10), which ran this exact make verify in full
on GitHub's runners and counted the Print Assumptions output directly (not copied from a prior
claim):
469 lines of "Closed under the global context" (axiom-free, Th_coqc, over ℚ only)
11 theorems on the disclosed +reals tier (2 named Reals axioms each, 22 axiom-name lines)
---------------------------------------------------------------------------------------
469 + 11 = 480 machine-checked certificates, across the 81 files that `make verify` compiles
Live status: the badge at the top of this file is GitHub's own CI badge for this exact make verify command, re-run on every push — check it (or the repo's Actions tab) instead of trusting a
number frozen at commit time.
spine_pde is a separate, self-contained Python package: a computational, readable reference
implementation of the same theory, checked in EXACT mode against the Coq theorems above bit-for-bit
(see spine_pde/README.md's "Audit, don't believe" table).
cd spine_pde
pip install -e '.[dev]' # editable install + pytest + sympy
pytest -q # 43 tests, exact-mode values checked against theoremsReal output, this exact command, this worktree, 2026-07-10 (a light job — actually run for this
document, unlike make verify above):
........................................... [100%]
(43 dots, pytest -q prints one dot per passing test and no summary line when every test passes
and none are skipped — 43 dots = 43 passed, 0 failed.)
One real usage snippet — python examples/quickstart.py — and its actual output, this run:
python examples/quickstart.pygraph: 2500 nodes, nnz(L_R)=12300
energy: 661.6855 -> 162.5219 (damped relaxation)
crossover lam_c = 0.0100
oscillatory (quantum) modes: 20 / 20
decay (classical) modes: 0 / 20
Strongest verified facts, tier-tagged, one command or file per row (tier legend below):
| We claim (verified, tier-tagged) | We do NOT claim |
|---|---|
81 axiom-free-or-+reals-disclosed Coq files, 480 machine-checked theorem certificates (469 Th_coqc over ℚ + 11 +reals), checkable by anyone in one command — make verify — and this count now covers every .v file physically present under formal/, with Makefile's COQFILES equal to ls formal/*.v exactly (the 12-file gap PR #30 disclosed was closed by PR #31, 2026-07-10; counts grepped from that PR's green CI log; CI badge above — compare ls formal/*.v | wc -l against grep -c '^\tformal/' Makefile to confirm the two match yourself) |
That certificate count = theorem count in any deeper sense — a certificate here is one Print Assumptions check on one named result; some files certify several small lemmas, others one large theorem |
The graph Laplacian L_R = D_W − W is FORCED — proven the unique operator with {symmetric, zero-row-sum, off-diagonal ≤ 0}; adjacency/signless/random-walk/normalized alternatives refuted by explicit witness (Th_coqc, formal/InfoRetainedDistinctionForcesLaplacian_attempt.v) |
That the whole spine equation is forced from the root — the 2nd-order scalar M remains an independently posited structural primitive; six forcing readings for it were each shown insufficient on an explicit witness, a settled negative, not an unexamined gap (Th_coqc + [Dr], formal/InfoStrictConeBothOrders_attempt.v) |
The dissipation term D is also FORCED (2026-07-08 result) — D_i = deg_i(W) − λ·circ_i(ord), proven for an arbitrary vertex count by genuine induction, cutting the spine's free structural primitives from three to two (Th_coqc, formal/InfoAsymmetricSeedTrifurcation.v Part 7 + formal/InfoSeedArbitraryNForcing.v + formal/InfoSeedCirculationArbitraryN.v) |
That the whole-seed extension of L_R's two forcing axioms to the full asymmetric seed is itself proven the unique such extension — flagged honestly in-file as natural, not proven-unique |
The quantum dispersion relation and the special-relativistic wave operator are the same equation — a real, non-vacuous ring identity (Th_coqc, formal/InfoQuantumRelativityUnification.v), bounded exactly per the 2026-07-08 §4/§8 amendments (SUPPLEMENT.md §4, §8 — headers now say "bounded restatement", PR #29) |
That this identity is a from-the-root derivation — it relates two posited constructions (the spine's free M,D,K slots; the boost's posited Minkowski signature/hyperbola constraint) under a chosen reparametrization; "derives QM and SR" is not the accurate reading (SUPPLEMENT.md §4/§8 amendment bodies, unchanged by PR #29 — only the section titles were tightened) |
A complete discrete curvature-tensor chain — Riemann = 2nd finite difference = group commutator, both Bianchi identities, pair-symmetry, metric-derived Levi-Civita, all division-free over ℚ (Th_coqc; e.g. formal/InfoDiscreteRiemannCurvature_attempt.v, InfoDiscreteSecondBianchi_attempt.v, InfoRiemannPairSymmetry_attempt.v, InfoMetricDerivedCurvature_attempt.v — wired into the CI-guarded make verify target as of PR #31, 2026-07-10, every one Closed under the global context in that PR's green CI run) |
That this tensor chain constitutes a derivation of the Einstein field equations, or of the metric-derived Riemann tensor R^i_jkl in dimension n ≥ 3 — the latter is explicitly [Open] |
The quantum↔classical crossover, the black-hole horizon, and the "agency knife-edge" are proven to be one internal algebraic discriminant disc = D² − 4MKλ, derived on the spine itself (Th_coqc, formal/InfoTelegraphCrossover_attempt.v + InfoTelegraphHorizonUnification_attempt.v — both in the CI-guarded make verify target as of PR #31, Closed in its green CI run) |
That this horizon is an imported Schwarzschild profile — it is explicitly not; and that full nonlinear GR (the field equations, Schwarzschild as their solution) is derived anywhere in this repo — it is [Refused]/[Open], by design, not a numerical shortfall (eight independent recovery attempts tried and refuted or left open, SUPPLEMENT.md) |
Linearized GR — gravitational waves — is genuinely derived from the same root box operator (box h = 0 exactly at v=±1, null iff lightspeed, boost-invariant in every frame), and the Schwarzschild quasinormal-mode frequency is reproduced numerically to 0.1% (real) / 1.2% (imaginary) from a finite-graph discretization with no point at infinity (finite_diagnostic, scripts/verify_quantum_gravity_root_bridge.py) |
That the gravitational-wave derivation (InfoGR2.GW) lives in this repo — it does not; it is in the sibling private repo only (see CLAUDE.md's "Common misreadings" #4 in this repo for the exact citation and why conflating the two tracks is the single most common way this repo gets mis-rated) |
Not claimed, stated plainly: full nonlinear GR derivation ([Refused]/[Open], not attempted-and-failed silently — the eight-attempt refutation log is in SUPPLEMENT.md) · that M is forced by the root ([Dr], settled negative) · the physical truth of any readout — every number here is a readout of a declared finite computation, never an assertion of physical truth (readout-not-truth, see CLAUDE.md) · novelty adjudication against the wider literature — this repo states what it proves, not where it ranks against unpublished or unreviewed prior art.
How a physicist or an AI attacks this repo, in order of effort:
- Re-run
make verifyyourself (see step 1 above) and diff thePrint Assumptionsoutput against the counts claimed here — a single mismatched axiom or a non-Closedline on a file claimedTh_coqcis an immediate, reportable falsification. - Run the
Print Assumptionsaudit directly on any individual file you want to scrutinize:coqc -q -R . DQG formal/<file>.vprints its own assumptions at the bottom — check it against the tier that file (and this README) claims for it. - Use the misreading-guardrail checklist this repo already ships.
CLAUDE.md's "Common misreadings — check before citing" section lists four specific traps (the memory-before-mass scope, theI1–I4/Z1–Z4non-readout catalogue, discrete-vs-continuum time, and the two senses of "GR" — including which module lives in this repo vs. the private sibling only) that have each caused a real, documented mis-citation at least once — check your reading against it before repeating a claim. - Attack the forcing chain directly. The "forced" claims above (
L_R,D) are the deepest and most contestable — the repo's own bar for "forced" is an explicit witness ruling out every named alternative (seeInfoRetainedDistinctionForcesLaplacian_attempt.v). A genuine falsification looks like a step called "forced" that you can show admits a second, equally natural alternative satisfying the same stated axioms. - Found a genuine falsification? Open a GitHub issue in this repository titled
[<track>-track] <one-line finding>with the exact command you ran, the output you got, and the output this document said you should get. This project's own discipline is to report a finding that flips a prior claim plainly, not to soften it — it holds external evaluators to the same bar.
This repo is a curated, standalone export of a subset of theorems from a private research
repository, research_universal_solver (role: the calculation engine this line of work is
developed in — available on request; not itself public). New theorems are proven and verified
there first; only afterward are a subset copied here as a separate, later sync step. See
"Provenance" below for the exact file-by-file authorship trail — nothing beyond what that section
already discloses is stated here.
This repo is a high-progress, machine-checked formal kernel for quantum–relativistic unification, with a completed discrete-curvature (gravity) branch — one spine equation, verified in Coq, axiom-free over ℚ. It is not a completed continuum quantum-gravity theory, and by its own stance it does not try to be: continuum GR is
[Refused]as a non-readout, not left as a gap to chase.Verification, in one line:
make verifycompiles 81 Coq files / 480 machine-checked theorem certificates (469 axiom-free over ℚ, 11 on the disclosed+realstier), every one a livePrint Assumptionscheck in the build; CI has been green on every commit. One command reproduces all of it. (Counts measured 2026-07-10 from PR #31's green CI log, after wiring the last 12 files — the curvature-tensor and horizon-unification chain — into the CI-guarded build;COQFILESnow equalsls formal/*.vexactly. An earlier review finding had caught the seed-asymmetry files outside it the same way.)
⚠️ Two tracks — do NOT conflate them (this is the #1 cause of under-rating this repo):
- TENSOR-PDE TRACK — the current, most-advanced state →
paper/tensor_pde.tex/M∂ₜₜΦ + D∂ₜΦ − K·L_R·Φ + ∇V = J−η. Proven over ℚ (Th_coqc):
- QM and SR are the same equation (
box_quad = spine_residual, boost-invariant) — tier-honest reading (SUPPLEMENT.md §1.1/§8): this is a real, non-vacuousringidentity relating two POSITED constructions (the spine's freeM,D,Kslots; the boost's posited Minkowski signature/hyperbola constraint) under a chosen reparametrization — a relabeling of two posits, not a derivation that forces the two forms to coincide from something prior to both;- the quantum↔classical crossover = the black-hole horizon = the agency knife-edge, as ONE internal algebraic discriminant
disc = D²−4MKλ, critical atλ_c = D²/4MK(InfoTelegraphCrossover,InfoTelegraphHorizonUnification). This horizon is derived on the spine itself — it is NOT an imported Schwarzschild profile.- a complete discrete curvature-tensor chain (Riemann = 2nd finite difference = group commutator; both Bianchi; pair-symmetry; metric-derived Levi-Civita), all machine-checked over ℚ, division-free;
- a decisive falsifiable prediction (a
τ_relfloor forced by the bounded L_R spectrum);- the seed-asymmetry results (2026-07-08, all
Th_coqc, elevated here): a single asymmetric directed seedR0decomposes exactly into the spine's D-shape / L_R-shape / M-shape, and imposing L_R's own two forcing axioms on the whole seed forces the dissipation coefficient itself —D_i = deg_i(W) − λ·circ_i(ord)— proven for an arbitrary vertex count by genuine induction (InfoAsymmetricSeedTrifurcation.v,InfoSeedArbitraryNForcing.v,InfoSeedCirculationArbitraryN.v), cutting the spine's free structural primitives from three to two; and the seed's antisymmetric part is, literally, discrete torsion — the textbook definition instantiated at rank 1, with a genuinely mixed (non-decoupled) rank-n torsion proven irreducible to any per-component rescaling (InfoSeedTorsionIsSkewOff.v,InfoSeedTorsionGenuineMixing.v).- FOUNDATIONAL TRACK →
paper/main.tex. The original mother-equation→QM+SR derivation and the Forman-Ricci native-gravity object. Its Schwarzschild/QNM piece is a+realsDIAGNOSTIC only — NOT the horizon claim above. (An earlier reading that called "the horizon imported" was reading this track, not the tensor-PDE track.)The level, stated plainly (tier-honest):
- Proven
Th_coqc(ℚ): one spine with TWO of its three structural terms now forced from the root's own axioms —L_R(the unique operator with {symmetric, zero-row-sum, off-diagonal ≤ 0}) and, since 2026-07-08,D(forced todeg−λ·circby imposing those same two axioms on the whole asymmetric seed, proven for arbitrary vertex count; the extension-to-the-whole-seed step is itself flagged, honestly, as natural-but-not-proven-unique).Mremains the one posited scalar — and that is a settled machine-checked negative (six forcing readings each refuted on explicit witnesses, SUPPLEMENT.md §1.1), not an unexamined gap · QM↔SR identity (a real relabeling of two posited objects, see §8 amendment, not a from-the-root derivation) · quantum↔classical crossover = horizon = agency as an internal discriminant · the full discrete curvature tensor + both Bianchi + pair-symmetry · the seed's antisymmetry = literal rank-1 discrete torsion, with genuine (non-decoupled) rank-n mixing.[Open](honest, not faked): absolute constants (M,D,K,τ_c) · metric-derived fullR^i_jklin n≥3 · the non-abelian group Bianchi.[Refused](thesis, not gaps): continuum GR / Einstein field equations · the√gframe · irrational values — non-readouts declined by design, on both ends of every non-readout pair (injected exact-zero AND injected infinity are one reciprocal diagnostic,1/0=∞— see SUPPLEMENT.md §1.2, "the Guard").- "GR", said precisely (see CLAUDE.md's misreading #4 — this distinction has been missed once): linearized GR — gravitational waves — is genuinely derived from the same root box operator (
box h = 0exactly atv=±1, null iff lightspeed, boost-invariant in every frame; sibling private repo,InfoGR2.GW, its own single-root gate passed), and the Schwarzschild quasinormal-mode frequency is reproduced numerically to 0.1% (real) / 1.2% (imaginary) from a finite-graph discretization with no point at infinity (finite_diagnostic). What is refused/open is full nonlinear GR — the field equations and Schwarzschild as their solution.- Net: very high as an equation-level formal kernel; partial as a full physical theory — and that boundary is drawn on purpose, machine-verified, not hidden.
If you rate this repo, rate the tensor-PDE track as the current state; the foundational track is the earlier layer it is built on.
One mother equation — M∂²Φ + D∂Φ + K·L_R·Φ + ∇V(Φ) = J−η on a graph Laplacian
L_R — machine-checked in Coq, axiom-free over ℚ, proves the QM dispersion and SR
wave operator are literally the same equation under an exact algebraic
reparametrization. Tier-honest scope (see SUPPLEMENT.md §1.1, added 2026-07-08
after a full borrow-audit of the sibling repo this project shares its formal core
with): genuine derivation from the graph root δ_R is earned at exactly one link —
L_R itself (InfoRetainedDistinctionForcesLaplacian_attempt.v, unique-operator
argument). M remains an independent structural primitive the equation needs on
top of that (InfoStrictConeBothOrders_attempt.v, a settled negative); D was in the
same position when this paragraph was first written, but is forced as of 2026-07-08
by the seed-asymmetry results (see the banner above and InfoAsymmetricSeedTrifurcation.v
Part 7 — InfoDissipationIsIndependent_attempt.v's independence-of-M verdict still
stands; what changed is that D's structural form now follows from the whole-seed
axioms); the QM/SR
identity itself relates constructions built from those posited slots plus a posited
Minkowski signature, so "derives quantum mechanics and special relativity" is best
read as derives L_R, and proves a real relabeling identity among the remaining
posited-but-independently-characterized ingredients — not a from-one-root
derivation of either branch whole. A six-result
strengthening campaign then upgrades four previously-informal claims to theorems: a
frequency/UV ceiling forced by the graph's own maximum degree, an exact "no local
creation" energy-balance law, a Schrödinger-shaped skew-adjoint first-order skeleton,
a causal sign-construction theorem, and a discrete Noether theorem. A companion graph-
growth result gives a native, non-continuum discrete analog of cosmological expansion.
General relativity is honestly not derived: eight independent attempts this project made to recover it were tested and refuted or left open, and the manuscript argues this is the correct outcome — continuum GR is, by this project's own diagnostic standard, a non-readout (an artifact of injecting actual infinity), so an exact match was never the right target. In its place, a genuinely native discrete object is identified instead: Forman-Ricci curvature on the graph, proved to be an honest readout of the same data the mother equation uses, and linked by exact algebraic substitution to an already-proven stability (coercivity) theorem.
Knowledge map: KGMAP.md — a one-page document graph and
"which file answers which question" table; start here if you are new to
this repo and want to know where to look before reading anything else.
Manuscript: paper/main.pdf (compile from paper/main.tex) —
theorem-level claims, tiers, and reproduction commands, self-contained.
Supplement: SUPPLEMENT.md — full dependency DAG, the complete
eight-attempt GR refutation log, the full novelty audit, and the extended
reference-verification trail. Split into four files (see its own index at
the top); the open-problem ledger, completeness scoreboard, and reference
list each live in supplement/. See the manuscript's
"Main-Text vs. Supplement Boundary" section for what belongs where.
Companion synthesis note: paper/mass_note.pdf
(compile from paper/mass_note.tex) — a separate, self-contained preprint by
the same author composing several of this repository's theorems (none
individually about mass) into a curvature-limited mass bound, with its own
ten-stream literature review, circularity audit, and open-problem register,
pinned to this repository's own SHA-256 hashes at a specific commit. The
main manuscript's section "A Composed Reading: Curvature-Limited Mass"
states the overlapping claim at main-text weight and is the authoritative
version where the two differ.
Project logbook: LOGBOOK.md — a chronological, captain's-log
style record of the project's actual history: every positive result,
negative result, and scope decision, in the order it happened, including
ones later superseded (never rewritten with hindsight).
External audit gate: AUDIT_BRIEF.md — an adversarial
attack form for the companion note's four load-bearing claims (C1-C4),
each given verbatim with an exact, actionable refutation condition,
pinned artifact hashes, and a standing retraction pledge. Open this if
you are trying to break something, not just read about it.
| Tier | Meaning |
|---|---|
Th_coqc |
Machine-checked in Coq, axiom-free over ℚ (Print Assumptions prints "Closed under the global context"). |
+reals |
Machine-checked, but depends on Coq's standard Reals axioms (ClassicalDedekindReals.sig_forall_dec, FunctionalExtensionality), honestly disclosed. |
finite_diagnostic |
A numerical measurement, reproducible, not a proof. |
Dr |
An interpretive stance, not machine-checked. |
Open |
Admitted gap. |
formal/
RDL_GammaSpectral.v Edge/w_of/u_of/v_of + Dirichlet energy/term + Laplacian stencil (Q). Th_coqc.
RDL_MetricReadout.v Directional 2nd difference reads the Hessian/metric form off exactly; window-, location-, graph-gauge-invariant. Th_coqc.
InfoMetricIsEnergyReadout.v The graph metric IS an energy readout: the same L_R data read as metric/curvature equals the mother-equation energy form. Th_coqc.
InfoMemoryBeforeMass.v Discrete core of "memory before mass": inertia as retained memory, exact over Q (no continuum, no 1/(2m) division). Th_coqc.
InfoCoercivityBoundedClosure.v Csafe/wshare/wdeg definitions. Th_coqc.
InfoDiscreteGraphCurvature.v Forman-Ricci curvature, flat-cycle fact, wdeg=w*deg link to coercivity. Th_coqc.
InfoAnalysisLift.v Schwarzschild metric factor + real radial derivative. +reals.
InfoQuantumGravityRootBridge.v Regge-Wheeler potential built on InfoAnalysisLift.schw. +reals.
InfoSchrodinger.v Quantum dispersion M*omega^2=K*lambda and energy spectrum from the Laplacian spectrum. Th_coqc.
InfoLorentzInvariance.v Boost-invariant interval + exact-quadratic-class box_quad operator. Th_coqc.
InfoQuantumRelativityUnification.v Quantum dispersion IS box_quad vanishing -- one equation, two readouts. Th_coqc.
InfoLorentz.v Discrete causal bilinear form: self-adjoint, Euclidean reduction, permutation-invariant. Th_coqc.
InfoLorentzContinuum.v Continuum limit of the signed second-difference operator = the d'Alembertian Box=-dtt+dxx. +reals.
InfoSpectralCeiling.v Degree-sum (Rayleigh/Gershgorin) spectral ceiling lambda<=2*dmax. Th_coqc.
InfoRecurrenceEnergy.v Exact leapfrog Lyapunov identity: CFL window + damped energy decrement. Th_coqc.
InfoQuantumFrequencyCeiling.v Composes the above with quantum dispersion: a real UV/frequency ceiling + tau_c-floor window. Th_coqc.
InfoGraphFluxBalance.v Discrete divergence theorem + Green's identity + exact vector energy balance ("no local creation"). Th_coqc.
InfoCompanionSkew.v First-order companion form, skew-adjoint under the energy inner product (Schrodinger-shaped skeleton). Th_coqc.
InfoCausalSignature.v Sign constructed from order comparability; exact PSD-split; a concrete (1,3)-signature witness. Th_coqc.
InfoGraphNoether.v Graph automorphism => exact conserved (momentum-like) quantity. Th_coqc.
InfoGraphGrowth.v Graph growth: curvature/energy laws, order-collapse obstruction theorems, and an exact discrete dilution law -- a native, non-continuum expansion analog. Th_coqc.
InfoActionStationarity.v The mother equation is an exact Euler-Lagrange stationarity readout (field + geometry sides); NOT claimed to narrow any gap to GR. Th_coqc.
InfoCurvatureBalance.v Forman curvature composed into an exact affine horizon threshold + an unconditional no_escape/repair_exists dichotomy; a separate curvature-affine balance law is conditional on an explicit modeling ansatz. Th_coqc.
InfoProductSpectrum.v n-D spectral ladder step 1: Kronecker/Rayleigh additivity for product graphs. Th_coqc.
InfoContinuumLimit_nD.v n-D spectral ladder step 2: flat/weighted multi-axis continuum-limit readout; reproduces this repo's own lorentz_box as an instance. +reals (Tier-1, no classic).
InfoWeightedReadout.v n-D spectral ladder step 3: variable-coefficient (a*u')' readout from the discrete flux stencil. +reals (Tier-1, no classic).
InfoCrossTermDominance.v n-D spectral ladder step 4: an iff between graph-form representability and diagonal dominance, both directions sharp. Th_coqc.
InfoDiskBeforeLock.v Anisotropic retention: a perpendicular candidate strictly worsens the retention functional while a parallel one never does, immediate at every decision point. Th_coqc.
InfoGrowthFold.v Multi-edge curvature fold: exact, order-independent cumulative curvature shift over any list of added edges. Th_coqc.
InfoCeilingMonotone.v Rayleigh ceiling monotonicity under retention; explicitly does NOT claim individual eigenvalue interlacing. Th_coqc.
InfoCurvatureNoether.v Forman curvature is invariant under any graph automorphism (extends an existing quadratic-form invariance result to curvature). Th_coqc.
InfoModeRotation.v The mother equation's CFL stepper at one window point IS the i-rotation matrix; two more window points give crystallographic periods 6 and 3. Th_coqc.
InfoPentagonSpectrum.v 5-cycle Laplacian cubic identity lands in the golden ratio's own field; 6-cycle exhibits all 4 rational eigenvalues explicitly. Th_coqc.
InfoAreaLaw.v A uniform region's energy comes entirely from its boundary -- a graph-native fact, explicitly not the holographic bound. Th_coqc.
InfoDegreeFromCurvature.v Degree bounded by 4 minus local Forman curvature; feeds the spectral ceiling with a curvature-derived value. Th_coqc.
InfoTensorFrame.v General symmetric-tensor reconstruction from diagonal + face-diagonal evaluations, any dimension -- an abstract fact, not yet about this repo's own graphs. Th_coqc.
InfoStrainTensorBridge.v Connects curvature to the tensor-reconstruction fact, conditional on an affine-cell hypothesis; also a native local-screen split and a disclosed-ansatz Clausius-type inequality. Th_coqc.
InfoOptimizerWindow.v Heavy-ball/momentum optimization on a quadratic mode is exactly the mother equation's own leapfrog energy theory, under an exact reparametrization. Th_coqc.
InfoEntropyLicense.v Degree recast as a per-node entropy quantity; handshake identity, append-only monotonicity, and an entropy-language frequency ceiling. Th_coqc.
InfoBoundaryScreening.v A region's exterior is invisible to interior field changes off the boundary; capacity and boundary-node count kept as separate, non-equal quantities. Th_coqc.
InfoCubicLinearization.v First file to give the mother equation's nabla-V(Phi) slot a concrete nonzero instance; exact one-step polarization of an on-site cubic force term. Th_coqc.
InfoReadabilityBoundary.v No rational stepper parameter gives the 5th-iterate period-5 case; one further instance in the crystallographic-restriction family, explicitly not the general theorem. Th_coqc.
InfoSpectralCeilingSharp.v The Anderson-Morley eigenvalue ceiling, mechanized in witness form: lambda <= 4-F_min directly, a factor sqrt(2) tighter than the earlier 2*dmax route. Th_coqc.
InfoRetainedDistinctionForcesLaplacian_attempt.v L_R = D_W-W is the UNIQUE vertex operator with {symmetric, zero-row-sum, off-diagonal<=0}; adjacency/signless/random-walk/normalized alternatives refuted by witness. The one FORCED link in the root->spine chain (SUPPLEMENT.md §1.1). Th_coqc.
InfoStrictConeBothOrders_attempt.v Six forcing readings for why the spine needs a 2nd-order (M) term are each shown insufficient on a 5-node witness; M is an independent structural primitive, not forced by the root (SUPPLEMENT.md §1.1). Th_coqc + [Dr] interpretation (tagged in-file).
InfoStrictConeSymmetryIrrelevant_attempt.v Generalizes the above to ANY graph-distance-banded operator, symmetric or not -- no symmetry hypothesis used anywhere; confirmed concretely on an explicit asymmetric witness. Closes the question of whether the sibling file's symmetric L_R was hiding the discriminator: it was not -- cone-locality is a pure sparsity-pattern fact, insensitive to direction. Th_coqc + [Dr] (converges with InfoAsymmetricSeedTrifurcation.v's independent finding that asymmetry does not touch conservation either).
InfoDissipationIsIndependent_attempt.v A 2-node toy isolates D: the M-branch preserves a quadratic energy exactly (reversible), the D-branch strictly decreases it every step -- neither derivable from the other (SUPPLEMENT.md §1.1). Th_coqc + [Dr] interpretation (tagged in-file).
InfoZeroInfinityReciprocal_attempt.v The reciprocal 0<->infinity blow-up over Q; the singularity paradigm (Z1 point + I4 density, together) as one non-readout, not two (SUPPLEMENT.md §1.2). Th_coqc + [Dr].
InfoOperatorLosesPropertyAtEndpoints_attempt.v Multiplication over Q provably loses cancellation/invertibility exactly at 0 and has no element to close at infinity -- every operator pays a price at either refused endpoint (SUPPLEMENT.md §1.2). Th_coqc + [Dr].
InfoErasureArrowOfTime_attempt.v x0 erasure and /0 non-readout, machine-checked; zero-as-redistribution not zero-as-destruction (SUPPLEMENT.md §1.2). Th_coqc + [Dr].
InfoAsymmetricSeedTrifurcation.v CANDIDATE upgrade (not proven equivalent to the above): any asymmetric R0 exactly decomposes into DiagPart+SymOff+SkewOff; the antisymmetric shape is FORCED by nat's own trichotomy (not posited); SkewOff/DiagPart genuinely recover step_M/step_D by direct computation at concrete parameter values, not shape resemblance. Part 7 (added): imposing {offdiag_le0, rowsum0} on the WHOLE seed (not just its symmetric part) forces D itself -- the symmetric-coupling degree minus the seed's own net directed circulation -- down to two free primitives (Wt, lam), not three. Does NOT retract InfoDissipationIsIndependent_attempt.v's Th_coqc content; realizes a possibility that file's own SCOPE block left explicitly open. Th_coqc + [Dr] (header SCOPE block + its appended UPDATE block state what remains open: whether {offdiag_le0_full, rowsum0_full} are themselves uniquely forced, not just a natural extension of L_R's own axioms).
InfoSeedFeedsQuantumRelativity_attempt.v A uniform-weight seed instantiation induces the standard K3 combinatorial Laplacian, whose eigenvalue 3*w is EXHIBITED (explicit rational eigenvector (1,-1,0), not posited) -- that eigenvalue fact is the genuinely new content here. It is then applied (one-line, not a strengthening) to InfoQuantumRelativityUnification.box_quad_is_spine_residual, which is already universally quantified over all M,K,omsq,lam -- supplying lam=3*w adds no new logical content to that theorem, it was already true for every lam (audit note, 2026-07-08: an earlier framing implied this "wires in"/strengthens the QM/SR theorem; it does not, only the eigenvalue fact is new). The SAME seed simultaneously forces D (Part 7) at that instantiation. Part 5: a GENERIC (not seed-specific -- audit-corrected name, was `seed_causal_speed_forces_K_lt_M`) causal_speed_forces_K_lt_M shows identifying phase-speed-squared K/M with a Lorentz boost's v^2 forces K < M, from a fact already proven elsewhere in this repo (g^2(1-v^2)=1 implies v^2<1) -- an INEQUALITY between two still-free parameters, explicitly NOT a retry of SUPPLEMENT.md's refuted "Attempt 4" (which fixed K/M to one universal Planck-scale ratio and predicted a mass-independent decay rate, refuted against literature); the seed's own K,M are merely substituted into this generic bound in the witness. Built directly in this repo (not elevated from the sibling), since its dependencies only exist as separate importable files here. Th_coqc + [Dr] (M itself remains a free parameter in the existing QM/SR theorem; the bound is a conditional necessity claim, not checked against any external dataset).
InfoSeedTorsionIsSkewOff.v Discrete torsion, specialized to a rank-1 connection: Torsion(R,i,j) := R(i,j)-R(j,i) equals EXACTLY 2*SkewOff(R,i,j); on R0_forced, Torsion == 2*lam*ord, so a zero-lam seed is torsion-free and a nonzero-lam seed has a genuine, non-vacuous torsion witness (concrete: Torsion(0,1)=2 on the WtRoot/lamRoot seed). Th_coqc.
InfoSeedTorsionGroupAndRankN.v Part A: InfoConnectionFromFrame's own coboundary connection is GROUP-torsion-free (Omega(j,i)==hinv(Omega(i,j)), ring-provable); a concrete non-coboundary witness shows genuine group-valued torsion is possible -- holonomy curvature and torsion are two INDEPENDENT ways a connection can be non-trivial. Part B: a MODEST rank-n extension -- n INDEPENDENT decoupled seeds sharing one lam, each getting Part 1's identity -- explicitly flagged as the decoupled special case, not the fully general mixing torsion (see InfoSeedTorsionGenuineMixing.v). Th_coqc.
InfoSeedTorsionGenuineMixing.v Closes the harder half of the torsion item: Gamma(k,i,j):=T(k,i)*R(i,j) genuinely entangles output component k with base pair (i,j) through a shared table T, not n independent copies. Separable T collapses to the decoupled shape (making explicit what "decoupled" meant); a concrete non-separable T (Kronecker delta) on the WtRoot/lamRoot seed gives a real, computed witness where the zero/nonzero pattern itself changes with k; no_shared_shape_decoupling RIGOROUSLY proves no single scalar reduces one k's torsion to another's -- a genuine impossibility proof, not an illustration. Th_coqc.
InfoSeedCurvatureIntegration.v Builds this repo's already-proven Forman-Ricci curvature from the SAME uniform-weight K3 seed InfoSeedFeedsQuantumRelativity_attempt.v already used for the QM/SR eigenvalue bridge. Every node has degree 2, so every edge is Forman-flat (applying forman_flat_if_both_degree_two, not re-deriving it -- an honest, unglamorous result matching this repo's own documented 2-regular-graph pattern). THE LINK: weighted degree (wdeg) is computed to equal exactly the degree term in the seed's forced-D formula -- checked, not assumed. No underlying theorem becomes tighter or more general; K3 is flat, honestly. Th_coqc.
InfoSeedTauRelFloor.v Applies InfoSpectralCeilingSharp's Anderson-Morley bound (lam<=4-Fmin) to the seed's own eigenpair on the unweighted K3 carrier -- verified (not assumed) that eigenvector (1,-1,0) gives eigenvalue 3, matching InfoSeedFeedsQuantumRelativity_attempt.v's weighted eigenvalue formula (3*w at w=1) exactly: two independently-defined machineries agree on the same carrier. Genuinely new: tau_rel_floor, a general reciprocal-monotonicity lemma turning the curvature ceiling on lam into a genuine LOWER BOUND on relaxation time 1/lam. Honest caveat: not numerically dramatic (K3 is small/flat, an unsaturated floor -- 1/4 vs actual 1/3); the spectral-gap-as-relaxation-time reading is a standard interpretation, not derived here. Th_coqc.
InfoSeedLambdaCCrossover.v Plugs the seed's forced D (5, node 0 of the WtRoot/lamRoot witness) and its verified eigenvalue (3) into InfoTelegraphCrossover_attempt.v's existing under/over-damped classification. Honest finding stated up front: M and K remain genuinely free -- the seed does NOT force a regime. It DOES force the critical PRODUCT M*K=D^2/(4*lam)=25/12 to a single seed-determined number, even though M,K individually stay unpinned. Two concrete witnesses straddling this threshold, both respecting the existing K<M causal bound: (M,K)=(3,1) is under-damped (quantum/wave reading), (M,K)=(2,1) is over-damped (classical/decay reading) -- same D, same lam, genuinely different regime, exactly as expected since M,K are not forced. Th_coqc + [Dr] (whether M,K should be further constrained beyond K<M is explicitly [Open]).
InfoSeedArbitraryNForcing.v Generalizes the seed's forced-D identity from fixed n=3/n=4 witnesses to an ARBITRARY NoDup vertex list, via genuine induction (not per-size re-checking). Key lemma fold_right_replace_one: two functions agreeing everywhere except one distinguished list element have fold-sums differing by exactly the gap there -- proved once, reused for every vertex count. R0_general_rowsum0_forced/R0_general_diagpart_forced re-derive the row-sum axiom and D=degree-lam*circulation identity for any NoDup list; a concrete n=5 witness (D values 10,21,28,33,38, genuinely new numbers) applies the general theorem directly. Th_coqc.
InfoSeedCirculationArbitraryN.v Closes the remaining fixed-n gap: the seed's circulation-sums-to-zero ("asymmetric but balanced") principle also generalizes to an ARBITRARY vertex list, via a discrete Fubini lemma (fubini_double_sum: swapping outer/inner in a fold_right double sum, with the function's arguments swapped to match, leaves the total unchanged). circulation_sums_to_zero_general: for any antisymmetric function and any vertex list, the double sum over L x L vanishes exactly (swap via Fubini, antisymmetry turns the swap into a negation, so the sum equals its own negation, hence zero). Applied to SkewOff via its already-proven antisymmetry; checked on the same n=5 instance. Both halves of the seed's forcing-machinery generalization (row-sum/D-forcing AND circulation-balance) are now genuinely arbitrary-n. Th_coqc.
scripts/
verify_quantum_gravity_root_bridge.py Finite-graph (PML) quasinormal-mode eigenvalue solver; converges to the literature Schwarzschild QNM. finite_diagnostic.
40+ Coq files (this count predates the 2026-07-08 six-file addition above and was
already not re-verified against ls formal/*.v at time of writing -- run
ls formal/*.v | wc -l for the current number rather than trusting this line),
186+ theorems, every one Tier-0 axiom-free or +reals as marked.
# Ubuntu/Debian
sudo apt-get update && sudo apt-get install -y coq
# or via opam (any platform)
opam init -y && opam install -y coqVerified against Coq 8.20.1.
pip install -r requirements.txtmake verifyThis compiles all 81 formal/*.v files in dependency order (see Makefile's COQFILES for the
current authoritative list — as of PR #31 it equals ls formal/*.v exactly; the file-by-file
table above is a legacy inventory and may itself lag the current file count, per its own
"40+ Coq files" caveat two paragraphs up) with
coqc -q -R . DQG <file>, then runs scripts/verify_quantum_gravity_root_bridge.py,
and prints a PASS/FAIL summary. Expected per-file result:
| File | Expected Print Assumptions output |
|---|---|
RDL_GammaSpectral.v |
Closed under the global context |
RDL_MetricReadout.v (metric_form_readout, metric_readout_graph_gauge) |
Closed under the global context |
InfoMetricIsEnergyReadout.v (metric_form_is_energy_readout) |
Closed under the global context |
InfoMemoryBeforeMass.v (memory_before_mass, mass_inferred) |
Closed under the global context |
InfoCoercivityBoundedClosure.v |
Closed under the global context |
InfoDiscreteGraphCurvature.v |
Closed under the global context |
InfoSchrodinger.v |
Closed under the global context |
InfoLorentzInvariance.v |
Closed under the global context |
InfoQuantumRelativityUnification.v |
Closed under the global context |
InfoLorentz.v |
Closed under the global context |
InfoSpectralCeiling.v |
Closed under the global context |
InfoRecurrenceEnergy.v |
Closed under the global context |
InfoQuantumFrequencyCeiling.v |
Closed under the global context |
InfoGraphFluxBalance.v |
Closed under the global context |
InfoCompanionSkew.v |
Closed under the global context |
InfoCausalSignature.v |
Closed under the global context |
InfoGraphNoether.v |
Closed under the global context |
InfoGraphGrowth.v |
Closed under the global context |
InfoActionStationarity.v |
Closed under the global context |
InfoCurvatureBalance.v |
Closed under the global context |
InfoProductSpectrum.v |
Closed under the global context |
InfoCrossTermDominance.v |
Closed under the global context |
InfoDiskBeforeLock.v |
Closed under the global context |
InfoGrowthFold.v |
Closed under the global context |
InfoCeilingMonotone.v |
Closed under the global context |
InfoCurvatureNoether.v |
Closed under the global context |
InfoModeRotation.v |
Closed under the global context |
InfoPentagonSpectrum.v |
Closed under the global context |
InfoAreaLaw.v |
Closed under the global context |
InfoDegreeFromCurvature.v |
Closed under the global context |
InfoTensorFrame.v |
Closed under the global context |
InfoStrainTensorBridge.v |
Closed under the global context |
InfoOptimizerWindow.v |
Closed under the global context |
InfoEntropyLicense.v |
Closed under the global context |
InfoBoundaryScreening.v |
Closed under the global context |
InfoCubicLinearization.v |
Closed under the global context |
InfoReadabilityBoundary.v |
Closed under the global context |
InfoSpectralCeilingSharp.v |
Closed under the global context |
InfoAnalysisLift.v |
ClassicalDedekindReals.sig_forall_dec, FunctionalExtensionality.functional_extensionality_dep |
InfoQuantumGravityRootBridge.v |
same two Reals axioms as above |
InfoLorentzContinuum.v |
same two Reals axioms as above |
InfoContinuumLimit_nD.v |
same two Reals axioms as above |
InfoWeightedReadout.v |
same two Reals axioms as above |
python3 scripts/verify_quantum_gravity_root_bridge.pyPrints a grid-resolution convergence table (N=400..6400) of the fundamental
scalar (l=2, n=0) quasinormal-mode eigenvalue against the literature target
Mω ≈ 0.4836 − 0.0968i (Leaver 1985). The full N=6400 run can take several
minutes; make verify allows a 90s timeout and treats a partial (but
monotonically converging) run as a pass — a timeout exit code alone is not a
failure.
spine_pde is a separate, self-contained Python package — a computational,
readable reference implementation of the same theory, checked in EXACT mode
against the Coq theorems above bit-for-bit (see spine_pde/README.md's
"Audit, don't believe" table).
make test-lib
# equivalent to:
# pip install -e "spine_pde[dev]"
# cd spine_pde && python -m pytest -q tests/or, from a fresh clone:
git clone https://github.com/morrocwi/causal-quantum-gravity.git && cd causal-quantum-gravity/spine_pde
pip install -e '.[dev]' # editable install + pytest + sympy
pytest -q # exact-mode values checked against theorems
python examples/quickstart.py # runnable end-to-end exampleRemoves all .vo/.vok/.vos/.glob/.aux build artifacts.
This repository is an extracted, minimal, standalone subset of a private
research repository, research_universal_solver — flattened into 35 independent formal/*.v files (each
carrying only the definitions its own theorems actually use, trimmed from
larger source modules) plus one Python script, copied verbatim. Nothing was
renamed or altered beyond: dropping the _attempt suffix some source files
used internally, and adding a minimal Require/Open Scope preamble to each
file so it compiles standalone outside its original multi-thousand-line
context. Original authorship dates, by file:
| File | Originally authored |
|---|---|
InfoLorentz.v, InfoLorentzContinuum.v, InfoLorentzInvariance.v |
2026-06-27 |
RDL_GammaSpectral.v, InfoCoercivityBoundedClosure.v, InfoDiscreteGraphCurvature.v, InfoSchrodinger.v, InfoAnalysisLift.v, InfoQuantumGravityRootBridge.v, InfoQuantumRelativityUnification.v, scripts/verify_quantum_gravity_root_bridge.py |
2026-07-04 / 2026-07-05 |
InfoSpectralCeiling.v, InfoRecurrenceEnergy.v, InfoQuantumFrequencyCeiling.v, InfoGraphFluxBalance.v, InfoCompanionSkew.v, InfoCausalSignature.v, InfoGraphNoether.v, InfoGraphGrowth.v, InfoActionStationarity.v, InfoCurvatureBalance.v, InfoProductSpectrum.v, InfoContinuumLimit_nD.v, InfoWeightedReadout.v, InfoCrossTermDominance.v, InfoDiskBeforeLock.v, InfoGrowthFold.v, InfoCeilingMonotone.v, InfoCurvatureNoether.v, InfoModeRotation.v, InfoPentagonSpectrum.v, InfoAreaLaw.v, InfoDegreeFromCurvature.v, InfoTensorFrame.v, InfoStrainTensorBridge.v, InfoOptimizerWindow.v |
2026-07-05 |
InfoEntropyLicense.v, InfoBoundaryScreening.v |
2026-07-05 |
Every citation to outside literature in this repository (Forman, Bekenstein,
Jacobson, etc.) should already be registered, with owner and year, in
research_universal_solver's docs/root/EQUATION_REGISTRY.md — that file, not
memory, is the canonical source if you need to add or verify a citation.
See SUPPLEMENT.md for the full narrative, the dependency DAG, the
numerical validation (Hückel benzene, Forman curvature sanity checks), and the
honest audit of what was and was not derived; the open-problem ledger and the
complete reference list are in supplement/ (see SUPPLEMENT.md's
own index).