interfaces

The interface ledger — where kernel-checked ends

Every theorem in this library compiles axiom-clean: #print axioms reports nothing beyond {propext, Classical.choice, Quot.sound}, and no sorryAx appears anywhere. What the kernel does not check is anything a theorem takes as a hypothesis. This library’s discipline — the IsSolutionTo precedent, applied on every rung — is that un-formalized machinery never enters silently: it enters as a named hypothesis in the theorem signature, documented in the module’s own honest-scope section. This page is the single ledger of those hypotheses: what each one says, who assumes it, who discharges it (or what the candidate discharge is), and the one-sentence boundary each carries. All boundary sentences below are quoted or tightly paraphrased from the modules’ own derivation pages — nothing here is new.

Reading rule for the defense: a sealed module rests on no open interface; an interfaced module is kernel-checked given the rows below.

Summary

Interface	One sentence	Assumed by	Status
IsSolutionTo	The flow solves the ODE orbitwise	lasalle_invariance, reduction_cascade, com_lasalle, coupled_dissipation, coupled_collapse	open — semiflow/Picard–Lindelöf stays applier-side
hcpt	Two-sided precompact orbit closure	same five modules	open — candidate: forward-only semiflow refactor
QuadSandwich	$c_1\Vert y{\Vert }^2\le V\le c_2\Vert y{\Vert }^2$	lyapunov_comparison	discharged by rayleigh_sandwich quadSandwich_matrix
hM (Christoffel factorization)	$\dot{\mathbf{M}}=\mathbf{C}+{\mathbf{C}}^{\top }$	passivity_identity	discharged by passivity_transport congruence_transport
hdec	$DV(y)[f(y)]\le 0$ everywhere	lasalle, propIV1_tendsto	discharged — coupled_hdec (coupled block), com_decrease (CoM block)
hzero	$\{DV[f]=0\}\subseteq {\Gamma }_1$	reduction_cascade, coupled_dissipation	superseded for the coupled block by coupled_collapse’s invariance route
hStable	EHM Theorem 6 $\epsilon$–$\delta$ set stability	reduction_cascade	open — L4b / rung-5 candidate
hLandsInΓ₁	EHM Theorem 8 / Lemma 22 relative-attraction collapse	reduction_cascade	open — L4b / rung-5 candidate
hsvd	${\sigma }_{\min }>0⟺\det \ne 0$	gamma_invertible	open — candidate: Mathlib LinearMap.singularValues bridge
g2 (the coordinate field)	The closed-loop coupled-block field, eq 34b	named by reduction_cascade, stiffness_residual	discharged by coupled_field g2Field (constant-operator form)
hreal + hfield (moving-metric bracket)	The state-dependent-operator calculus	coupled_dissipation, coupled_collapse	open — the deferred analytic step
hvc, hv, hbound, hnn (solution regularity)	Continuity, right-derivative, decrease inequality, nonnegativity of $v$	time_varying_comparison	applier-side by design
Concrete-SPD operator hypotheses	Symmetry, definiteness, inverse, adjoint of $\mathbf{M},\mathbf{K},\mathbf{D},\mathbf{J}$	com_lasalle, coupled_field, coupled_dissipation, coupled_collapse	open — matrix corollary is the boarded rung-1 follow-up; each has a sealed discharge route

IsSolutionTo

What it says. IsSolutionTo ϕ f (defined in LaSalle.lean:55): for every point and time, the orbit of the Mathlib Flow ℝ E has derivative $f({\phi }_t(x))$ in the HasDerivAt sense — the flow is given and asserted to solve $\dot{x}=f(x)$.

Assumed by lasalle (lasalle_invariance), propIV1_tendsto (reduction_cascade), com_collapse/com_gas (com_lasalle), coupled_block_tendsto (coupled_dissipation), coupled_collapse/coupled_gas/coupled_velocity_tendsto (coupled_collapse).

Discharged by — open. A construction would be Picard–Lindelöf existence + uniqueness + completeness on the singularity-free region $\Omega$, packaged into a Flow; Mathlib’s PicardLindelof gives local existence but no packaged flow.

Honest boundary (from lasalle_invariance): “How such a flow arises on $\Omega$ — completeness of the closed-loop field, forward-only versus two-sided time — stays on the applier’s side, stated in the application, not smuggled into the theorem.”

hcpt

What it says. IsCompact (closure (range fun t : ℝ => ϕ t x₀)) — the two-sided orbit closure is compact.

