The Missing Anchor
Every "canonical constant" in this series — ε₀ = 1/3, μ_max = −2, τ = 2 — is proved as a dimensionless fact about an abstract operator chain. None of them carry a physical unit anywhere in the Lean sources. The autophagy/mTORC1 chapter is the one place in the corpus that reaches past that and claims a real, unit-bearing number: μ_max ≈ −0.41 s⁻¹, obtained by rescaling the dimensionless −2 with a physical mTORC1 kinase time constant, citing Mizushima et al. (2010) and Melia et al. (2020). This working paper traces that calibration to its source. It does not hold up, on two independent grounds, and both are fixed in the source files as of this paper.
What was checked first, and cleared
Before treating anything here as an error, the apparent −3-vs-−2
discrepancy between mu_canonical and mu_dm3 in
AutophagyDm3_v2.lean was checked directly, by hand, rather
than assumed to be a bug.
What was checked next, and did not clear
The next step in the same source claims a physiological rescaling: dividing the dimensionless −2 by a real time constant τ_mTOR to get a rate in inverse seconds. Two files in the corpus make this claim, with two different numbers, for the identical result.
Neither number was found anywhere in a search of the ULK1/mTORC1 kinetics literature. What that literature actually reports, across several 2015–2024 papers on mTORC1–ULK1–AMPK regulation and oscillatory autophagy induction, is timescales of hours: ULK1 protein levels fall over roughly the first 4 hours of starvation and recover to baseline by roughly 6 hours, and autophagy induction itself is described as oscillatory on that same hours-long scale. A single-digit-second time constant is roughly three to four orders of magnitude away from anything reported for this specific pathway. "Melia et al. (2020)" did not surface as a findable paper on this topic in the sources checked.
The chapter also contradicts itself internally, in adjacent sections of the same file. Step 4 states the −0.41 s⁻¹ result as settled. Step 5, "Obligation 2," lists as an open obligation that "establishing that the mTORC1 suppression map σ is C∞-equivalent to V near ρ* (Mather's theorem) requires constitutive data from Mizushima et al. (2010)" — i.e., the same file already says, two paragraphs later, that the data needed to justify the Step 4 claim has not yet been brought in.
sample-chapter-autophagy.html and withdrawn with a
correction note in AutophagyDm3_v2.lean, both pointing
here. The dimensionless results (−3, −2, 1/3, all still
Lean-proved as dimensionless facts) are untouched; only the claim that
they'd been anchored to a real, physical, unit-bearing measurement is
withdrawn.
Why this one is bigger than WP-24/28/29
The earlier working papers in this series each found one unsupported or false claim in one place. This one is different in kind: it was the corpus's only candidate for a genuine bridge from an abstract, dimensionless, Lean-proved dynamical system to a real, externally measurable, unit-bearing quantity — the thing that would let someone actually test the framework against data, the way NANOGrav's 15-year pulsar timing data set tests general relativity's prediction for a stochastic gravitational-wave background. It does not currently do that. This does not mean such a bridge is impossible to build; it means it has not been built yet, and the corpus should not describe itself, in any chapter, as though it has been.
Path forward, if this is worth pursuing properly: go to the actual Mizushima (2010) and a correctly identified Melia paper (the 2020 citation could not be confirmed as it stands and may be a wrong year, wrong author, or non-existent reference — this should be checked directly against a citation database, not assumed), extract whatever real kinetic time constant either paper actually reports for ULK1 or mTORC1 activity, and redo the rescaling from that number rather than from a placeholder. Until then, the honest status of "μ_max in physiological units" is: not yet computed.