GravityCrossTerm — unified Lean 4 audit project

Lean 4 / Mathlib formalization project corresponding to the paper:

Gravity as a Cross-Term Effective Gradient: Source-Position Dependence and Spherical-Symmetry Breaking in an A₅-Seeded Finite Medium (v13 self-contained first-paper revision)

This single library covers all 23 §10.1 M-claims of the paper.

Toolchain

• Lean: leanprover/lean4:v4.29.0-rc2
• Mathlib: v4.29.0-rc2 (specified in lakefile.toml)

Build

lake update      # fetch Mathlib (slow on first run)
lake build       # build all 22 files

Expected outcome: sorry = 0, axiom = 0 across all files.

File / M-claim correspondence

Existing seed-graph foundation (9 files)

File	§10.1 M-claim / audit role	Section
IcosaGreenFunctionTable.lean	M3, M4, M5	§3.2, §7.1
IcosaLaplacianMatrix.lean	M1, M2	§3.1
ZeroMeanMonopoleSource.lean	M17 (source convention)	§4.7
EquilibriumGreenEnergy.lean	M17 (E_eq cross term)	§4.7, §7.1
IcosaAttractivePotentialAudit.lean	M5 + P_grav (U₁<U₂<U₃)	§7.1
AttractiveSignTheoremIcosa.lean	§7.1 attractive-sign anchor	§7.1
A5MediumAttractiveSignBridgeAudit.lean	§7.5 bridge audit	§7.5
GradientMonopoleAdmissibilityAudit.lean	§11.4 firewall audit	§11.4
MinimalDirectionSign.lean ★	M23 (+ partial M18, M22)	§6.4, App.B

★ = the file the paper explicitly names as "build OK".

New M-layer audits (13 files, Batch 1–6)

File	§10.1 M-claim	Section
SingleSourceShellUniformity.lean	M6	§3.3
SingleSourceStabInvariance.lean	M7	§3.3
PolarizationBookkeepingGeneralQ.lean	M8 (general Q)	§4.1, §4.2
LinearResponseGrammar.lean	M9	§2.2, §4.2
OverlapDistancePairFunctorial.lean	M10	§5.1
OverlapStabReduction.lean	M11	§5.2
DistanceKernelLocalization.lean	M20* / M20a / M12	§1.2.1, §4.4–4.6
MassCrossProfileOrdering.lean	M13	§7.4
FiniteDifferenceGradientAxial.lean	M14	§6.2
ShellCountSquareAnsatzFirewall.lean	M15	§8.1
StaticChannelTrichotomy.lean	M18	§6.3
CrossProfileNonvanishingA5.lean	M21	§7.4
ResistiveChannelExclusion.lean	M22	§6.3

Central theorem

DistanceKernelLocalization.lean contains the central M-layer theorem M20* (distance_kernel_localization), with M20a (self-energy independence) and M12 (cross-distance kernel) as direct corollaries.

Namespaces

All files use namespace A5Cosmology.<X>. The A5Born sub-namespace of the parent project has been removed in this consolidation, so existing files now declare namespace A5Cosmology directly without an intermediate A5Born layer.

MinimalDirectionSign.lean already used A5Cosmology.MinimalDirectionSign in the parent project and is unchanged.

Imports

All 9 existing files have had import A5Born.X rewritten to import GravityCrossTerm.X. Internal open <ChildNamespace> statements are unchanged because they are unqualified and resolve correctly under the new namespace layout.

File coverage / claim matrix

Claim	File
M1, M2	IcosaLaplacianMatrix
M3, M4, M5	IcosaGreenFunctionTable
M6	SingleSourceShellUniformity
M7	SingleSourceStabInvariance
M8	PolarizationBookkeepingGeneralQ
M9	LinearResponseGrammar
M10	OverlapDistancePairFunctorial
M11	OverlapStabReduction
M12	DistanceKernelLocalization
M13	MassCrossProfileOrdering
M14	FiniteDifferenceGradientAxial
M15	ShellCountSquareAnsatzFirewall
M17	EquilibriumGreenEnergy + ZeroMeanMonopoleSource
M18	StaticChannelTrichotomy (+ partial in MinimalDirectionSign)
M20*, M20a	DistanceKernelLocalization
M21	CrossProfileNonvanishingA5
M22	ResistiveChannelExclusion (+ partial in MinimalDirectionSign)
M23	MinimalDirectionSign

(M16, M19 are absorbed into M8 / M20* per §10.1 dependency map.)

Firewall (per the paper)

This formalization does NOT establish:

• Newton's law of gravitation, inverse-square scaling, or Newton's constant
• Continuum / GR / equivalence-principle limits
• Quantum-side address-relaxation duality
• Substrate uniqueness of the A₅ icosahedral seed
• The reformulation thesis itself
• Any P-layer interpretive contract beyond §7.1 attractive-sign reading
• Any Open Bridge resolution (G₃ wake kernel, G₅ continuum, etc.)

These remain explicit Open Bridges per the paper's §10–§11 disclosure.

Design notes

• Each new M-layer audit file (SingleSourceShellUniformity etc.) is import Mathlib-only and self-contained. Some definitions (DistanceAut, shellField, etc.) are duplicated across files so that each can be built independently.
• The substrate is abstracted as a finite type V with a distance function d : V → V → ℕ, avoiding direct dependence on SimpleGraph.
• All scalars use ℚ (rationals) — the paper's M-layer claims are algebraic identities that hold in any ordered field.
• Existing files retain their cross-import dependency structure (IcosaGreenFunctionTable → IcosaLaplacianMatrix → ...) and internal references (open IcosaGreenFunctionTable etc.).