Assumed by the same five modules as IsSolutionTo (it is the LaSalle engine’s compactness input, carried unchanged through every assembly).

Discharged by — open. Candidate discharge, recorded on the stream board: the forward-only semiflow refactor of the LaSalle engine, after which the sealed blockLyap_coercive (block_lyapunov) closes it outright.

Honest boundary (from com_lasalle §5): coercivity of $V$ bounds the forward orbit only — “Mathlib’s Flow ℝ is two-sided, and a stable system’s backward orbit is unbounded, so full two-sided precompactness is genuinely more than forward coercivity yields.” blockLyap_coercive is cited as the forward-boundedness witness.

QuadSandwich

What it says. QuadSandwich V c₁ c₂: $c_1\Vert y{\Vert }^2\le V(y)\le c_2\Vert y{\Vert }^2$ for all $y$ (defined in Lyapunov.lean).

Assumed by lyapunov_norm_sq_exp_decay (lyapunov_comparison) — L2 shipped it as an unproven hypothesis.

Discharged by rayleigh_sandwich — verified: quadSandwich_matrix produces exactly QuadSandwich (fun y => y ⬝ᵥ K *ᵥ y) c₁ c₂ on EuclideanSpace ℝ n from uniform eigenvalue bounds, via the sealed Rayleigh–Ritz sandwich.

Honest boundary (from rayleigh_sandwich): the norm is the Euclidean norm — the producer is stated on EuclideanSpace ℝ n, not the plain n → ℝ sup norm; symmetry alone gives the sandwich, and Matrix.PosDef.eigenvalues_pos licenses the strictly positive $c_1$ the Lyapunov argument relies on.

hM — the Christoffel factorization

What it says. hM : Mdot = C + Cᵀ — the inertia rate factors through the Coriolis matrix, which holds when $\mathbf{C}$ is chosen through the Christoffel symbols (ott2008cartesian Lemma 3.2’s construction).

Assumed by mdot_sub_two_coriolis_skew and passivity_identity (passivity_identity) — L3 proved eq 23 conditionally on it.

Discharged by passivity_transport — verified: congruence_transport proves the transported factorization $\dot{\hat{\mathbf{M}}}=\hat{\mathbf{C}}+{\hat{\mathbf{C}}}^{\top }$ from symmetry of $\mathbf{M}$ and the original-coordinate Christoffel choice; “automatically holds” is machine-checked.

Honest boundary (from passivity_transport): two pieces of scaffolding are supplied at the statement level rather than proved — the product-rule identification of $\dot{\hat{\mathbf{M}}}$ with $\frac{d}{dt}({\mathbf{P}}^{\top }\mathbf{MP})$ along a trajectory, and the $\mathbf{P}={\mathbf{\Gamma }}^{-1}$ identification plus the $12\times 12\to 9\times 9$ block extraction (the latter certified symbolically by SymPy pin C).

hdec

What it says. $\forall y,DV(y)[f(y)]\le 0$ — the energy-decrease input the LaSalle engine and propIV1_tendsto consume.

Assumed by lasalle (lasalle_invariance) and propIV1_tendsto (reduction_cascade) as a theorem hypothesis.

Discharged by — verified twice: com_decrease (com_lasalle) for the CoM driver, and coupled_hdec (coupled_dissipation) for the coupled block, where the sign-indefinite Coriolis term is killed by the transported passivity identity (“the hdec hole is now filled by construction”). The coupled discharge is itself conditional on hreal and hpass below.

hzero

What it says. hzero : {y | fderiv ℝ V y (f y) = 0} ⊆ Γ₁ — the zero set of the Lyapunov derivative sits inside the target set; the paper’s ”$\breve{\mathbf{v}}\equiv 0$ implies $\tilde{\mathbf{x}}=0$”, made precise.

Assumed by propIV1_tendsto (reduction_cascade) and coupled_block_tendsto (coupled_dissipation).

Status — superseded for the coupled block, and the supersession is itself machine-checked (coupled_collapse): the pointwise containment with ${\Gamma }_1=\{0\}$ is false — the zero set is the whole subspace $\{\breve{\mathbf{v}}=0\}⊋\{0\}$ (pin: 5000/5000 counterexamples) — so it was never sealed; coupled_gas reaches the origin through the invariance route instead (coupled_collapse + the reduction engine), and coupled_velocity_tendsto records the pointwise route’s honest ceiling. The linear algebra behind the paper’s closing sentence (${\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}=0\Rightarrow \tilde{\mathbf{x}}=0$) is sealed in stiffness_residual.

