\section{Formal evidence and reproducibility}\label{sec:formal}
The conventional arguments above are supported by two separate registered Lean developments. They retain their own module names, dependencies and proof interfaces; consolidation of the exposition does not create a new compared formal theorem. Both registered projects pin Lean \lean{v4.35.0-rc2} and Mathlib revision \lean{065356127b1dc0016f66b7283ce0ce2c4055aa55}. Their permitted axioms are \lean{propext}, \lean{Classical.choice} and \lean{Quot.sound}. References to earlier Lean~4.30.0 research receipts identify historical checks rather than the environment of these registrations.

\subsection{Registered endotactic permanence}
\href{https://palomar-registry.org/entry?id=PALOMAR-2026-10-09-000015&version=1}{PALOMAR-2026-10-09-000015, version~1} records the source commit \href{https://github.com/mmislan/palomar-endotactic-permanence/tree/c72c945264565397ecc3eee779e6bd5f3f3a061d}{revision \texttt{c72c94526456}}. The selected declarations, in namespace \lean{EndotacticSubmission}, are \lean{uniform_permanence} and \lean{continuous_dependence}.

The compared permanence statement allows arbitrary signed real source and target coordinates and evaluates the exponential-log monomials on positive states. It tests ordinary endotacticity in every real direction, admits almost-everywhere measurable histories bounded almost everywhere in a fixed positive rate box, and selects the compact convex invariant target before the initial compact set and history. The common entry deadline precedes the initial point and history. A global locally absolutely continuous solution with the almost-everywhere ODE is constructed, and uniqueness is among positive Carath\'eodory competitors. The statement thus supports the nonnegative real-complex scope of Theorem~\ref{u:thm:main}, as well as the compact-initial uniformity. The continuous-dependence statement supports Proposition~\ref{u:prop:dependence} for a common history on a compact positive region.

The periodic-forcing and equilibrium corollaries and the state-feedback extension retain the conventional proofs given here. For the first three-species example, historical Lean receipts establish the clocked comparison, inverse-square transformation, two-stage clock estimates and rational roundings. The reaction classification, invariant-box checks, clock identification and Riccati comparison retain their conventional status. Registration of the general theorem is not a claim that all example-specific arguments were selected for independent comparison.

\paragraph{Scalar-clock evidence for the first example.}
The steps of the proof of Theorem~\ref{u:thm:staged} after the clocks and the
inverse-square transformation are formalized as one Lean theorem,
\lean{staged_coordinate_recovery} (Section~\ref{sec:formal}): given an absolutely
continuous coordinate $u$ with values in $[1/10,10]$, an absolutely continuous
clock $\sigma$ with $\sigma(0)=0$ and $\sigma'\ge0$, coefficients with
$k_+\ge1/2$, $k_-\le2$, the equation $u'=\sigma'u(k_+-k_-u^2)$ almost everywhere,
clock floors $\sigma'\ge1/10$ on $[0,t_1]$ and $\sigma'\ge2/5$ on $[t_1,\infty)$,
and the arithmetic condition $t_1/10+\frac25(t_2-t_1)\ge19/5$, it concludes
$u(t)\ge2/5$ for all $t\ge t_2$. Its instances \lean{staged_recovery_second}
($t_1=9$, $t_2=65/4$) and \lean{staged_recovery_third} ($t_1=65/4$, $t_2=347/16$)
are the two stages, and \lean{a_stage_deadline_lt_nine},
\lean{recovery_deadline_lt_38} and \lean{staged_deadline_lt_22} are the roundings.
The conventional parts are the invariance of the startup box, the existence of the
clocks with the stated almost-everywhere derivatives (the integral of a bounded
measurable function), the identification $\sigma_b'=a$ with the floors from stage
$a$, and the Riccati comparison~\eqref{u:eq:aenvelopes}.

\subsection{Registered reverse-rate bounds and recovery}
\href{https://palomar-registry.org/entry?id=PALOMAR-2026-10-11-000020&version=1}{PALOMAR-2026-10-11-000020, version~1} records source commit \href{https://github.com/mmislan/palomar-quantitative-permanence/tree/e542422946035f4509e92c963b494e586105d09d}{revision \texttt{e54242294603}} and eighteen selected declarations. The principal correspondences are listed below. Except where a different namespace is printed, declaration names are in \lean{ReverseRateLimits}.

\begin{longtable}{>{\raggedright\arraybackslash}p{.43\linewidth}>{\raggedright\arraybackslash}p{.49\linewidth}}
\caption{Selected reverse-rate statements and their manuscript counterparts.}\label{tab:formal-correspondence}\\
\toprule
Manuscript conclusion & Selected declaration or coverage\\
\midrule
\endfirsthead
\multicolumn{2}{l}{\tablename~\thetable\ (continued)}\\
\toprule
Manuscript conclusion & Selected declaration or coverage\\
\midrule
\endhead
Theorem~\ref{q:thm:general}: network-first geometric gap, rate-dependent reciprocal containment and global solutions
& \lean{general_quantitative_root}\\[3pt]
Theorem~\ref{q:thm:coupled}: prepared-basin existence, concentration bounds and residence by $(31/10)\lambda^{-1}$
& \lean{SharpRecovery.prepared_recovery_sharp}\\[3pt]
The designated witness and its $(400/1313)\lambda^{-1}$ necessary target time
& \lean{SharpRecovery.witness_sharp}\\[3pt]
Theorem~\ref{q:thm:global-clocks}: arbitrary positive seeds, global solutions and necessary inventory restoration/depletion times
& \lean{GlobalInventory.global_inventory_clocks}\\[3pt]
Reverse-exponent family, both concentration and worst-case prepared recovery orders
& \lean{SharpRecovery.family_root_sharp}; exact scale identities and cutoff comparisons are selected separately\\[3pt]
Common-clock transport, preparation identities and cumulative reverse-reaction requirements
& \lean{CommonClock.rescale_iff}, \lean{RecoveryCorollaries.scale_tradeoff}, \lean{ReactionExtent.restoration_extent}\\[3pt]
Constant-capacity inventory comparison, including zero capacity
& \lean{SharpRecovery.inventory_bottleneck}, \lean{SharpRecovery.inventory_unreachable}\\[3pt]
Abstract inverse-power clock and absence of a linear conservation law
& \lean{GlobalInventory.inventory_bottleneck_scaling}, \lean{RecoveryCorollaries.no_linear_inventory}\\[3pt]
Admitted parameters and family admission with arbitrary admitted prefactors
& \lean{QuantitativeRegistry.admitted_parameters}, \lean{QuantitativeRegistry.family_parameters}\\[3pt]
Open-range version of the state-dependent capacity comparison in Proposition~\ref{q:prop:bottleneck-state}
& \lean{QuantitativeRegistry.state_capacity_clock}: positive continuous capacity on an open convex range containing the trajectory and target; no inventory monotonicity assumption\\
\bottomrule
\end{longtable}

The exact eighteen statement names and complete independent Challenge definitions are preserved with the source archives. The registered endpoints include the exact exponent identities, original cutoff comparison and cutoff decimal identity in addition to the grouped rows above. Definitions of literal trajectories do not assume the corridor, residence deadline or witness conclusion. The interval expression checker and the polynomial identifications used for the eighteen inclusions in Appendix~\ref{q:app:certificate} are contained in the proof closure.

The stochastic absorbing-state correction and birth-process comparison, the parameter-corner optimization, and the reaction-flux bookkeeping used to instantiate the abstract inventory estimate remain conventional arguments. Proposition~\ref{q:prop:bottleneck-state} is proved conventionally at its displayed interval scope; the selected formal version explicitly assumes an open convex positive-capacity range. The saved trajectory is a numerical illustration and does not certify its sampled hitting time. No stochastic success probability, upper recovery deadline or whole-class sharp-corridor capture theorem is inferred.

\subsection{Sources, historical verification and computational material}
The registered source archives include independent Challenge statements, completed Solution entry points, the supporting proof modules, dependency pins, licenses and upstream attribution. The affine construction is attributed to the pinned OpenAI development~\cite{OpenAI2026Boundedness,OpenAI2026Uniform,OpenAI2026Formal}; the port preserves the mathematical dependencies rather than replacing them by additional axioms. The public registration records describe their historical verification. Saved local receipts additionally report independent comparison and six configured kernel checks. Neither those historical runs nor the public registry status is presented as a fresh proof replay for this manuscript edition.

The exact registered source archives and their registration records are preserved in \href{https://zenodo.org/records/23442569/files/formalization.zip}{\nolinkurl{formalization.zip}}. Figure producers, exact certificate data, saved trajectories, parameter-corner files and historical evidence are in \href{https://zenodo.org/records/23442569/files/computational-companion.zip}{\nolinkurl{computational-companion.zip}}. The manuscript, TeX source and both archives are publicly available together at \href{https://doi.org/10.5281/zenodo.23442569}{\nolinkurl{doi:10.5281/zenodo.23442569}}. The immutable formalization repositories are also linked through the two Palomar records above.

All manuscript figures are carried over from the source papers. Their saved solver settings and numerical status are retained: declared simulations illustrate the analytic statements, while rational interval inclusions and formal statement comparisons are distinct evidence channels. Preparation of this edition checked source identities, bibliographic records, TeX compilation and rendered pages. No Lean, Lake, independent kernel, research numerical solver or certificate producer was executed.

\paragraph{Acknowledgements.}
The affine permanence construction and its Lean formalisation are due to OpenAI~\cite{OpenAI2026Uniform,OpenAI2026Boundedness,OpenAI2026Formal} and are used here as an attributed input at a pinned revision.

\paragraph{Use of AI tools.}
Generative AI was used extensively for mathematical development, manuscript drafting, computations and Lean formalization under human direction.