% ==============================================================================
% appendices/main_appendices.tex
% Unified Technical Appendix: Companion Lean 4 (§A.1) & Python (§A.2) Locator Tables
% ==============================================================================

\appendix
\addtocontents{toc}{\protect\setcounter{tocdepth}{1}}

\section{Certified Lean 4 Formal Artifacts and Numerical Schemes}
\label{sec:master_appendix}

% ==============================================================================
% SUBSECTION A.1 : LEAN 4 FORMAL PROOF SUITE LOCATOR
% ==============================================================================
\subsection{Companion Lean 4 Formal Proof Suite: Architecture, Axiom Audit, and Module Locator (\texttt{lean4/NormalConeNBody/})}
\label{app:config_defs_sec}
\label{app:relative_config}
\label{app:ambient_config}
\label{app:collision_defs_sec}
\label{app:pairwise_collision}
\label{app:regular_locus}
\label{app:collision_divisor}
\label{app:collision_thms_sec}
\label{app:regular_duality}
\label{app:symplectic_defs_sec}
\label{app:symplectic_form}
\label{app:symplectic_thms_sec}
\label{app:symplectic_nondeg}
\label{app:symplectic_skew}
\label{app:bargmann_defs_sec}
\label{app:bargmann_obs}
\label{app:bargmann_thms_sec}
\label{app:bargmann_so3}
\label{app:bargmann_charge}
\label{app:normal_cone_limit_sec}
\label{app:rees_defs}
\label{app:normal_flow_symp}
\label{app:normal_cone_limit}
\label{app:canonical_splitting_recipe_sec}
\label{app:canonical_splitting_defs}
\label{app:strang_casimir_preservation}
\label{app:strang_time_reversibility}
\label{app:strang_theorems}
\label{app:cas1_heavy_top_sec}
\label{app:heavy_top_defs}
\label{app:cas1_heavy_top}
\label{app:heavy_top_theorems}
\label{app:pcr3bp_hamiltonian_sec}
\label{app:pcr3bp_hamiltonian}
\label{app:pcr3bp_regularization_bridge_sec}
\label{app:pcr3bp_regularization_bridge}
\label{app:whitney_lattice}
\label{app:partition_lattice_defs}
\label{app:cluster_hyperradius_theorems}
\label{app:maximal_flag_jacobi_theorems}
\label{app:disjoint_cotangent_commutation}
\label{app:screened_apex}
\label{app:apex_universal_lipschitz_theorems}
\label{app:lie_bargmann_invariance_theorems}
\label{app:extended_palindromic_theorems}
\label{app:synchronous_supernodes}
\label{app:unified_super_node_theorems}
\label{app:super_node_anti_zeno_theorems}
\label{app:atlas_transition_symplectic_theorems}
\label{app:strang_propagator}
\label{app:strang_order_two_theorems}
\label{app:lie_bargmann_theorems}
\label{app:suzuki_barrier_mcgehee}
\label{app:suzuki_barrier_theorems}
\label{app:bm4_seven_stages}
\label{app:blanes_moan_theorems}
\label{app:bm6_eleven_stages}
\label{app:bm6_theorems}
\label{app:symplectic_correctors}
\label{app:corrector_bm4_theorems}
\label{app:conormal_corrector_pbm4_order6}
\label{app:pbm4_gauge_transition_order6}
\label{app:global_conormal_corrector_pbm4}
\label{app:universal_order6_obstruction}

