§ 1 · De Duve's Lysosomes and Ohsumi's ATG Genes

Christian de Duve isolated lysosomes from rat liver cells in 1955 — membrane-bound organelles filled with hydrolytic enzymes capable of digesting almost any biological molecule. In 1963 he coined the term autophagy (Greek αὐτοφαγία, "self-eating") to describe the process by which the cell delivers its own cytoplasmic contents to the lysosome for recycling. He was awarded the Nobel Prize in 1974.

For three decades, autophagy remained a morphological curiosity. Then in 1993, Yoshinori Ohsumi performed a screen in Saccharomyces cerevisiae under nitrogen starvation and identified the first autophagy-defective mutants. By 1997 his lab had cloned the first ATG (autophagy-related) genes. The discovery that autophagy has a defined, conserved genetic programme — now more than 40 ATG genes identified in yeast, with mammalian orthologues — earned Ohsumi the Nobel Prize in 2016.

What Ohsumi could not have foreseen in 1997 is that the genetic cascade his screen revealed — from nutrient sensor to membrane fold to lysosomal restoration — is the dm³ operator chain G = U ∘ F ∘ K ∘ C, written in the language of kinase biochemistry.

§ 2 · The mTOR Decision Surface

The autophagy switch is controlled by mTOR (mechanistic target of rapamycin), a serine/threonine kinase and master nutrient sensor. When amino acids and growth factors are abundant, mTORC1 is active and suppresses autophagy by phosphorylating and inactivating the ULK1 initiation complex. When nutrients fall below threshold, mTORC1 is inhibited, ULK1 fires, and the autophagy programme begins.

The complementary sensor is AMPK (AMP-activated protein kinase), which detects falling ATP/AMP ratios — cellular energy deficit. AMPK directly activates ULK1 (by phosphorylating S317 and S777) and simultaneously inhibits mTORC1, creating a bistable switch: growth or renewal.

In contact geometry, this is a fold singularity. The contact manifold of the cell's metabolic state space is:

The fold operator F fires when r ≤ r*(λ) = √(K_aa / λ): below this threshold, the contact condition α_cell = 0 forces the system onto the autophagy branch. This has the same functional form as the self-trapping bound in the zeolite model (Ch CatGT, where it carries an explicit length scale and an open normalization) and as a Sweet-Parker-type threshold in plasma reconnection. A shared functional form is a proposed analogy across substrates, not a demonstrated shared mechanism.

§ 3 · G = U ∘ F ∘ K ∘ C in the Autophagy Cascade

The four operators of the dm³ chain fire in strict sequence during autophagy initiation, elongation, and completion:

The cycle closes: lysosomal amino acid export reactivates mTOR, which terminates ULK1, ending autophagy. The system returns to its resting state — the contact manifold has returned to the basin of the fixed point x*. This is the proposed Lyapunov-stability reading: the post-autophagy state as an attractor with eigenvalue μ = −2. That is the dm³ model's assumed value; no kinetic data here measure it. To build it up, one would fit the mTOR/AMPK feedback ODE to published time-courses and linearise at the resting state.

The LC3-I → LC3-II transition at the F step deserves special emphasis. LC3-II (phosphatidylethanolamine-conjugated LC3) inserts into the phagophore membrane on both sides, which the dm³ reading proposes to model as a Legendrian submanifold: the autophagosome membrane as a contact surface on which a contact flow is integral. The curvature of the membrane is set by the ATG5–ATG12–ATG16L1 complex; that it equals the curvature required by a contact condition α_cell = 0 is a conjecture, not derived here (no α_cell is defined on the cell state space).

§ 4 · The Lean 4 Proof

The fold is proved where a proof is available: on the potential itself. The two Whitney A₁ conditions — a critical point at q = 1, and that critical point non-degenerate — are a few lines of Lean each, and the factorisation exhibiting the double root is one more. What follows is verbatim from AutophagyDm3.lean in the AXLE repository.

The triple-alpha side is a separate file, and deliberately a spare one. Three α-particles couple, so the fold ladder is the three-term recurrence w(k+3) = w(k+2) + w(k+1) + w(k), whose characteristic root is the Tribonacci constant η ≈ 1.8393 — above the two-body constant φ, below the embodiment threshold τ = 2. TripleAlphaDm3.lean proves the ordinal form of that sandwich, and carries no dependency on Mathlib, so it can be checked from a clean checkout with nothing to fetch.

The two files answer different questions and are held to different standards. The autophagy theorems are sorry-free in source, compiled against Mathlib. The triple-alpha theorems have been through the kernel with a per-declaration #print axioms. Five of the six return [propext, Quot.sound] — two of the three standard axioms, since nothing in the file is classical. The sixth, tribo_rec, returns does not depend on any axioms: the recurrence holds definitionally, so the kernel needs nothing at all to accept it. Re-run 27 August 2026 under Lean 4.32.0, from a clean checkout, by lean TripleAlphaDm3.lean — no lake, no Mathlib, nothing fetched.

Three statements in AutophagyDm3.lean are placeholders and are labelled as such in the source: contactForm_nondeg_full, whitneyFold_from_kinase_data and limitCycle_exists_auto are each stated as True pending AXLE Issue #14. They are open obligations, not results, and the scalar or algebraic content standing in for each is the theorem named beside it above.

