feat(M14.7): add AdS radial pointwise double copy - #182
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Scope
Adds the AdS radial/boundary field layer above the merged M14 AdS-normalized double-copy model.
Formal authority
jagg-ix/entropic-physlib-privateentropic-physlib-linear-full35f98f147771a4e250ec01b4cbf2afab72313db7EMComplexEinsteinAdSCFT, and GKP--Witten source blobs are pinned in the ledger.Toolchain
4.31.0/leanprover/lean4:v4.31.0jagg-ix/zil-lean@6daee2698304feb203c6adb91b2e8853613f85b5Validation
The study closes all 9 acceptance groups.
Claim boundary
The radial carrier is linear and harmonic. This PR does not prove AdS/CFT, construct an interacting Witten functional, identify amplitudes with entropy, or establish a global/loop-level AdS double-copy theorem.
Merge audit
maindirectly;93607ae7c147e071fe62d6f4c0a2d182f276477d;Recommended merge order: M14.5 → M14.6 → M14.7. This branch remains executable against current
mainbecause it imports no files from the companion branches.