{\emergencystretch=1.5em
In accordance with repository archival standards, the complete mechanized \textbf{Lean~4 (\texttt{v4.35.0-rc2}) + Mathlib~4} formalization referenced throughout Sections~\ref{ch:ch01_introduction}--\ref{ch:ch05_higher_order_symplectic} is hosted in the permanent companion archive (\href{https://github.com/jeremynusa-hub/normal_cone_nbody3d}{\texttt{jeremynusa-hub/\allowbreak normal\_cone\_nbody3d}}, \href{https://doi.org/10.5281/zenodo.23982968}{\texttt{DOI:~10.5281/\allowbreak zenodo.23982968}}) under the directory \texttt{lean4/}. Every \texttt{Lean} verification badge in the main text links directly to this subsection: Tables~\ref{tab:lean4_module_locator_part1} and~\ref{tab:lean4_module_locator_part2} index all \textbf{35 modular proof files} (\texttt{416} formal declarations including \texttt{214} theorems and lemmas) and the \textbf{5 self-contained chapter compilation suites} (\texttt{CertifiedSuites/Sec01..05.lean}, executing \texttt{99} explicit \texttt{\#print axioms} audits with \textbf{\texttt{0 sorry}, \texttt{0 sorryAx}, and \texttt{0} custom axioms}).\par}

\begin{table}[!htbp]
\centering
\caption{Module-by-module locator for the companion Lean~4 formalization (\texttt{lean4/NormalConeNBody/}, Part~I: Sections~\ref{ch:ch01_introduction}--\ref{ch:ch04_fulton_macpherson_splitting}, Modules \texttt{01}--\texttt{18}). All modules compile with \texttt{0 sorryAx}.}
\label{tab:lean4_module_locator_part1}
\scriptsize
\renewcommand{\arraystretch}{0.94}
\resizebox{\textwidth}{!}{%
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.14\textwidth}>{\raggedright\arraybackslash}p{0.29\textwidth}>{\raggedright\arraybackslash}p{0.49\textwidth}>{\raggedright\arraybackslash}p{0.12\textwidth}@{}}
\toprule
\textbf{Sub-Package} & \textbf{Module Path (\texttt{NormalConeNBody/...})} & \textbf{Formal Structures, Definitions \& Certified Theorems (\texttt{Decls / Thms})} & \textbf{Scope} \\
\midrule
\textbf{\texttt{Ch01\_Intro}} & \texttt{01\_\allowbreak Configuration\allowbreak Space\_\allowbreak Defs.lean} & \texttt{Vec3}, \texttt{Ambient\allowbreak Configuration}, \texttt{PhaseState3D}, \texttt{Relative\allowbreak Configuration}: 3D Euclidean algebra \& barycentric slice $M_{\mathrm{rel}} = M/\R^3$ (\texttt{11 / 0}) & \S\ref{sec:common_foundations} \\
 & \texttt{02\_\allowbreak Collision\allowbreak Divisor\_\allowbreak Defs.lean}, \texttt{03\_\allowbreak Collision\allowbreak Divisor\_\allowbreak Theorems.lean} & \texttt{Binary\allowbreak Collision}, \texttt{InCollision\allowbreak Locus}, \texttt{NonCoincident}, \texttt{non\_\allowbreak coincident\_\allowbreak pair\_\allowbreak symm}, \texttt{regular\_\allowbreak iff\_\allowbreak not\_\allowbreak collision}: Pairwise diagonals $\Delta_{ij}$ \& complement duality $X = M \setminus \Delta$ (\texttt{5 / 2}) & \S\ref{sec:common_foundations} \\
 & \texttt{04\_\allowbreak Symplectic\allowbreak Form\_\allowbreak Defs.lean}, \texttt{05\_\allowbreak Symplectic\allowbreak Form\_\allowbreak Theorems.lean} & \texttt{Tangent\allowbreak Vector3D}, \texttt{omega0At}, \texttt{omega0}, \texttt{omega0\_\allowbreak skew}, \texttt{omega0\_\allowbreak self}, \texttt{omega0\_\allowbreak tangent\_\allowbreak nondeg}, \texttt{omega0\_\allowbreak global\_\allowbreak nondeg}: Darboux 2-form $\omega_0$ skew-symmetry \& global non-degeneracy (\texttt{13 / 9}) & \S\ref{sec:common_foundations} \\
 & \texttt{06\_\allowbreak Bargmann\allowbreak Algebra\_\allowbreak Defs.lean}, \texttt{07\_\allowbreak Bargmann\allowbreak Algebra\_\allowbreak Theorems.lean} & \texttt{Formally\allowbreak Smooth\allowbreak Observable}, \texttt{poisson\allowbreak BracketVal}, \texttt{poisson\_\allowbreak P\_\allowbreak G\_\allowbreak same}, \texttt{poisson\_\allowbreak L\_\allowbreak X\_\allowbreak L\_\allowbreak Y}, \texttt{poisson\_\allowbreak L\_\allowbreak X\_\allowbreak P\_\allowbreak Y}, \texttt{poisson\_\allowbreak L\_\allowbreak X\_\allowbreak G\_\allowbreak Y}: Central charge $-M_{\mathrm{tot}}$ \& $\mathfrak{bargmann}(3)$ closure (\texttt{24 / 14}) & \S\ref{sec:common_foundations} (Prop.~\ref{prop:lie_bargmann_closure}) \\
\midrule
\textbf{\texttt{Ch02\_Normal}} & \texttt{01\_\allowbreak Rees\allowbreak Deformation\_\allowbreak Defs.lean}, \texttt{02\_\allowbreak Rees\allowbreak Deformation\_\allowbreak Theorems.lean} & \texttt{Normal\allowbreak ConePoint}, \texttt{omegaNormal}, \texttt{deformation\_\allowbreak limit\_\allowbreak zero}, \texttt{omegaNormal\_\allowbreak skew}, \texttt{omegaNormal\_\allowbreak nondegenerate}, \texttt{transverse\_\allowbreak conormal\_\allowbreak flow\_\allowbreak symplectic}: Rees degeneration $t \to 0$ \& flat fiber symplecticity (\texttt{10 / 5}) & \S\ref{sec:rees_deformation} (Thm.~\ref{thm:calaque_safronov_degen}, Prop.~\ref{prop:conormal_fiber_linearity}) \\
 & \texttt{03\_\allowbreak Canonical\allowbreak Splitting\_\allowbreak Defs.lean}, \texttt{04\_\allowbreak Canonical\allowbreak Splitting\_\allowbreak Theorems.lean} & \texttt{Splitting\allowbreak State}, \texttt{Conormal\allowbreak Integrator}, \texttt{strang\allowbreak Composition}, \texttt{stepNL\_\allowbreak preserves\_\allowbreak base\_\allowbreak casimir}, \texttt{strang\_\allowbreak exact\_\allowbreak casimir\_\allowbreak preservation}, \texttt{strang\_\allowbreak time\_\allowbreak reversibility}: 4-step Strang Casimir invariance \& reversibility (\texttt{10 / 5}) & \S\ref{sec:algorithmic_recipe} (Thm.~\ref{thm:casimir_preservation}, Prop.~\ref{prop:strang_time_reversibility}) \\
 & \texttt{05\_\allowbreak HeavyTop\_\allowbreak Defs.lean}, \texttt{06\_\allowbreak HeavyTop\_\allowbreak Theorems.lean} & \texttt{HeavyTop\allowbreak State}, \texttt{conormal\allowbreak TorqueKick}, \texttt{rodrigues\allowbreak Isometry}, \texttt{heavy\_\allowbreak top\_\allowbreak strang\_\allowbreak casimirs\_\allowbreak exact}, \texttt{heavy\_\allowbreak top\_\allowbreak strang\_\allowbreak rodrigues\_\allowbreak casimirs\_\allowbreak exact}: Exact $\mathfrak{se}(3)^*$ Casimirs $C_1 = \|\boldsymbol{\Gamma}\|^2$, $C_2 = \mathbf{\Pi}\cdot\boldsymbol{\Gamma}$ (\texttt{17 / 7}) & \S\ref{sec:retrospective_cases} (Prop.~\ref{prop:heavy_top_casimirs}) \\
\midrule
\textbf{\texttt{Ch03\_3Body}} & \texttt{01\_\allowbreak PCR3BP\allowbreak Hamiltonian\_\allowbreak Theorems.lean} & \texttt{jacobi\_\allowbreak conservation\_\allowbreak identity}, \texttt{coriolis\_\allowbreak step\_\allowbreak symplectic}: Autonomous synodic Jacobi integral $\dot{C}_J \equiv 0$ \& exact $\operatorname{Sp}(4)$ Coriolis propagator (\texttt{5 / 2}) & \S\ref{sec:pcr3bp_canonical} (Prop.~\ref{prop:pcr3bp_jacobi}) \\
 & \texttt{02\_\allowbreak PCR3BP\allowbreak Regularization\_\allowbreak Theorems.lean} & \texttt{levi\_\allowbreak civita\_\allowbreak normal\_\allowbreak cone\_\allowbreak covering}, \texttt{levi\_\allowbreak civita\_\allowbreak antipodal\_\allowbreak covering}, \texttt{levi\_\allowbreak civita\_\allowbreak conformal\_\allowbreak scaling}: Double covering $z = u^2$, $\mathbb{Z}/2\mathbb{Z}$ fiber \& conformal factor $4|u|^2$ (\texttt{5 / 4}) & \S\ref{sec:classical_regularizations} (Thm.~\ref{thm:conormal_bridge}) \\
\midrule
\textbf{\texttt{Ch04\_FM}} & \texttt{01\_\allowbreak Partition\allowbreak Lattice\_\allowbreak Defs.lean}, \texttt{02\_\allowbreak Cluster\allowbreak HyperRadius\_\allowbreak Theorems.lean} & \texttt{collision\allowbreak Codimension}, \texttt{collision\_\allowbreak diagonal\_\allowbreak non\_\allowbreak transversality}, \texttt{hyperRadiusSq}, \texttt{newtonian\_\allowbreak potential\_\allowbreak is\_\allowbreak homogeneous}, \texttt{mcgehee\_\allowbreak potential\_\allowbreak factorization}: $\Pi(N)$ codimension $3(k-1)$ \& hyper-radius $\rho_S$ (\texttt{13 / 8}) & \S\ref{sec:whitney_lattice} (Thm.~\ref{thm:fulton_macpherson_snc}) \\
 & \texttt{03\_\allowbreak MaximalFlag\allowbreak JacobiTree\_\allowbreak Theorems.lean}, \texttt{04\_\allowbreak Disjoint\allowbreak Cotangent\allowbreak Commutation\_\allowbreak Theorems.lean} & \texttt{Binary\allowbreak ClusterTree}, \texttt{jacobi\_\allowbreak node\_\allowbreak exact\_\allowbreak union}, \texttt{jacobi\_\allowbreak node\_\allowbreak defines\_\allowbreak hierarchy}, \texttt{disjoint\_\allowbreak cotangent\_\allowbreak commutation\_\allowbreak local}: Nested flags on $\mathbf{Q}[N]$ \& $\{H_{\mathrm{leaf}}^{(S_1)}, H_{\mathrm{leaf}}^{(S_2)}\} = 0$ (\texttt{12 / 8}) & \S\ref{sec:whitney_lattice} (Prop.~\ref{prop:disjoint_cotangent_commutation}) \\
\bottomrule
\end{tabular}%
}
\end{table}

\newpage
\begin{table}[!htbp]
\centering
\caption{Module-by-module locator for the companion Lean~4 formalization (\texttt{lean4/NormalConeNBody/}, Part~II: Sections~\ref{ch:ch04_fulton_macpherson_splitting}--\ref{ch:ch05_higher_order_symplectic}, Modules \texttt{19}--\texttt{35}, and the 5 self-contained kernel compilation suites \texttt{CertifiedSuites/Sec01..05.lean}).}
\label{tab:lean4_module_locator_part2}
\scriptsize
\renewcommand{\arraystretch}{0.94}
\resizebox{\textwidth}{!}{%
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.14\textwidth}>{\raggedright\arraybackslash}p{0.29\textwidth}>{\raggedright\arraybackslash}p{0.49\textwidth}>{\raggedright\arraybackslash}p{0.12\textwidth}@{}}
\toprule
\textbf{Sub-Package} & \textbf{Module Path (\texttt{NormalConeNBody/...})} & \textbf{Formal Structures, Definitions \& Certified Theorems (\texttt{Decls / Thms})} & \textbf{Scope} \\
\midrule
\textbf{\texttt{Ch04\_FM}} \textit{(cont.)} & \texttt{01\_\allowbreak ApexUniversal\allowbreak LipschitzBound\_\allowbreak Theorems.lean} & \texttt{Conormal\allowbreak Regime}, \texttt{AdaptedChart\allowbreak ApexData}, \texttt{apexGradBound}, \texttt{apexHessBound}, \texttt{apex\_\allowbreak universal\_\allowbreak lipschitz\_\allowbreak bound}: Global $\mathcal{C}^{1,1}$ Lipschitz \& Hessian bounds of $W_{\mathrm{apex}}^{\mathrm{screen}}$ (\texttt{9 / 3}) & \S\ref{sec:screened_apex} (Thm.~\ref{thm:universal_c11_apex}) \\
 & \texttt{02\_\allowbreak LieBargmann\allowbreak ExactInvariance\_\allowbreak Theorems.lean}, \texttt{03\_\allowbreak Extended\allowbreak Palindromic\allowbreak Symplecticity\_\allowbreak Theorems.lean} & \texttt{LieBargmann\allowbreak Generators}, \texttt{lie\_\allowbreak bargmann\_\allowbreak exact\_\allowbreak invariance}, \texttt{Extended\allowbreak PhasePoint}, \texttt{extended\_\allowbreak palindromic\_\allowbreak symplecticity}: Exact 10-generator Galilean invariance \& Poincaré--Sundman symplecticity (\texttt{15 / 7}) & \S\ref{sec:screened_apex} (Props.~\ref{prop:lie_bargmann_preservation}, \ref{prop:extended_palindromic_symplecticity}) \\
 & \texttt{01\_\allowbreak Unified\allowbreak SuperNodeDef\_\allowbreak Theorems.lean}, \texttt{02\_\allowbreak SuperNode\allowbreak AntiZeno\allowbreak Regularization\_\allowbreak Theorems.lean} & \texttt{isCompact\allowbreak Cluster}, \texttt{super\_\allowbreak node\_\allowbreak time\_\allowbreak step\_\allowbreak sq\_\allowbreak pos}, \texttt{Unfolded\allowbreak SundmanState}, \texttt{keplerian\_\allowbreak conormal\_\allowbreak time\_\allowbreak scaling}, \texttt{super\_\allowbreak node\_\allowbreak anti\_\allowbreak zeno\_\allowbreak regularization}: Unfolded Sundman clock \& Anti-Zeno bound (\texttt{9 / 5}) & \S\ref{sec:synchronous_supernodes} (Thm.~\ref{thm:anti_zeno_regularization}) \\
 & \texttt{03\_\allowbreak AtlasTransition\allowbreak Symplectic\allowbreak AntiChattering\_\allowbreak Theorems.lean} & \texttt{Jacobi\allowbreak Transition\allowbreak Matrix2x2}, \texttt{jacobi\_\allowbreak transition\_\allowbreak matrix\_\allowbreak in\_\allowbreak sl2}, \texttt{cotangent\_\allowbreak lift\_\allowbreak preserves\_\allowbreak darboux}, \texttt{atlas\_\allowbreak transition\_\allowbreak symplectic\_\allowbreak anti\_\allowbreak chattering}: $\mathrm{SL}(2,\R)$ chart transitions \& dwell-time bound (\texttt{9 / 5}) & \S\ref{sec:synchronous_supernodes} (Thm.~\ref{thm:atlas_transition_anti_chattering}) \\
