Your holography paper,
checked end to end.
Energy Transmission Across Holographic Conformal Interfaces in General Dimensions
arXiv:2609.38318 [hep-th] · submitted 29 September 2026 · 9 + 20 pages
Igal Arav, Theodore Bertrand, Shira Chapman, Giuseppe Policastro, Sebastian Waeber
arxiv.org/abs/2609.38318 · PDF
About this deck. A workflow proposal prepared by Daniel Liezrowice (Engineering Software Lab) for the paper's authors: what the MantiQ Factor process would do with this specific paper. Independent of the authors; no work has been executed yet; paper facts cited from v1. Precedents: MantiQ Factor / REED, MantiQ / QPE, MantiQ / Solidity.
MantiQ Factor, in one picture.
The production line the REED case study built: seven stages from a public research paper to formally verified, executable systems. This deck maps that same line onto your paper.
Reading the picture: the seven stages (input, conversion, understand, compute, verify, engineer, output) compress into the six-stage pipeline on slide 04, adapted to a theory paper. Image source: MantiQ Factor / REED case study, slide 1.
Four results that invite independent checking.
Energy scattering across a conformal interface, studied through AdSd-sliced domain walls: a compact research paper with dense, checkable mathematics.
1 · Closed-form transmission from the warp factor
For metrics ds² = dy² + a²(y) ds²(AdSd) asymptotic to empty AdSd+1, the transmission coefficient TL is a closed-form functional of the warp factor a(y) alone (Eq. 15), independent of the wave details.
2 · Recovers d = 2, extends to general d
Reproduces the known two-dimensional holographic results (Refs. 11, 12, 16) and extends them to arbitrary dimension. The d = 2 Janus case has a fully explicit form (Eq. 154).
KNOWN RESULTS = READY-MADE REGRESSION TARGETS3 · Universality within the class
Transmission is independent of the incidence angle, of the profile of the incident perturbation, and of the source used to create it. Examples: thin-brane models, Janus geometries (Eqs. 27 to 29).
SWEEPABLE IN A SIMULATOR4 · Bounds from CFT-like data
Transmission is bounded by central-charge-like quantities: lower and upper bounds controlled by CTL / CTR (Eq. 23), with the bound structure proved in Appendix B. Complete reflection is attainable in multi-brane models.
INEQUALITY · A NATURAL PROOF TARGETKey d = 2 check value (Eq. 154): TL = Ω(b) = √(b(2−b)) / (2 arctanh √(b/(2−b))), with T → 1 as b → 0 and T → 0 as b approaches the bound of the allowed range. Boundary: results are for the stated class, linearized perturbations; the Discussion itself asks how far they extend.
The MantiQ pipeline, applied to your paper.
Six stages. Each produces a different evidence class, and no stage silently strengthens the one before it.
Freeze the source
PDF + LaTeX source, SHA-256 manifest. The paper's claims are enumerated verbatim into a claim ledger.
PAPER / DERIVEDMake scope explicit
Manual transcription of the metric ansatz, the TL definition, conventions (Fefferman-Graham, slicing, branches). Ambiguities become ledger entries, never silent repairs.
RECORDED ASSUMPTIONSWolfram notebook oracle
Symbolically re-derive Eq. 15 for thin-brane and Janus warp factors, reproduce Eq. 154, verify limits, generate frozen regression vectors plus a named audit.
SYMBOLICALLY VALIDATEDLean 4, scoped
Kernel-checked theorems: the transmission bounds (Appendix B structure), the d = 2 Janus identity, the complete-reflection limit. The proof boundary is published.
FORMALLY PROVED (SCOPED)QASM / Classiq artifact
Compile the domain-wall wave dynamics into a quantum circuit (OpenQASM or a Classiq program), run it on a simulator, and overlay measured transmission on the closed form.
NUMERICALLY TESTEDEvidence package
Claim-status table, notebook, Lean files, vectors, QASM / Classiq circuit, simulator, reproduction guide. Public, downloadable, extensible by readers.
REPRODUCIBLEWhy the front of the pipeline fits this paper.
One central object, one headline functional
The whole paper lives on the warp factor a(y) and the functional TL[a]. Closed forms, limits, and bounds around a single object are exactly what an executable oracle is for.
Known results become regression vectors
The d = 2 results (Refs. 11, 12, 16) and Eq. 154 are fixed targets. The REED pattern applies directly: freeze vectors, audit them, and never edit the oracle to fit an implementation.
The bound is a scoped proof target
Appendix B is an inequality over a stated class of warp factors, the kind of statement Lean 4 + Mathlib handles well when the scope is explicit.
Culture match
The paper already separates what is proved, what is checked, and what is expected (Appendix D is labeled a consistency check, not a fix). MantiQ formalizes exactly that separation.
Boundary: this is the assessment for the workflow's first four stages. Stage-fit for the endpoint is addressed separately (slides 08 and 10).
The notebook: an independent oracle for TL.
Symbolic re-derivations
- Evaluate the warp-factor integral (Eq. 15) for the thin-brane family and the explicit per-dimension forms of Appendix F.
- Reproduce the d = 2 Janus closed form (Eq. 154) from the warp-factor solution (Eq. 29).
Limit and edge behavior
- b → 0 gives TL = 1 (no defect); b approaches its maximum gives TL → 0 (complete reflection, logarithmic divergence).
- Pure-AdS reference: TL = 1 by construction.
Dimension scans
- Sweep even and odd d, testing the paper's observation that transmission increases slightly with d under the b / bmax parameterization.
- Check the tension bounds of Appendix C against the admissible-parameter region.
Frozen vectors and audit
- Deterministic regression vectors (d, family, parameter, TL) with SHA-256 manifest, the REED vector-schema pattern.
- A named audit of checks, run headless via wolframscript, with exact counts reported.
Status language: each item ends as SYMBOLICALLY VALIDATED for the named families and cases only. A notebook checks named cases; it is not a universal theorem.
Scoped theorems, published boundary.
Candidate headline theorems
- Bounds: for the stated warp-factor class, TL lies between the CTL / CTR-controlled lower and upper bounds (the Appendix B inequality structure).
- d = 2 certificate: the Janus integral evaluates to Ω(b) = √(b(2−b)) / (2 arctanh √(b/(2−b))), kernel-checked like the REED BASE-1024 certificate.
- Complete reflection: TL → 0 as b approaches the allowed maximum, under stated hypotheses.
What Lean would not prove
- The linearized Einstein-scalar derivation (Appendix A) and holographic renormalization stay outside.
- Israel-condition matching (Appendix D) and the angular-coordinate computations stay outside.
- These remain PAPER / DERIVED, with the derivation chain cited. Declared non-goals, not omissions.
Trust discipline
No sorry, no admit, no project axioms. Only Mathlib's logical foundation (propext, Classical.choice, Quot.sound), with an axiom audit published alongside the theorems, as in the REED and QPE runs.
Precedent scope
The QPE case study proved exactly one resource identity and said so. The same honesty applies here: a bounded, correct proof set beats an implied but unreachable whole-paper formalization.
Boundary: Lean proves mathematics under definitions. It asserts nothing about any numerical solver, and the solver asserts nothing about Lean.
The endpoint: a verified circuit on a simulator.
From warp factor to circuit
The domain-wall scattering problem is a wave equation with a position-dependent speed: exactly the class Hamiltonian simulation and discrete-time quantum walks handle. Discretize the linearized perturbation on a(y) into a unitary circuit.
QASM and Classiq targets
Emit OpenQASM for stock simulators, or synthesize through Classiq; both are named target outputs of the MantiQ production line. The circuit is the executable artifact, not a diagram of one.
Three routes to the same number
Run the circuit on a simulator, read the transmitted energy from measured amplitudes, and compare against two independent routes: the Wolfram oracle and the closed-form TL. Disagreement is preserved and diagnosed, never repaired away.
Interactive lab alongside
A browser lab sweeps d, family (thin brane, Janus, multi-brane), and parameters: watch the transmission curve move, watch the bounds tighten as CTL / CTR changes, and see the slight d-dependence directly.
Status language: simulator agreement is NUMERICALLY TESTED for the swept grid. No quantum speedup is claimed: the circuit is the checked, executable form of the model, not a hardware claim. And it is hardware-ready: if the research ever needs a real device, the same artifact is the input to cloud backends, not a rewrite.
Claim by claim: what a run would establish.
| Paper claim | MantiQ evidence status | Artifact and boundary |
|---|---|---|
| Closed-form TL[a] (Eq. 15) | SYMBOLICALLY VALIDATED | Wolfram re-derivation for thin-brane and Janus families; exact values per named case. Not a theorem about all warp factors. |
| d = 2 reproduction (Eq. 154) | FORMALLY PROVED + TESTED | Lean certificate for the Janus identity plus numeric regression vectors. Scoped to the flat-potential d = 2 case. |
| Central-charge bounds (Eq. 23) | FORMALLY PROVED (SCOPED) | The Appendix B inequality structure, formalized for the stated class. Hypotheses travel with the theorem. |
| Universality: angle and profile independence | NUMERICALLY TESTED | Simulator sweeps over angles, profiles, and sources within the class. The paper's derivation remains PAPER / DERIVED. |
| Beyond the class: top-down models, beyond linearized order, quantum corrections | NOT ESTABLISHED (TODAY) | Open questions the Discussion itself raises. The simulator becomes the probe for future follow-ups rather than a claimed result. |
The contract: statuses apply to their stated scope and never combine into a blanket claim. Downstream stages can add evidence; they never silently strengthen an upstream claim.
Is this paper a good fit? Yes, with one scope adjustment.
● Strong fit
Wolfram oracle for the closed forms, limits, and dimension scans. Claim and ambiguity ledgers for a conventions-heavy holography derivation. Independent cross-checks through a QASM / Classiq circuit artifact executed on a simulator.
● Adapted fit
Lean 4 verification must be scoped: bounds, certificates, and limits are realistic; formalizing the full linearized-gravity derivation is research-level work and stays a declared non-goal.
● Not applicable
RTL, FPGA, and Solidity gates do not apply. The executable layer lands one level up, in the MantiQ production line's quantum targets: a QASM / Classiq circuit on a simulator, plus a public evidence package.
Summary: the pipeline applies end to end: normalize, compute, verify, then engineer the model as a QASM / Classiq circuit executed on a simulator, closing with the evidence package.
What the authors gain from a run.
Independent confirmation of the core formula
TL[a], the bounds, and the limit behavior re-derived by a separate symbolic engine, formalized where feasible, and tested numerically. Useful before follow-up work builds on the paper.
A public, extensible artifact
Notebook, Lean files, vectors, QASM / Classiq circuit, and simulator travel together with reproduction instructions, like the QPE evidence folder. Readers and referees can re-run rather than re-derive.
A lab for the open questions
The Discussion asks how far universality extends: more general matter couplings, top-down solutions, beyond linearized order. The simulator is the instrument for those probes.
A precise claimed-versus-proved map
The claim-status table gives referees and readers an exact picture of what is proved, what is computed, and what is assumed, strengthening rather than inflating the paper's claims.
Note: nothing about the paper's results changes. What changes is how independently a reader can verify them, and how easily follow-up work can start from a checked baseline.
Proposed next step: a scoped case study.
Run arXiv:2609.38318 through the QPE-shaped scope: manual transcription with an ambiguity ledger, a Wolfram notebook with a named audit and frozen vectors, scoped Lean theorems for the bounds and the d = 2 identity, an interactive scattering lab, a QASM / Classiq circuit executed on a simulator, and a public evidence page.
Weeks 1 to 2
Normalize the claims and conventions; build the Wolfram oracle for Eqs. 15, 29, and 154; freeze the first vector set and audit.
Weeks 3 to 4
Lean theorems for the bounds and the Janus certificate; publish the axiom audit and the proof boundary.
Weeks 5 to 6
QASM / Classiq circuit artifact and simulator runs, three-way cross-model comparison, and the public evidence package with claim-status table.
Daniel Liezrowice · Engineering Software Lab · daniel.l@eswlab.com · eswlab.com
Boundary: independent of the paper's authors; prepared 14 October 2026 from arXiv:2609.38318 v1. Equation numbers cite v1. This deck proposes a workflow; it reports no executed verification. Case-study precedents: REED / FHE hardware, quantum phase estimation, Solidity escrow. Third-party names remain the property of their owners; no endorsement implied.