Four (not three) falsifiable predictions from a zero-free-parameter model of HIV escape from the eCD4-Ig decoy

Abstract

A network engineer, not a virologist, modelled the eCD4-Ig decoy as a black-hole route — a destination that accepts the packet and discards it — and asked what it would cost HIV to route around it. The model refuses curve-fitting. Every rate is taken from published measurement. Unknown quantities are not guessed: when a number is bounded and small, all 99 possible values are swept, and the answer becomes a bound rather than an assumption. --- ### VERSION 2 & 3: REBOUND RATE CORRECTION Version 1 required the decoy to clear 76 percent of virion output. That figure carried the BioNumbers 0.65-day doubling time, which belongs to primary infection, not to rebound after treatment interruption. The rebound rate is computable from the published medians themselves: x8 in 5 days between 50 and 400 copies gives 1.67 days. Correcting it lowers the rebound clearance requirement to 53 percent AND makes the untouched 400-copy prediction land exactly on the published median of 21 days, instead of 18. A correction that improves a prediction it does not calibrate is recorded here as such. --- ### VERSION 4: LEAN 4 FORMAL VERIFICATION & NON-LINEAR BIFURCATION Version 4 delivers the complete Lean 4 formal mathematical verification of the entire model (formalization_lean/), following the verification standards of OpenAI Math and CDC-Lean:- 32 formal theorems kernel-checked under Lean 4 (v4.34.1) with zero external axioms, zero warnings, and zero "sorry".- Analytical proof via the Routh-Hurwitz stability criterion demonstrating that the uninfected steady-state E0 is locally asymptotically stable if and only if theta > 1 - 1/R0. The clearance threshold is proven to be the exact transcritical bifurcation point of the full non-linear ODE system.- Sensitivity elasticity E(theta_c, R0) = 1 / (R0 - 1) = 0.2927, proving that a 10% uncertainty on viral contagiousness only shifts the required clearance threshold by 2.9%. --- ### THE FOUR FALSIFIABLE PREDICTIONS 1. **Escape cost above 73 percent.** Sweeping all 99 fitness costs, hardened across mutation rates from 1e-3 to 1e-8 (693 runs). Under standard mutation (1e-6), the extinction threshold is 74%; under hardened bounds (1e-8), it is 73%. Pixel-level reading of Fig. 5 of Fellinger et al., J Virol 2019 (PMC6600210) gives 92 to 97 percent for Q428K alone. A third independent mutation set (R315G/A436T/G471E, PMC11853013) carried a "marked loss of viral fitness" in a living animal. 2. **Serum neutralisation of the compensated variant at least 67 percent** in primary infection (31 percent in rebound). Fig. 6 gives about 75 percent for Q428K alone and 47 percent for N301D alone, against about 0 percent for wild type; the triple variant cannot be separated at the published resolution, and the missing value is reported as missing. 3. **Decoy clearance at least 76 percent (acute) and 53 percent (rebound).** Taken with the ~25 ug/ml in vivo IC50 estimated by Dhody, Cardozo-Ojeda et al. (PMC8754410), the 53% threshold corresponds to ~28 ug/ml of serum eCD4-Ig — below the 30-110 ug/ml carried by macaques, and below the 35-57 ug/ml 28-day troughs published for 20-40 mg/kg IgG infusions in humans. The 76% acute threshold corresponds to ~79.2 ug/ml (ratio 19/6 * IC50). 4. **Split-Intein biological microservices trans-splicing yield at least 57.1 percent (4/7) in muscle.** In network terms, splitting the oversized eCD4-Ig payload across dual AAV vectors introduces two bottlenecks: co-transduction (E_co) and protein trans-splicing yield (E_intein). The required overproduction factor scales as: S = 1 / (E_co * E_intein) Under median intramuscular co-transduction (35%), keeping the metabolic dose penalty within a viable 5.0x ceiling requires E_intein >= 4/7 = 57.1%. This formally validates optimized inteins (Cfa at 75% yield gives S = 3.81x in muscle, 2.67x in liver; Gp41-1 gives S = 3.36x in muscle, 2.35x in liver) and formally rules out standard Npu DnaE (40% yield requires S = 7.14x, exceeding cellular tolerance). --- ### WHAT THAT THIRD NUMBER IMPLIES The binding constraint appears not to be achievable concentration but durable concentration. AAV delivery reaches about 1 ug/ml with single capsids but holds for three years in half of participants (Casazza et al., Nature Medicine 2022). Infusion reaches ample titre but must be repeated: decaying from a 1177 ug/ml peak, 28 ug/ml is held for 29 to 116 days depending on the half-life taken. Dose or duration, not both — an engineering constraint rather than a virological one. --- ### WHERE THE MODEL FAILS, STATED BY THE AUTHOR In primary infection it requires target cells to fall to about 1 percent to turn the acute peak over, against a measured nadir near 304 cells per microlitre: it is wrong there. A pass threshold chosen after seeing the error it needed to accommodate was replaced by published interquartile ranges, which the author did not choose. A figure-reading program was wrong by a factor of four before correction; that is recorded in its source. Prior work is acknowledged where it precedes this: PMC8754410 performed the rigorous version of the concentration question, on real data, before and better than this model does. This work demonstrates nothing about HIV. It states conditions under which a model reproduces published measurements, and offers numbers that can refute it. All code (38 Python modules), the complete Lean 4 formalization project, the source-by-source provenance of every figure used, and the third-party expert audit pack (SHA256 checksums) are included in code-et-donnees-v4.zip.