\midrule
\textbf{\texttt{Ch05\_Schemes}} & \texttt{01\_\allowbreak StrangOrderTwo\allowbreak Symplectic\_\allowbreak Theorems.lean} & \texttt{StrangOrderTwo\allowbreak Symplectic\allowbreak Certificate}, \texttt{strang\_\allowbreak order\_\allowbreak two\_\allowbreak symplectic\_\allowbreak theorem}: 7-stage palindromic Strang $\mathcal{S}_2(h)$ extended symplecticity \& odd BCH parity (\texttt{17 / 7}) & \S\ref{sec:strang_propagator} (Thm.~\ref{thm:strang_extended_symplecticity}) \\
 & \texttt{02\_\allowbreak LieBargmann\allowbreak Conservation\_\allowbreak Theorems.lean} & \texttt{LieBargmann\allowbreak Conservation\allowbreak Certificate}, \texttt{lie\_\allowbreak bargmann\_\allowbreak conservation\_\allowbreak theorem}: Exact discrete Noether conservation of all 10 Lie--Bargmann generators under $\mathcal{S}_2$ (\texttt{22 / 12}) & \S\ref{sec:strang_propagator} (Prop.~\ref{prop:strang_bch_parity_bargmann}) \\
 & \texttt{01\_\allowbreak YoshidaOrderFour\allowbreak Suzuki\_\allowbreak Theorems.lean} & \texttt{YoshidaSuzuki\allowbreak Certificate}, \texttt{yoshida\_\allowbreak order\_\allowbreak four\_\allowbreak suzuki\_\allowbreak theorem}: Sheng--Suzuki negative-step necessity ($w_0 < 0$), unitary McGehee involution $\mathcal{B}_C^2 = \mathrm{Id}$, and 4th-order Yoshida $\mathcal{S}_4$ (\texttt{7 / 4}) & \S\ref{sec:suzuki_barrier_mcgehee} (Thm.~\ref{thm:sheng_suzuki_barrier}, Lem.~\ref{thm:mcgehee_bounce_unitary}) \\
 & \texttt{01\_\allowbreak BlanesMoan\allowbreak Shadow\allowbreak Confinement\_\allowbreak Theorems.lean} & \texttt{BlanesMoan\allowbreak Shadow\allowbreak Confinement\allowbreak Certificate}, \texttt{blanes\_\allowbreak moan\_\allowbreak shadow\_\allowbreak confinement\_\allowbreak certified}: 7-stage $\mathrm{BM}_4^{(7)}$ cubic order cancellation ($|C_5| \le 0.01236$) \& shadow Hamiltonian confinement (\texttt{10 / 8}) & \S\ref{sec:bm4_seven_stages} (Thms.~\ref{thm:bm4_error_minimization}, \ref{thm:unsoftened_shadow_confinement}) \\
 & \texttt{01\_\allowbreak BlanesMoan\allowbreak OrderSix\_\allowbreak Theorems.lean} & \texttt{BlanesMoan\allowbreak OrderSix\allowbreak Certificate}, \texttt{blanes\_\allowbreak moan\_\allowbreak order6\_\allowbreak certified}: 11-stage $\mathrm{BM}_6^{(11)}$ order-6 RKN consistency, $\operatorname{ad}_{W}^3(A_{\mathrm{JK}}) \equiv 0$ nilpotence, and $\mathcal{O}(h^6 t)$ phase bound (\texttt{63 / 23}) & \S\ref{sec:bm6_eleven_stages} (Thms.~\ref{thm:bm6_order_conditions}, \ref{thm:bm6_shadow_confinement}) \\
 & \texttt{01\_\allowbreak CorrectorBM4\_\allowbreak Theorems.lean} & \texttt{ConeNormal\allowbreak Corrector\allowbreak Certificate}, \texttt{cone\_\allowbreak normal\_\allowbreak corrector\_\allowbreak bm4\_\allowbreak certified}: 2-stage palindromic Lie conjugator $\mathcal{Z}_4^{\mathrm{BM4}}(h)$, antipodal node/kick weights, and exact invertibility (\texttt{59 / 26}) & \S\ref{sec:symplectic_correctors} (Thm.~\ref{thm:c4_corrector_solvability}) \\
 & \texttt{03\_\allowbreak Conormal\allowbreak Corrector\allowbreak PBM4\_\allowbreak Order6.lean} & \texttt{pbm4\_\allowbreak order6\_\allowbreak single\_\allowbreak chart\_\allowbreak cancellation}, \texttt{cotangent\_\allowbreak generator\_\allowbreak K4\_\allowbreak solves\_\allowbreak homological}: Homological equation $D_A K_4 = h^4 H_5^{\mathrm{linear}}$ via $K_4 = c_4^{\mathrm{BM4}} h^4 D_A^3 B \in \mathcal{P}_1$ \& torque-free cancellation (\texttt{22 / 13}) & \S\ref{sec:symplectic_correctors} (Thms.~\ref{thm:c4_corrector_solvability}, \ref{thm:asymptotic_conormal_scaling}) \\
 & \texttt{06\_\allowbreak ConormalGauge\allowbreak Transition\allowbreak PBM4\_\allowbreak Order6.lean} & \texttt{pbm4\_\allowbreak gauge\_\allowbreak transition\_\allowbreak cocycle}, \texttt{abelian\_\allowbreak P0\_\allowbreak gauge\_\allowbreak specialization}: Non-commutative gauge connection $T_{A\to B}^{(\mathrm{PBM4})} = (\mathcal{Z}_4^{(B)})^{-1}\circ\mathbf{M}_{A\to B}\circ\mathcal{Z}_4^{(A)}$ \& \v{C}ech 1-cocycle closure (\texttt{14 / 11}) & \S\ref{sec:symplectic_correctors} (Thm.~\ref{thm:pbm4_gauge_operator_exact}) \\
 & \texttt{07\_\allowbreak GlobalConormal\allowbreak Corrector\allowbreak PBM4\_\allowbreak Order6.lean} & \texttt{global\_\allowbreak pbm4\_\allowbreak atlas\_\allowbreak gauge\_\allowbreak invariance}: Global atlas gauge-invariance of processed $\mathrm{PBM}_4$ trajectories across multi-chart Jacobi tree transitions (\texttt{17 / 13}) & \S\ref{sec:symplectic_correctors} (Thm.~\ref{thm:pbm4_gauge_operator_exact}) \\
 & \texttt{08\_\allowbreak Universal\allowbreak OrderSix\allowbreak Obstruction.lean} & \texttt{parity\_\allowbreak obstruction\_\allowbreak P0\_\allowbreak impossible}, \texttt{hall\_\allowbreak L52\_\allowbreak cohomological\_\allowbreak obstruction}, \texttt{universal\_\allowbreak double\_\allowbreak obstruction\_\allowbreak order6}: Momentum-parity obstruction ($\operatorname{Im}(D_A|_{\mathcal{P}_0})\subseteq\mathcal{P}_1$) \& Hall class $[D_B D_A^3 B] \in H^1(D_A,\mathcal{L}_{5,2})\cong\R$ (\texttt{18 / 13}) & \S\ref{sec:symplectic_correctors} (Thm.~\ref{thm:universal_order6_obstruction}) \\