Honest boundary (from reduction_cascade): the containment “uses the un-formalized closed-loop field ${\mathbf{g}}_2$, the positive-definiteness of $\breve{\mathbf{D}},\breve{\mathbf{K}}$, and the rank of ${\mathbf{J}}_{\tilde{x}}$ on $\Omega$ — none of which is a Flow ℝ E fact.”

hStable — EHM Theorem 6 core

What it says. hStable : StableSet ϕ Γ₁ — the $\epsilon$–$\delta$ set stability of the target (El-Hawwary–Maggiore 2013, Theorem 6, compact branch).

Assumed by reduction_asymptotic_stability (reduction_cascade).

Discharged by — open; L4b / rung-5 candidate (boarded on the stream, charter + go/no-go when opened).

Honest boundary (from reduction_cascade): “the genuine topological reduction — that conditions (i)–(iii) upgrade relative asymptotic stability to full asymptotic stability — is EHM’s Appendix A and is beyond L4a’s stall gate”; a faithful-statement Theorem 10 whose proof reasserted its conclusion would be vacuous, so the core enters named, never faked.

hLandsInΓ₁ — EHM Lemma 22 core

What it says. There is $\delta >0$ such that every point within $\delta$ of ${\Gamma }_1$ has precompact orbit closure and ${\omega }^{+}(x)\subseteq {\Gamma }_1$ — the relative-attraction collapse (EHM Theorem 8 core / Appendix-A Lemma 22).

Assumed by reduction_asymptotic_stability (reduction_cascade).

Discharged by — open; L4b / rung-5 candidate, same boundary as hStable. What is proved is the assembly: this hypothesis fed through the sealed reduction engine yields AttractiveSet, which with hStable gives AsymStableSet — “the attractivity conclusion here is real reduction content produced by the engine, not an assumption.”

hsvd — the singular-value criterion

What it says. hsvd : 0 < sigmaMin J ↔ J.det ≠ 0, with sigmaMin a bare function parameter — whatever "${\sigma }_{\min }$" means, the conclusion holds provided it satisfies this standard SVD fact.

Assumed by gamma_isUnit_iff_sigmaMin_pos (gamma_invertible); the determinant and unit biconditionals of that module carry no interface.