Later state of the file. The header of AutophagyDm3_v2.lean (dated 2026-08-25) records that those three True statements were removed, not proved, because a theorem whose conclusion is True passes every sorry count. The file now claims 24 theorems, no sorry, and no axiom beyond propext, Classical.choice, Quot.sound; the three obligations are open and stated in prose. That header is the file's own statement; it has not been re-run here (no Lean toolchain in this session).

§ 5 · A Proposed Analogy: Autophagy ↔ Stars ↔ Zeolites

The dm³ programme proposes that a threshold of the form r*(λ) = √(J/λ) recurs across domains (see the cross-domain table in Ch CatGT, now labelled a shared functional form, not a shared invariant). In the autophagy reading, the mTOR/AMPK ratio plays the role of λ, the normalised nutrient concentration is r, and the fold threshold r* separates the growth mode from the renewal mode. This identification is proposed here, not derived.

The proposed structural parallel with the triple-alpha process is:

Both are self-regulating: the product of the fold (carbon atoms / amino acids) terminates the process by restoring the variable (temperature drops / mTOR reactivates) that keeps r above threshold. The intended reading is Lyapunov stability — the orbit returns to x* after perturbation — and, if it held, it would help explain why both stellar nucleosynthesis and cellular autophagy are stable over geological / evolutionary timescales. Stability of the full system is not proved in this chapter.

§ 6 · Aging, Cancer, and the μ = −2 Principle

Impaired autophagy is now documented in virtually every major age-related disease: Alzheimer's (tau and amyloid aggregation), Parkinson's (α-synuclein accumulation), cancer (dual role: tumour-suppressive early, survival-promoting late), and metabolic syndrome (lipid droplet accumulation). The common thread is failure to maintain the μ = −2 anti-entropy rate — the cell cannot export disorder fast enough.

Rapamycin — discovered from soil bacteria on Easter Island (Rapa Nui, hence the name) (from soil samples collected in 1964) — inhibits mTORC1 and forces the cell into autophagy mode. Rapamycin extends lifespan in yeast, worms, flies and mice. In the dm³ interpretation: rapamycin fixes the fold operator F in its "on" state, maintaining the C→K→F→U cycle even when nutrient signals would otherwise suppress it.

In the dm³ reading, the anti-entropy rate μ = −2 would be the Lyapunov exponent of the G-chain at the fixed point x* (a model assumption, not a measured quantity). On that reading, ageing would be the drift of μ toward 0 — loss of Lyapunov stability — and autophagy one of the mechanisms keeping μ below 0. This is a hypothesis to be tested, e.g. by asking whether an autophagy-flux decline tracks a loss of contraction rate in the fitted ODE. This is why caloric restriction — which chronically activates AMPK and suppresses mTOR — is among the most reproducible lifespan-extending interventions known.

§ 7 · Connection to the BZ Reaction and Neural Oscillation

The Belousov-Zhabotinsky reaction (see Ch BZ) and autophagy share a deep structural identity: both are dissipative oscillators maintained at a non-equilibrium steady state by continuous energy (chemical potential) input. Both produce spatial patterns — BZ produces spiral waves on a dish; autophagy produces spatial autophagy flux patterns that are cell-cycle-phased (autophagy peaks at G1/S transition and is suppressed during mitosis).

The period of the autophagy cycle — typically 15–30 minutes for autophagosome formation, 30–60 minutes for lysosomal degradation — is proposed to map to the π operator period T* = 2π/ω₀ (an analogy; ω₀ is not measured here). The frequency ω₀ is set by the mTOR/AMPK kinetics. In nutrient-starved cells, ω₀ falls and the period lengthens; in growth conditions, ω₀ rises and the cycle shortens. This is the π operator modulating the A operator: the recurrence ladder determining the rhythm of self-renewal.

§ 8 · AXLE Cross-Reference and Lean 4 Status

The autophagy theorems live in AutophagyDm3.lean and the three-body ladder in TripleAlphaDm3.lean, both in the AXLE repository, with the zeolite companion in CatGT_Main.lean (canonical in TOTOGT/io, mirrored in geometry/catgt/lean/). Counts are per file, produced by tools/theorem_census.py (re-run 2026-09-20), and separate declarations stated as True (placeholders) from those that are not. The census counts declarations written and sorry-free; it does not count theorems proved, and “substantive” here means “not stated as True,” not “deep” (several entries are short numerical or algebraic checks):

The cross-domain reading — that a threshold of the form r*(λ) = √(J/λ) governs qualitative transitions in cells, zeolites, plasmas and stellar interiors — is a working conjecture of the dm³ programme, not a result of this chapter. √(J/λ) is the generic crossover scale of a spreading term against a localizing term, so the same form appearing in several domains is weak evidence of a shared mechanism by itself, and the zeolite version now carries an explicit length scale and an open normalization (Ch CatGT). Autophagy is worked here as one instance. What is stated and proved (sorry-free in AutophagyDm3.lean) is algebra on the model potential: V′(1) = 0, V″(1) = 6 ≠ 0 and the double-root factorisation. The step from kinase data to that potential (whitneyFold_from_kinase_data) is one of the three placeholders above. It is the theorems that are verified, not the analogy between domains.