\midrule
\textbf{\texttt{Certified\allowbreak Suites}} & \texttt{Sec01\_\allowbreak Introduction.lean}, \texttt{Sec02\_\allowbreak NormalCone.lean}, \texttt{Sec03\_\allowbreak ThreeBody.lean} & Self-contained Lake compilation units for Sections~\ref{ch:ch01_introduction}--\ref{ch:ch03_three_body_paradigm} with automated \texttt{\#print axioms} verification confirming exclusive reliance on \texttt{[propext, Classical.choice, Quot.sound]} (\texttt{0 sorryAx}) & \S\ref{ch:ch01_introduction}--\S\ref{ch:ch03_three_body_paradigm} \\
 & \texttt{Sec04\_\allowbreak Fulton\allowbreak MacPherson.lean}, \texttt{Sec05\_\allowbreak Symplectic\allowbreak Schemes.lean} & Self-contained Lake compilation units for Sections~\ref{ch:ch04_fulton_macpherson_splitting}--\ref{ch:ch05_higher_order_symplectic} \& \texttt{lean4/scripts/verify\_\allowbreak lean4\_\allowbreak suite.py} (\texttt{35/35} modules certified, \texttt{99} axiom audits, \texttt{0 sorryAx}) & \S\ref{ch:ch04_fulton_macpherson_splitting}--\S\ref{ch:ch05_higher_order_symplectic} \\
\bottomrule
\end{tabular}%
}
\end{table}

% ==============================================================================
% SUBSECTION A.2 : PYTHON DUAL-PRECISION & BENCHMARK REPOSITORY LOCATOR
% ==============================================================================
\newpage
\subsection{Companion Dual-Precision Python Engine and Benchmark Suite (\texttt{normal\_\allowbreak cone\_\allowbreak nbody\_\allowbreak float64} \& \texttt{normal\_\allowbreak cone\_\allowbreak nbody\_\allowbreak float128})}
\label{app:github_benchmark_suite}
\label{app:arenstorf_solver_sec}
\label{app:pcr3bp_synodic_solver}
\label{app:global_pipeline}
\label{app:global_pipeline_interfaces}
\label{app:initialization_shadow}
\label{app:init_shadow_interfaces}
\label{app:dyadic_scheduler}
\label{app:dyadic_scheduler_interfaces}
\label{app:symplectic_subcycle}
\label{app:symplectic_subcycle_interface}
\label{app:atlas_transitions_diagnostics}
\label{app:atlas_transitions_interface}
\label{app:computational_optimizations}
\label{app:computational_optimizations_interface}
\label{app:py_core}
\label{app:py_geometry}
\label{app:py_kernels}
\label{app:py_physics}
\label{app:py_hierarchy}
\label{app:py_integrators}
\label{app:py_system}
\label{app:py_interfaces}
\label{app:py_bench_ch03}
\label{app:py_bench_ch06}
\label{app:py_bench_gen01}
\label{app:py_bench_gen02}
\label{app:py_bench_gen03}
\label{app:py_bench_gen04}
\label{app:py_bench_gen05}
\label{app:py_bench_rebound}

