Transcript-Length SVD,
from simulation to measured evidence
Dr. Orly Alter’s supplied datasets now drive the modernized Wolfram analysis, while an independent Lean 4 lane machine-checks the exact mathematical claims.
Alter & Golub, PNAS 2006 • Bertagnolli, Drake, Tennessen & Alter, PLoS ONE 2013
github.com/zuwasi/transcript-length-svd • public proof + synthetic baseline
The workflow, end to end
Two papers, one idea: SVD of mRNA length distributions
PNAS 2006 — mRNA lengths
SVD of a genome-scale mRNA-length distribution reveals an asymmetry in RNA gel-electrophoresis band broadening: transcripts spread more on one side of the peak than the other.
PLoS ONE 2013 — GBM oscillator
SVD identifies transcript-length distribution functions from microarray data and reveals evolutionary forces pulling transcript length toward an equilibrium, shifting in glioblastoma metabolism.
The math backbone: asymmetric Gaussian profiles, asymmetric Hermite-like modes, an SVD spectrum, and an asymmetric restoring force toward a length equilibrium.
Why add machine-checked proofs?
Numerics can pass and still not prove
- The Wolfram lane checks measured-table dimensions, SVD reconstruction, fraction sum, entropy, geometric decay, and GBM subset ordering
- Every check passes — but a passing numeric check is evidence, not a proof
Several claims are exact
- Positivity, unique peak, unique equilibrium, restoring sign, probability-simplex fractions, entropy nonnegativity
- Exact statements — ideal for a kernel-checked Lean 4 proof rather than sampling
The project now separates three evidence levels: measured observations, numerical validation in Wolfram, and exact theorem checking in Lean 4.
Four objects, mirrored in both lanes
Asymmetric Gaussian
amp·e^(−½k(x−c)²)
gene abundance vs migration; different left/right curvature
Asymmetric Hermite modes
modern basis functions replacing hand-flipped eigengenes
SVD fractions
fₖ = sₖ² / Σs₃²
eigen-abundance spectrum + entropy
Restoring force
x′ = −k(x)(x−c)
evolutionary pull toward length equilibrium
The original measurements replaced the synthetic baseline
Before receiving the datasets
- Calibrated synthetic transcript profiles
- Paper-inspired GBM scenario values
- Method reproduction, not measured reanalysis
- One explicit missing-data audit warning
After Dr. Alter supplied the datasets
- 6,776 × 30 measured mRNA matrix
- 4,109 × 50 human transcript matrix
- 3,620 × 30 yeast transcript matrix
- 11 passed, 0 failed, 0 warnings
The reusable loader detects *_mm columns, preserves biological annotations, validates numeric rows, and records source provenance.
The supplied data confirm the GBM length shift
n=180
n=257
n=412
Means from the supplied 500-cutoff annotations
Measured SVD entropy
Geometric λ
Leading fraction
Recon. error
The earlier synthetic run remains a reproducibility reference
Synthetic entropy
Synthetic λ
Synthetic mode corr.
Synthetic recon. error
Modes and evolutionary forces
10 theorems, kernel-checked, no sorry
Abundance profile
- asymGaussian_pos — strictly positive
- asymGaussian_le_amp — bounded by amplitude
- asymGaussian_eq_amp_iff — unique peak at center
Evolutionary force
- force_center_eq_zero — center is equilibrium
- force_eq_zero_iff — equilibrium is unique
- force_pos_of_lt / neg_of_gt — always restoring
SVD spectrum
- fractions_nonneg — each ≥ 0
- fractions_sum_one — sum to 1
- entropyTerm_nonneg — entropy ≥ 0
Lean 4 v4.32.0 + Mathlib • lake build → Build completed successfully (8658 jobs)
Formally proved vs numerically validated
Formally proved (Lean)
Positivity, boundedness, unique peak, unique equilibrium, restoring sign, probability-simplex fractions, entropy nonnegativity — exact, assumption-explicit.
Numerically validated only (Wolfram)
Measured SVD reconstruction, geometric-decay fit, GBM subset statistics, and full ODE convergence — floating-point or empirical results, kept honest in formalization_map.md.
A kernel-checked proof certifies only the stated theorem — not data provenance, biological interpretation, measurement quality, or the paper’s transcription.
Run both lanes from their project folders
Measured Wolfram analysis — my_version/
wolframscript -file .\build_project.wls wolframscript -file .\proof_audit.wls
Public proof repository — transcript-length-svd/
cd lean lake exe cache get # first time only lake build # kernel-checks all proofs
The measured analysis writes figures and CSVs to my_version/exports/; the separate public proof repository produces lean_build_report.txt.
Measured analysis and public proofs remain distinct
my_version/ measured analysis (local delivery) data sets/ Dr. Alter's supplied tables src/AlterLengthSVD.wl loader + model + SVD my_version_*.nb modern notebooks exports/ measured PNG/CSV evidence transcript-length-svd/ public code + proof repository lean/AlterProofs/*.lean 10 exact theorems docs/formalization_map.md proof boundary exports/ synthetic baseline + build reports
Public proof baseline
git clone https://github.com/zuwasi/transcript-length-svd
Measured tables are not included.
Why no Mathlib in the repo?
lean/.lake/ is Lean’s dependency cache — like node_modules. It holds the full Mathlib library (~7 GB) the proofs import. It’s derived state, so it’s excluded; lake exe cache get rebuilds it from the pinned manifest.
Data boundary
Code is MIT. Dr. Alter’s supplied measured tables retain their own provenance and are not relicensed or embedded by this presentation.
Measured evidence,
numerical validation, exact proof
The updated project analyzes Dr. Alter’s supplied measurements, preserves the synthetic baseline for comparison, and independently machine-checks the exact mathematical claims.
supplied measured tables
data and numerical audits passing
Lean theorems, 0 sorry
github.com/zuwasi/transcript-length-svd
© 2026 ESL — Engineering Software Lab • Released under the MIT License