Discharged by — open. Candidate: Mathlib’s LinearMap.singularValues route (matrix → toLin' → injectivity → det ≠ 0 via rank-nullity).

Honest boundary (from gamma_invertible): “There is no library lemma of the form ${\sigma }_{\min }(\text{matrix})>0⟺\det \ne 0$” in the Mathlib pin; discharging it means building the whole bridge — “honest standard mathematics, not a weaker substitute and not a silent sorry.”

g2 — the closed-loop coordinate field

What it says. The driven coupled-block field of Giordano eq 34b on the driver-zeroed manifold: ${\mathbf{g}}_2(y)=({\mathbf{J}}_{\tilde{x}}\breve{\mathbf{v}},-{\breve{\mathbf{M}}}^{-1}(\breve{\mathbf{C}}\breve{\mathbf{v}}+\breve{\mathbf{D}}\breve{\mathbf{v}}+{\mathbf{J}}_{\tilde{x}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}))$.

Named as un-formalized by reduction_cascade (inside hzero) and stiffness_residual (“that field is deliberately un-formalized across this campaign”).

Discharged by coupled_field — verified: g2Field defines the field in Lean, with its equilibrium (g2Field_origin), the energy’s smoothness, and the exact derivative lemmas sealed against a SymPy pin frozen before any Lean was written.

Honest boundary (from coupled_field / coupled_collapse): the sealed field is the constant-operator linearization — the true field carries configuration-dependent $\breve{\mathbf{M}}(\mathbf{q}),\breve{\mathbf{C}}(\mathbf{q}),\dots$; identifying the two is exactly the hreal/hfield bracket below.

hreal + hfield — the moving-metric calculus bracket

What they say. hreal : ∀ y, fderiv ℝ V y (f y) = coupledLyapRate … y — the true field’s Lyapunov Fréchet-derivative realizes the assembled rate (state-space partial plus the $\frac{1}{2}⟨\breve{\mathbf{v}},\dot{\breve{\mathbf{M}}}\breve{\mathbf{v}}⟩$ moving-metric correction). hfield : ∀ y, (f y).2 = (g2Field …).2 — the true field’s velocity component is the eq-34b right-hand side.

Assumed by coupled_hdec/coupled_block_tendsto (coupled_dissipation, hreal) and coupled_collapse/coupled_gas (coupled_collapse, both).

Discharged by — open; the deferred analytic step, same family as the product-rule naming in passivity_transport.

Honest boundary (from coupled_dissipation): “identifying the moving-metric chain rule with the assembled rate is the deferred analytic step … It brackets exactly the analytic plumbing, never the algebra: the algebra it brackets is coupled_total_dissipation, proved.” And (from coupled_collapse) hfield “constrains only the second coordinate and is independent of hreal (which constrains the scalar energy rate).“

hvc, hv, hbound, hnn — solution regularity

What they say (in TimeVaryingComparison.lean): hvc — continuity of $v$ on the half-line; hv — the pointwise right-derivative witness HasDerivWithinAt v (v' t) (Ici t) t; hbound — the differential inequality $v^{\prime }(t)\le -av(t)+\epsilon (t)$; hnn — nonnegativity of $v$.

Assumed by comparison_shift, comparison_tendsto_zero, comparison_bounded (time_varying_comparison).

Discharged by — applier-side by design: here $v=V\circ x$ is the Lyapunov value along a solution, and “its continuity and right-differentiability come from the chain rule on a differentiable $V$ and a solution $x$, which is upstream scaffolding, not this theorem’s content.”

Honest boundary (from time_varying_comparison): hbound “is the field-level Lyapunov decrease pulled back along the trajectory — the honest input, exactly the object Panteley–Loría assume”; without hnn the theorem still proves $\mathrm{limsup}v\le 0$. The explicit derivative witness also disarms Mathlib’s total-fderiv junk-value trap.

The concrete-SPD operator hypotheses

The abstract-inner-product-space modules carry their operators as continuous linear maps with defining identities as named hypotheses — “for a concrete symmetric positive-definite matrix these are not assumptions but theorems, discharged by the sealed campaign” (com_lasalle §5). The matrix corollary that mechanically discharges them via Matrix.toEuclideanCLM is the boarded rung-1 honesty follow-up (deferred by ping 2026-07-06); until it lands, each row below names its sealed discharge route.

Hypothesis	Says	Assumed by	Sealed discharge route
hMsa	$\mathbf{M}$ self-adjoint	com_lasalle, coupled_field, coupled_dissipation, coupled_collapse	Matrix.PosDef.isHermitian
hKsa	$\mathbf{K}$ self-adjoint	same four	Matrix.PosDef.isHermitian
hMinv	$\mathbf{M}({\mathbf{M}}^{-1}w)=w$	same four	Matrix.nonsingularInverse
hJadj	$⟨\mathbf{J}a,b⟩=⟨a,{\mathbf{J}}^{\top }b⟩$	coupled_field, coupled_dissipation, coupled_collapse	the toEuclideanCLM adjoint fact
hDnn	$⟨v,\mathbf{D}v⟩\ge 0$	com_lasalle, coupled_dissipation, coupled_collapse	le_dotProduct_mulVec (rayleigh_sandwich) with $c_1=0$
hDdef	$⟨v,\mathbf{D}v⟩=0\Rightarrow v=0$	com_lasalle, coupled_collapse	le_dotProduct_mulVec with $c_1={\lambda }_{\min }(\mathbf{D})>0$
hKdef	$\mathbf{K}x=0\Rightarrow x=0$	com_lasalle	PosDef.isUnit + mulVec_injective_of_isUnit (the stiffness_residual pattern)
hMinj	${\mathbf{M}}^{-1}$ injective	coupled_collapse	$\mathbf{M}$ as left inverse (hMinv)
hJKinj	${\mathbf{J}}^{\top }(\mathbf{K}x)=0\Rightarrow x=0$	coupled_collapse	content sealed as stiffness_residual_injective' (stiffness_residual); the operator transcription stays applier-side
hpass	$⟨v,\dot{\mathbf{M}}v⟩=2⟨v,\mathbf{C}v⟩$	coupled_dissipation, coupled_collapse	content sealed as transported_passivity_identity (passivity_transport); the matrix↔operator bridge is “the same toEuclideanCLM/WithLp plumbing CoupledField already defers”, pinned identical in pin (3)

Honest boundary (from coupled_dissipation on hpass, representative of the family): the sealed theorem is matrix-shaped and the field abstract, so the hypothesis “is met at the level of mathematical content … rather than a literal import — because the sealed theorem is matrix-shaped and the field is abstract, exactly the hMinv precedent. No weaker math is substituted.”