{\emergencystretch=1.5em
Complementing the formal proof index of \S\ref{app:config_defs_sec}, this subsection presents the directory hierarchy and module-by-module index of the dual-precision computational and benchmark suites in the companion repository (\href{https://github.com/jeremynusa-hub/normal_cone_nbody3d}{\texttt{jeremynusa-hub/\allowbreak normal\_cone\_nbody3d}}, \href{https://doi.org/10.5281/zenodo.23982968}{\texttt{DOI:~10.5281/\allowbreak zenodo.23982968}}). Every \texttt{Python} badge throughout Sections~\ref{ch:ch01_introduction}--\ref{ch:ch07_benchmarks_and_lean4} links directly to this architectural guide so that any reader can immediately locate the exact production module, Numba \texttt{@njit} micro-kernel, campaign runner, figure plotter, or certified dataset of interest.\par}

\paragraph{1. Global Repository Directory Tree.}
{\emergencystretch=1.5em
The repository unites the self-contained \textbf{Lean~4 + Mathlib~4 formal proof package} (\texttt{lean4/}, 35 modules indexed in Tables~\ref{tab:lean4_module_locator_part1}--\ref{tab:lean4_module_locator_part2} and 5 chapter suites with \texttt{0 sorryAx}) and two strictly mirrored dual-precision Python engines (\texttt{normal\_\allowbreak cone\_\allowbreak nbody\_\allowbreak float64/}, IEEE~754 double precision with Numba \texttt{@njit(fastmath=False)} micro-kernels, and \texttt{normal\_\allowbreak cone\_\allowbreak nbody\_\allowbreak float128/}, 116-bit / 35-digit quadruple precision via \texttt{mpmath}/\texttt{gmpy2}), paired with 3-tier reproducibility scripts (\texttt{scripts/}), section interfaces (\texttt{interfaces/}), campaign runners (\texttt{benchmarks/}), figure plotters (\texttt{figures/}), certified datasets (\texttt{results/\allowbreak campaigns/}), unit test suites (\texttt{tests/}, 330 tests), and archival metadata (\texttt{CITATION.cff}, \texttt{.zenodo.json}, \texttt{LICENSE} \texttt{CC BY-NC-SA 4.0}, \texttt{.github/\allowbreak workflows/\allowbreak ci.yml}):\par}

\begin{tcolorbox}[
    enhanced,
    colback=BadgeGray,
    colframe=PythonSlate,
    boxrule=0.6pt,
    arc=2pt,
    left=6pt, right=6pt, top=3.5pt, bottom=3.5pt,
    title={\footnotesize\sffamily\bfseries Companion Archive (\href{https://github.com/jeremynusa-hub/normal_cone_nbody3d}{\textcolor{white}{\texttt{normal\_cone\_nbody3d}}} \,|\, \texttt{v1.0.0} \,|\, \href{https://doi.org/10.5281/zenodo.23982968}{\textcolor{white}{\texttt{DOI:~10.5281/zenodo.23982968}}})},
    coltitle=white,
    colbacktitle=PythonSlate,
    fonttitle=\footnotesize\sffamily\bfseries
]
\scriptsize
\renewcommand{\arraystretch}{0.96}
\begin{tabular}{@{}>{\ttfamily\raggedright\arraybackslash}p{0.40\textwidth}>{\sffamily\raggedright\arraybackslash}p{0.57\textwidth}@{}}
\textbf{normal\_cone\_nbody3d\_github/} & \textcolor{DarkSlate}{(Root directory of the companion formal \& dual-precision archive)} \\
|-- README.md, pyproject.toml, LICENSE & \textcolor{DarkSlate}{(Traceability matrix, PEP 621 / Conda specs \& \texttt{CC BY-NC-SA 4.0} license)} \\
|-- CITATION.cff, .zenodo.json, .github/ & \textcolor{DarkSlate}{(Zenodo/GitHub citation metadata \& CI: Lean 4 \texttt{0-sorryAx} + \texttt{pytest})} \\
|-- \textbf{scripts}/ & \texttt{reproduce\_figures.py} \textcolor{DarkSlate}{(Tier 1)}, \texttt{run\_smoke\_tests.py} \textcolor{DarkSlate}{(Tier 2)}, \texttt{run\_full\_campaigns.py} \\
|-- \textbf{lean4}/ & \textcolor{PythonSlate}{\textbf{[Lean 4 (\texttt{v4.35.0-rc2}) + Mathlib 4 Formal Proof Suite --- \S\ref{app:config_defs_sec}, Tables~\ref{tab:lean4_module_locator_part1}--\ref{tab:lean4_module_locator_part2}]}} \\
|   `-- NormalConeNBody/, lakefile.lean & \texttt{Ch01..05/} \textcolor{DarkSlate}{(35 modules, 416 decls, 214 thms)}, \texttt{CertifiedSuites/Sec01..05.lean} \textcolor{DarkSlate}{(0 \texttt{sorryAx})} \\
|-- \textbf{normal\_cone\_nbody\_float64}/ & \textcolor{PythonSlate}{\textbf{[IEEE-754 Float64 + Numba \texttt{@njit} Production Engine --- 46 modules]}} \\
|   |-- core/ & \texttt{state.py}, \texttt{jacobi.py}, \texttt{coordinates.py}, \texttt{invariants.py}, \texttt{transitions.py}, \texttt{constants.py}, \texttt{profiler.py} \\
|   |-- potential/ & \texttt{screened\_apex.py}, \textbf{\texttt{optimized\_screened\_apex.py}} \textcolor{PythonSlate}{(\texttt{@njit})}, \texttt{screening.py}, \texttt{supernode\_detector.py}, \texttt{direct.py} \\
|   |-- solvers/ & \texttt{stumpff.py}, \texttt{kepler\_sundman.py}, \textbf{\texttt{optimized\_kepler\_sundman.py}}, \texttt{supernode.py}, \textbf{\texttt{optimized\_supernode.py}}, \textbf{\texttt{jit\_supernode.py}} \textcolor{PythonSlate}{(\texttt{@njit})} \\
|   |-- integrators/ & \textbf{\texttt{common.py}} \textcolor{PythonSlate}{(\texttt{ContextVar} dispatch)}, \texttt{strang.py}, \texttt{yoshida.py}, \texttt{yoshida4.py}, \texttt{blanes\_moan\_4.py}, \texttt{blanes\_moan\_6.py}, \texttt{correctors.py}, \texttt{processed.py}, \texttt{protocol.py} \\
|   |-- system/ & \texttt{nbody\_system.py}, \texttt{atlas\_manager.py}, \texttt{dyadic\_scheduler.py}, \texttt{history.py} \\
|   |-- diagnostics/ & \texttt{metrics.py}, \texttt{collision\_radar.py}, \texttt{radar.py}, \texttt{profiler.py}, \texttt{visualizer.py} \\
|   `-- benchmarks/ & \texttt{registry.py}, \texttt{runner.py} \textcolor{DarkSlate}{(\texttt{BenchmarkRunner} with \texttt{use\_optimized\_kernels} toggle)} \\
|-- \textbf{normal\_cone\_nbody\_float128}/ & \textcolor{PythonSlate}{\textbf{[116-Bit / 35-Digit Float128 Mirror Engine --- 46 modules]}} \\
|   `-- core/ .. benchmarks/ & \textcolor{DarkSlate}{(Exact 1-to-1 structural mirror of all 7 sub-packages of \texttt{normal\_cone\_nbody\_float64/} in 35-digit \texttt{mpmath}/\texttt{gmpy2} arithmetic)} \\
|-- \textbf{interfaces}/ & \texttt{pcr3bp\_canonical\_solver.py}, \texttt{01..06\_*\_Interface.py} \textcolor{DarkSlate}{(Standalone facades for \S 3 \& \S 6)} \\
|-- \textbf{benchmarks}/ & \texttt{run\_generator\_01..05\_*.py}, \texttt{run\_rebound\_b1..b4\_*.py}, \texttt{run\_L1..L4\_*.py}, \texttt{run\_H1..H3\_*.py}, \texttt{run\_S1..S2\_*.py}, \texttt{contracts/00..05\_*.md} \\
|-- \textbf{figures}/ & \texttt{plot\_generator\_01..05\_*.py}, \texttt{plot\_rebound\_b1..b4\_*.py} \textcolor{DarkSlate}{(Publication figure generators)} \\
|-- \textbf{results/campaigns}/ & \texttt{generator\_01..05\_*.json}, \texttt{campaign\_II\_H1..H3\_*.json}, \texttt{rebound\_b1..b4\_*.json} \textcolor{DarkSlate}{(14 JSONs)} \\
`-- \textbf{tests}/ & \texttt{unit/} \textcolor{DarkSlate}{(265 Float64 \& interface tests)}, \texttt{unit\_float128/} \textcolor{DarkSlate}{(65 Float128 tests --- 330/330 PASS)}
\end{tabular}
\end{tcolorbox}

\newpage
\paragraph{2. Architectural Index of the Core Packages and Optimized Micro-Kernels (\texttt{normal\_\allowbreak cone\_\allowbreak nbody\_\allowbreak float64} \& \texttt{normal\_\allowbreak cone\_\allowbreak nbody\_\allowbreak float128}).}
Table~\ref{tab:github_core_module_locator} details every sub-package, reference module, and accelerated \texttt{@njit} micro-kernel inside \texttt{normal\_\allowbreak cone\_\allowbreak nbody\_\allowbreak float64/} and \texttt{normal\_\allowbreak cone\_\allowbreak nbody\_\allowbreak float128/}, mapping its primary classes and functions to the theoretical definitions, theorems, and optimization tiers of Sections~\ref{ch:ch01_introduction}--\ref{ch:ch06_algorithmic_architecture}.

\begin{table}[!htbp]
\centering
\caption{Module-by-module architectural locator for the dual-precision core packages \texttt{normal\_cone\_nbody\_float64/} and \texttt{normal\_cone\_nbody\_float128/}, the four high-performance micro-kernel modules (\S\ref{sec:computational_optimizations}), and the standalone \texttt{interfaces/} directory.}
\label{tab:github_core_module_locator}
\scriptsize
\renewcommand{\arraystretch}{0.96}
\resizebox{\textwidth}{!}{%
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.11\textwidth}>{\raggedright\arraybackslash}p{0.25\textwidth}>{\raggedright\arraybackslash}p{0.62\textwidth}>{\raggedright\arraybackslash}p{0.16\textwidth}@{}}
\toprule
\textbf{Sub-Package} & \textbf{Module Path (\texttt{64} \& \texttt{128})} & \textbf{Key Classes, Functions \& Mathematical / Algorithmic Role} & \textbf{Manuscript Scope} \\
\midrule
\textbf{\texttt{core/}} & \texttt{core/state.py}, \texttt{constants.py} & \texttt{ExtendedPhaseState}: Immutable phase state $(\mathbf{q}, \mathbf{p}, t, E) \in \mathcal{P}_{\mathrm{ext}}$, barycentric reduction $\mathbf{R}_{\mathrm{cm}} = \mathbf{0}, \mathbf{P}_{\mathrm{tot}} = \mathbf{0}$ & \S\ref{sec:global_pipeline}, \S\ref{sec:initialization_shadow} \\
 & \texttt{core/jacobi.py}, \texttt{coordinates.py} & \texttt{JacobiNode}, \texttt{JacobiTree}, \texttt{build\_optimal\_tree}: Maximal flag binary tree $\mathcal{T} \in \operatorname{Trees}(N)$, recursive Jacobi coordinates $(\mathbf{r}_v, \mathbf{w}_v)$, hyper-radius $\rho_C$, and Delaunay--Hill agglomeration ($\gamma = 1.0$) & \S\ref{sub:maximal_flag_jacobi_trees}, \S\ref{sec:initialization_shadow} \\
 & \texttt{core/invariants.py} & \texttt{compute\_lie\_bargmann\_\allowbreak invariants}: 10 Galilean Noether generators $(\mathbf{P}_{\mathrm{tot}}, \mathbf{L}_{\mathrm{tot}}, \mathbf{G}_{\mathrm{Gal}}, H)$ and Battin Wronskian audit $|f\dot{g} - \dot{f}g - 1|$ & \S\ref{sub:lie_bargmann_and_palindromy} (Prop.~\ref{prop:lie_bargmann_closure}), \S\ref{sec:atlas_transitions_diagnostics} \\
 & \texttt{core/transitions.py} & \texttt{apply\_jacobi\_\allowbreak transition}, \texttt{compute\_sl2\_\allowbreak matrix}: Exact unimodular $\mathrm{SL}(2,\R) \hookrightarrow \operatorname{Sp}(6N-6,\R)$ chart transition $\mathbf{M}_{A\to B}$ & \S\ref{sub:symplectic_atlas_anti_chattering} (Thm.~\ref{thm:atlas_transition_anti_chattering}), \S\ref{sec:atlas_transitions_diagnostics} \\
\midrule
\textbf{\texttt{potential/}} & \texttt{potential/screened\_\allowbreak apex.py}, \texttt{screening.py}, \texttt{direct.py} & \texttt{ScreenedApexPotential}, \texttt{septic\_screening\_theta}: Reference $\mathcal{C}^{1,1}$ screened apex potential $W_{\mathrm{apex}}^{\mathrm{screen}}$, exact monopole cancellation $+W_v - W_v \equiv 0$, and Cauchy / Hermite $\mathcal{C}^{2p}$ splines $\Theta(u_v)$ on $u_v \in [1, 2]$ & \S\ref{sec:screened_apex} (Thm.~\ref{thm:universal_c11_apex}), \S\ref{sec:symplectic_subcycle} \\
 & \textbf{\texttt{potential/optimized\_\allowbreak screened\_apex.py}} & \textbf{[Optimized Tier 1]} \texttt{OptimizedScreenedApexPotential}, \texttt{\_njit\_accumulate\_\allowbreak apex\_pairs}: Precomputed $\mathbf{G}_{\mathrm{mass}}$, topological non-leaf/non-intra-supernode pair cache $(\mathbf{idx}_A, \mathbf{idx}_B)$, scalar $N=3$ fast-path ($7.24\times$) and Numba \texttt{@njit(fastmath=False)} loop ($62.54\times$ at $N=64$, $0.0\text{ ULP}$) & \S\ref{sub:vectorized_apex_kick} (Prop.~\ref{prop:apex_acceleration_invariance}, Table~\ref{tab:optimization_performance_synthesis}) \\
 & \texttt{potential/supernode\_\allowbreak detector.py} & \texttt{SupernodeDetector}: Hill tidal ratio $\eta_S$ with Schmitt trigger $[2^{-1/3}, 2^{-1/6}]$, internal hierarchy ratio $\chi_S < 3.0$, and sub-Roche disruption mode $\Lambda_S \ge 0.25$ & \S\ref{sec:synchronous_supernodes}, \S\ref{sec:initialization_shadow} (Thm.~\ref{thm:spectral_schmitt_trigger}) \\
\midrule
\textbf{\texttt{solvers/}} & \texttt{solvers/stumpff.py}, \texttt{kepler\_sundman.py} & \texttt{KeplerSundmanSolver}, \texttt{stumpff\_c012345}: Reference universal Sundman--Stumpff leaf flow $\Phi_{\Delta t}^{\mathrm{leaf}}$, cubic Halley + 60-step bisection fallback, Battin Wronskian projection, and McGehee bounce $\mathcal{B}_C^2 = \mathrm{Id}$ & \S\ref{sub:sundman_stumpff_diffeomorphism}, \S\ref{sub:mcgehee_bounce_unitary} (Lem.~\ref{thm:mcgehee_bounce_unitary}), \S\ref{sec:symplectic_subcycle} \\
 & \textbf{\texttt{solvers/optimized\_\allowbreak kepler\_sundman.py}} & \textbf{[Optimized Tier 2]} \texttt{OptimizedKeplerSolver}, \texttt{stumpff\_c0123\_\allowbreak scalar}, \texttt{step\_kepler\_\allowbreak sundman\_fast}: Targeted $2\times 6$ Horner polynomials on $c_2, c_3$ with exact Stumpff recurrence, closure-free inlined Halley loop, and direct Gauss--Battin reuse ($1.62\times$ speedup, $0.0\text{ ULP}$) & \S\ref{sub:inlined_kepler_sundman_drift} (Rem.~\ref{rem:kepler_fast_invariants}, Table~\ref{tab:optimization_performance_synthesis}) \\
 & \texttt{solvers/supernode.py} & \texttt{SupernodeSolver}: Reference synchronous supernode flow under unfolded Sundman clock $\mathrm{d}t_S = \bar{\rho}_S\mathrm{d}\tau_S$ and recursive normal-cone splitting $H_S^{\mathrm{int}} = H_{\mathrm{leaf}}^{\mathrm{int}} + H_{\mathrm{base}}^{\mathrm{int}} + V_{\mathrm{apex}}^{\mathrm{int}}$ & \S\ref{sec:synchronous_supernodes} (Thm.~\ref{thm:anti_zeno_regularization}), \S\ref{sec:symplectic_subcycle} \\
 & \textbf{\texttt{solvers/optimized\_\allowbreak supernode.py}}, \textbf{\texttt{jit\_supernode.py}} & \textbf{[Optimized Tiers 3 \& 4]} \texttt{OptimizedSupernodeSolver} (zero-alloc unrolled $k \le 4$ loops) and \texttt{JitSupernodeSolver} / \texttt{\_njit\_integrate\_\allowbreak supernode} (native LLVM \texttt{@njit} compilation, symmetric dyadic bisection stack with half-step pair bridge, $L^2(\bar{\rho}_S)$ filter, $59.83\times$ speedup, $0.0\text{ ULP}$) & \S\ref{sub:zero_alloc_jit_supernodes} (Prop.~\ref{prop:supernode_jit_performance}, Table~\ref{tab:optimization_performance_synthesis}) \\
\midrule
\textbf{\texttt{integrators/}} & \textbf{\texttt{integrators/common.py}}, \texttt{protocol.py} & \textbf{[Optimized Tier 5]} Thread-local \texttt{ContextVar} dispatchers (\texttt{\_CURRENT\_APEX\_EVALUATOR}, \texttt{\_CURRENT\_KEPLER\_SOLVER}, \texttt{\_CURRENT\_SUPERNODE\_SOLVER}) inside \texttt{step\_drift\_and\_kepler}, \texttt{step\_apex\_kick}, and \texttt{step\_supernode\_flow} & \S\ref{sub:contextvar_modular_dispatch} (Table~\ref{tab:optimization_performance_synthesis}) \\
 & \texttt{integrators/strang.py}, \texttt{yoshida.py}, \texttt{blanes\_moan\_4.py}, \texttt{blanes\_moan\_6.py} & \texttt{StrangIntegrator} ($\mathcal{S}_2$), \texttt{Yoshida4Integrator} ($\mathcal{S}_4$), \texttt{BlanesMoan4Integrator} ($\mathrm{BM}_4^{(7)}$, 7 stages, $s=6$), and \texttt{BlanesMoan6Integrator} ($\mathrm{BM}_6^{(11)}$, 11 stages, $s=10$, 25-digit weights) & \S\ref{sec:strang_propagator}--\S\ref{sec:bm6_eleven_stages} (Thms.~\ref{thm:strang_extended_symplecticity}, \ref{thm:bm4_error_minimization}, \ref{thm:bm6_order_conditions}) \\
 & \texttt{integrators/correctors.py}, \texttt{processed.py} & \texttt{PalindromicCorrectorZ4}, \texttt{ProcessedBM4Integrator} ($\mathrm{PBM}_4$): Cotangent generator $K_4 = c_4^{\mathrm{BM4}} h^4 D_A^3 B \in \mathcal{P}_1$, 2-stage antipodal Lie conjugator $\mathcal{Z}_4^{\mathrm{BM4}}(h)$, and covariant gauge connection $T_{(A,h_A)\to(B,h_B)}^{(\mathrm{PBM4})}$ & \S\ref{sec:symplectic_correctors} (Thms.~\ref{thm:universal_order6_obstruction}, \ref{thm:c4_corrector_solvability}, \ref{thm:pbm4_gauge_operator_exact}) \\
\midrule
\textbf{\texttt{system/}} & \texttt{system/nbody\_system.py}, \texttt{atlas\_manager.py}, \texttt{dyadic\_scheduler.py}, \texttt{history.py} & \texttt{NBodySystem(use\_optimized\_kernels=...)}, \texttt{AtlasManager} (Voronoi $\gamma = 1.0$ / hysteresis $\gamma = 0.60$), and \texttt{DyadicScheduler} (two-endpoint symmetric selector $k_{\mathrm{sym},n}$, timescale triad \& Leaf/Apex decoupling) & \S\ref{sec:dyadic_multirate_scheduling}, \S\ref{sec:global_pipeline}, \S\ref{sec:dyadic_scheduler}, \S\ref{sec:atlas_transitions_diagnostics} \\
\midrule
\textbf{\texttt{diagnostics/}} \& \textbf{\texttt{interfaces/}} & \texttt{diagnostics/metrics.py}, \texttt{interfaces/pcr3bp\_*.py}, \texttt{01..06\_*\_Interface.py} & \texttt{SystemDiagnostics}, \texttt{CollisionRadar}, \texttt{PCR3BPNormalConeIntegrator} (\S\ref{ch:ch03_three_body_paradigm}), and standalone pedagogical facades (\texttt{01..06\_*\_Interface.py}) for \S\ref{sec:global_pipeline}--\S\ref{sec:computational_optimizations} & \S\ref{sec:pcr3bp_canonical}, \S\ref{sec:arenstorf_validation}, \S\ref{sec:global_pipeline}--\S\ref{sec:computational_optimizations} \\
\bottomrule
\end{tabular}%
}
\end{table}

\newpage
\paragraph{3. Reproducibility Index of Benchmark Campaigns, Figure Plotters, and Certified Datasets.}
Table~\ref{tab:github_benchmark_reproducibility} maps every numerical experiment, convergence table, and figure plate in Sections~\ref{ch:ch01_introduction}, \ref{ch:ch03_three_body_paradigm}, \ref{ch:ch06_algorithmic_architecture}, and~\ref{ch:ch07_benchmarks_and_lean4} to its corresponding execution script in \texttt{benchmarks/}, plotting script in \texttt{figures/}, and certified reference output in \texttt{results/campaigns/}.

\begin{table}[!htbp]
\centering
\caption{Benchmark campaign runners, publication figure generators, and certified JSON datasets in the companion GitHub repository.}
\label{tab:github_benchmark_reproducibility}
\scriptsize
\renewcommand{\arraystretch}{1.10}
\resizebox{\textwidth}{!}{%
\begin{tabular}{@{}>{\raggedright\arraybackslash}p{0.21\textwidth}>{\raggedright\arraybackslash}p{0.28\textwidth}>{\raggedright\arraybackslash}p{0.27\textwidth}>{\raggedright\arraybackslash}p{0.19\textwidth}@{}}
\toprule
\textbf{Manuscript Section, Figures \& Tables} & \textbf{Campaign Runner (\texttt{benchmarks/})} & \textbf{Figure Plotter (\texttt{figures/})} & \textbf{Certified JSON Output (\texttt{results/campaigns/})} \\
\midrule
\textbf{\S\ref{sec:arenstorf_validation}} Arenstorf Synodic Periodic Orbit Validation & \texttt{interfaces/\allowbreak pcr3bp\_canonical\_\allowbreak solver.py} & \texttt{interfaces/\allowbreak pcr3bp\_canonical\_\allowbreak solver.py} & \texttt{(Inline Arenstorf validation)} \\
\textbf{\S\ref{sec:computational_optimizations}} Table~\ref{tab:optimization_performance_synthesis} ($N \in [3, 64]$ Micro-Kernel Speedups) \& Fig.~\ref{fig:ch06_microkernel_performance_and_invariants} & \texttt{benchmarks/\allowbreak run\_generator\_01\_\allowbreak dual\_convergence\_\allowbreak and\_microkernels.py} & \texttt{figures/\allowbreak plot\_generator\_01\_\allowbreak dual\_convergence\_\allowbreak and\_microkernels.py} & \texttt{generator\_01\_\allowbreak dual\_convergence\_\allowbreak and\_microkernels.json} \\
\textbf{\S\ref{sub:laskar_dual_convergence}} Fig.~\ref{fig:laskar_dual_convergence} \& Table~\ref{tab:convergence_orders_table} (Figure-8 \& 3D Triple Dual Convergence) & \texttt{benchmarks/\allowbreak run\_generator\_01\_\allowbreak dual\_convergence\_\allowbreak and\_microkernels.py}, \texttt{run\_campaign\_IV\_\allowbreak convergence\_dual.py} & \texttt{figures/\allowbreak plot\_generator\_01\_\allowbreak dual\_convergence\_\allowbreak and\_microkernels.py} & \texttt{generator\_01\_\allowbreak dual\_convergence\_\allowbreak and\_microkernels.json} \\
\textbf{\S\ref{sub:pbm4_quadratic_floor_proof}} Fig.~\ref{fig:pbm4_quadratic_floor} (Order $6 \to 4$ Crossover \& $\mathcal{O}(\varepsilon^2 h^4)$ Floor) & \texttt{benchmarks/\allowbreak run\_generator\_02\_\allowbreak universal\_obstruction\_\allowbreak and\_shadow\_gauge.py}, \texttt{run\_pbm4\_vs\_bm4\_\allowbreak stress\_test.py} & \texttt{figures/\allowbreak plot\_generator\_02\_\allowbreak universal\_obstruction\_\allowbreak and\_shadow\_gauge.py} & \texttt{generator\_02\_\allowbreak universal\_obstruction\_\allowbreak and\_shadow\_gauge.json} \\
\textbf{\S\ref{sub:unsoftened_limit_cases}} Figs.~\ref{fig:l1_pericenter_conditioning}--\ref{fig:l4_adaptive_multiscale_burrau_kozai} \& Table~\ref{tab:campaign_I_kpi_table} (\texttt{L1}--\texttt{L4}: $e \to 1$, $\mathcal{Z}_4^{\mathrm{BM4}}$ Free-Fall, McGehee $k \in \{2,3,4\}$, Burrau/Kozai) & \texttt{benchmarks/\allowbreak run\_generator\_03\_\allowbreak unsoftened\_singularity\_\allowbreak limit\_cases.py}, \texttt{run\_L1\_eccentricity.py}, \texttt{run\_L2\_mcgehee.py}, \texttt{run\_L3\_burrau\_\allowbreak quadruple.py}, \texttt{run\_L4\_kozai\_lidov.py} & \texttt{figures/\allowbreak plot\_generator\_03\_\allowbreak unsoftened\_singularity\_\allowbreak limit\_cases.py} & \texttt{generator\_03\_\allowbreak unsoftened\_singularity\_\allowbreak limit\_cases.json} \\
\textbf{\S\ref{sub:historical_encounters_validation}} Figs.~\ref{fig:h1_lexell_atlas_gauge}--\ref{fig:h3_apophis_flyby_palindrome} \& Table~\ref{tab:campaign_II_kpi_table} (\texttt{H1} Lexell, \texttt{H2} SL9, \texttt{H3} Apophis) & \texttt{benchmarks/\allowbreak run\_generator\_04\_\allowbreak historical\_encounters\_\allowbreak and\_atlas\_gauge.py}, \texttt{run\_H1\_lexell.py}, \texttt{run\_H2\_shoemaker\_\allowbreak levy.py}, \texttt{run\_H3\_apophis.py} & \texttt{figures/\allowbreak plot\_generator\_04\_\allowbreak historical\_encounters\_\allowbreak and\_atlas\_gauge.py} & \texttt{generator\_04\_\allowbreak historical\_encounters\_\allowbreak and\_atlas\_gauge.json}, \texttt{campaign\_II\_\allowbreak H1..H3\_*.json} \\
\textbf{\S\ref{sub:secular_stability_laplace}} Figs.~\ref{fig:s1_jovian_laplace}--\ref{fig:s2_solar_system_brouwer_naff} \& Table~\ref{tab:campaign_III_kpi_table} (\texttt{S1} Jovian Laplace $4:2:1$, \texttt{S2} Solar System \& NAFF) & \texttt{benchmarks/\allowbreak run\_generator\_05\_\allowbreak secular\_stability\_\allowbreak laplace\_and\_laskar\_\allowbreak naff.py}, \texttt{run\_S1\_laplace\_\allowbreak resonance.py}, \texttt{run\_S2\_brouwer\_naff.py} & \texttt{figures/\allowbreak plot\_generator\_05\_\allowbreak secular\_stability\_\allowbreak laplace\_and\_laskar\_\allowbreak naff.py} & \texttt{generator\_05\_\allowbreak secular\_stability\_\allowbreak laplace\_and\_laskar\_\allowbreak naff.json} \\
\textbf{\S\ref{sec:rebound_head_to_head}} Figs.~\ref{fig:rebound_b1_star_grazing}--\ref{fig:rebound_b4_pythagorean_chaos} \& Table~\ref{tab:rebound_head_to_head} (\texttt{REBOUND 5.2.2} Head-to-Head \texttt{B1}, \texttt{B2}, \texttt{B4}) & \texttt{benchmarks/\allowbreak run\_rebound\_b1\_\allowbreak star\_grazing\_pericenter.py}, \texttt{run\_rebound\_b2\_\allowbreak hill\_crossings.py}, \texttt{run\_rebound\_b4\_\allowbreak pythagorean\_chaos.py} & \texttt{figures/\allowbreak plot\_rebound\_b1\_\allowbreak star\_grazing\_pericenter.py}, \texttt{plot\_rebound\_b2\_\allowbreak hill\_crossings.py}, \texttt{plot\_rebound\_b4\_\allowbreak pythagorean\_chaos.py} & \texttt{rebound\_b1\_\allowbreak star\_grazing\_\allowbreak pericenter.json}, \texttt{rebound\_b2\_\allowbreak hill\_crossings.json}, \texttt{rebound\_b4\_\allowbreak pythagorean\_chaos.json} \\
\bottomrule
\end{tabular}%
}
\end{table}