Every K-Lean contract is a Lean 4 file proving that a published biology formula holds the properties it claims: bounds, monotonicity, conservation. Each theorem below is sorry-free and checked by the Lean 4 kernel. Nothing on this page is asserted by us; it is asserted by the proof engine.
K-Lean verifies computational integrity: that a function matches its published formula. It does not assert clinical or biological correctness, efficacy of the underlying algorithms, or safety for medical use. A proven theorem means the implementation is mathematically faithful to the stated formula, nothing more, nothing less.
Contracts are grouped into ten domains. For each contract we list its file name, the key theorems
it proves (exactly as they appear in the Lean source), and what those theorems establish. To inspect
any theorem yourself, import the contract and run #check: no trust required.
import KLean.Contracts.MichaelisMenten #check KLean.MichaelisMenten.velocity_monotone #check KLean.MichaelisMenten.velocity_lt_vmax -- Lean 4 elaborates each theorem. No sorry. No axioms.
| Contract | Key theorems | What it proves |
|---|---|---|
| MichaelisMenten | velocity_posvelocity_lt_vmaxvelocity_monotone | Reaction velocity is positive, never exceeds Vmax, and rises with substrate. |
| HillEquation | effect_nonnegeffect_lt_emax | Dose-response effect stays non-negative and below Emax. |
| CompetitiveInhibition | velocity_posvelocity_lt_vmaxvelocity_decreases_with_inhibitor | Velocity is positive, bounded, and falls as inhibitor rises. |
| IC50Relationship | ic50_posic50_ge_KIic50_increases_with_substrate | Cheng-Prusoff: IC50 is positive, at least KI, and grows with substrate. |
| HillCooperativity | hillOccupancy_poshillOccupancy_lt_onehillOccupancy_half_at_K | Fractional occupancy lies in (0,1) and equals ½ at K. |
| LangmuirIsotherm | coverage_poscoverage_lt_onecoverage_monotone | Surface coverage is a bounded, monotone fraction. |
| ReceptorBinding | occupancy_posoccupancy_lt_onehalf_occupancy_at_KD | Receptor occupancy is bounded and half-saturated at KD. |
| CatalyticEfficiency | catalyticEfficiency_poscatalyticEfficiency_increases_with_kcat | kcat/Km is positive and rises with kcat. |
| Contract | Key theorems | What it proves |
|---|---|---|
| PhenoAge | mortalityScore_posmortalityScore_lt_onephenoage_M_range | Levine 2018: mortality score is a probability in (0,1); phenotypic age stays in range. |
| Telomere | telomere_postelomere_decreasingtelomere_wellDefined | Herrmann 2023: telomere length is positive, well-defined, and declines with age. |
| BiologicalAge | ensemble_nonnegensemble_upper_boundinsufficient_knowledge_propagates | Composite age is bounded; insufficient-knowledge flags propagate through the ensemble. |
| GompertzMortality | mortality_posmortality_increasing | Mortality hazard is positive and increases with age. |
| WeibullSurvival | survival_possurvival_le_onesurvival_decreasing | Survival function is a decreasing probability. |
| TelomereAttrition | telomereLength_postelomereLength_decreasinghayflick_bound | L-DNA: telomere length stays positive, decreases, and respects the Hayflick bound. |
| GCContent | gcContent_nonneggcContent_le_one | GC fraction lies in the unit interval. |
| DnaTm | meltingTemp_nonnegmeltingTemp_increases_with_GCmeltingTemp_pos_of_gc | DNA melting temperature is non-negative and rises with GC content. |
| EpigeneticClockAcceleration | clock_age_nonnegacceleration_realreversal_possible | Epigenetic age is non-negative; acceleration is real-valued; reversal is representable. |
| SenolyticSelectivity | selectivity_nonnegselectivity_boundclearance_monotone | Senolytic selectivity is bounded; clearance is monotone in selectivity. |
| InflammAgingScore | score_nonnegscore_monotone_il6score_bounded | Inflammaging score is bounded and monotone in IL-6. |
| StemCellSelfRenewal | symmetric_renewal_oneasymmetric_renewal_halfsymmetric_gt_asymmetric | Self-renewal probabilities for symmetric vs. asymmetric division are ordered correctly. |
| Contract | Key theorems | What it proves |
|---|---|---|
| CkdMdrd | egfr_pos | MDRD eGFR is strictly positive. |
| CkdEpi | ckdEpi_pos | CKD-EPI 2021 eGFR is strictly positive. |
| CockcroftGault | crcl_pos | Creatinine clearance is strictly positive. |
| MeldScore | meld_increases_with_bilimeld_increases_with_inrmeld_increases_with_creat | MELD rises monotonically with bilirubin, INR, and creatinine. |
| HendersonHasselbalch | pH_eq_pKa_when_equalpH_increases_with_ratio | pH equals pKa at equal ratio and rises with the base/acid ratio. |
| Osmolarity | osmolarity_pososmolarity_increases_with_na | Serum osmolarity is positive and rises with sodium. |
| OsmoticPressure | osmoticPressure_pososmoticPressure_increases_with_concentration | van't Hoff: osmotic pressure is positive and rises with concentration. |
| BloodOxygenSaturation | saturation_nonnegsaturation_le_onefull_saturation | SpO2 is a fraction in [0,1] reaching 1 at full saturation. |
| BMI | bmi_posbmi_increases_with_weightbmi_decreases_with_height | BMI is positive, rises with weight, falls with height. |
| CardiacOutput | cardiacOutput_poscardiacOutput_increases_with_hr | Fick principle: cardiac output is positive and rises with heart rate. |
| ErythropoiesisODE | equilibrium_nonnegequilibrium_posequilibrium_monotone_epo | RBC-production equilibrium is non-negative and monotone in EPO. |
| Contract | Key theorems | What it proves |
|---|---|---|
| HardyWeinberg | hardy_weinberg_equilibriumfreq_AA_nonneg | Genotype frequencies satisfy HWE and remain non-negative. |
| SirEpidemic | reproductionNumber_posepidemic_threshold | R0 is positive; the epidemic threshold condition holds. |
| LogisticGrowth | population_pospopulation_le_K | Population stays positive and bounded by carrying capacity K. |
| CellDoublingTime | doublingTime_posdoublingTime_decreasing | Doubling time is positive and decreases with growth rate. |
| AllometricScaling | allometric_posallometric_increases_with_mass | Allometric quantity is positive and rises with body mass. |
| ClonalExpansion | cloneSize_poscloneSize_increases_over_timecloneSize_at_zero | Clone size is positive, grows over time, and matches the initial seed at t=0. |
| MonodGrowth | growthRate_posgrowthRate_half_at_Ks | Microbial growth rate is positive, bounded by μmax, half at Ks. |
| NucleotideBalance | energyCharge_nonnegenergyCharge_le_one | Adenylate energy charge (ATP/ADP/AMP) lies in [0,1]. |
| AbsorbingStateProbability | absorption_prob_nonnegabsorption_prob_le_oneterminal_has_full_absorption | Markov absorption probability is a valid probability; terminal states absorb fully. |
| BranchProbabilitySimplex | branch_prob_nonnegbranch_prob_le_onebranch_simplex | Phylogenetic branch probabilities form a valid simplex. |
| CigarInvariant | refLen_nonnegqueryLen_nonnegcigarItem_len_pos | Alignment CIGAR reference/query lengths are non-negative; item lengths positive. |
| CodingSequenceLength | valid_cds_divisible_by_threenum_codons_posconcat_preserves_frame | A valid CDS length is divisible by three; concatenation preserves reading frame. |
| GOEnrichmentClosure | closure_monotoneclosure_union_supersetclosure_singleton | Gene-ontology ancestor closure is monotone and respects unions. |
| MarkovTransitionStochasticity | entry_le_onestochastic_rowentry_mem_unit_interval | Transition-matrix rows are stochastic; entries lie in [0,1]. |
| NucleotideCompositionSum | composition_sums_to_oneall_fractions_nonneg | Nucleotide composition fractions are non-negative and sum to one. |
| Contract | Key theorems | What it proves |
|---|---|---|
| ProteinRMSD | squaredDeviation_nonnegrmsd_nonnegrmsd_zero_iff | RMSD is non-negative and zero iff the structures coincide. |
| BoltzmannDistribution | boltzmannFactor_posprobability_posprobability_le_one | Boltzmann factors are positive; state probabilities lie in (0,1]. |
| ContactProbability | sigmoid_possigmoid_lt_onesigmoid_monotone | Contact probability is a monotone sigmoid in (0,1). |
| TmScore | tmTerm_postmTerm_le_onetmTerm_eq_one_iff | Each TM-score term lies in (0,1] and equals one iff aligned exactly. |
| TMScore | tmScore_nonneg | Aggregate TM-score variant is non-negative. |
| PairwisePotential | totalEnergy_appendtotalEnergy_neg_of_all_negtotalEnergy_singleton | Residue-pair energy is additive over concatenation. |
| SequenceIdentity | seqIdentity_nonnegseqIdentity_le_oneseqIdentity_one_iff_identical | Sequence identity is a fraction in [0,1], one iff identical. |
| AlphaFoldConfidence | plddt_boundshigh_confidence_threshold | pLDDT stays within bounds; the high-confidence threshold is well-defined. |
| ProteinAggregationRate | rate_nonnegrate_monotoneproteostasis_balance | Aggregation rate is non-negative, monotone, and balances at proteostasis. |
| Contract | Key theorems | What it proves |
|---|---|---|
| BeerLambert | absorbance_posabsorbance_monotone_concentration | Absorbance is positive and rises with concentration. |
| NernstEquation | nernstPotential_increases_with_cout | Membrane potential rises with external ion concentration. |
| FickDiffusion | flux_magnitude_posflux_increases_with_gradient | Diffusive flux magnitude is positive and grows with the gradient. |
| FretEfficiency | fret_posfret_lt_onefret_decreases_with_distance | FRET efficiency lies in (0,1) and falls with donor-acceptor distance. |
| EinsteinStokes | diffusionCoeff_posdiffusionCoeff_decreases_with_radius | Diffusion coefficient is positive and falls with particle radius. |
| PoiseuilleFlow | flowRate_posflowRate_increases_with_radius | Blood-flow rate is positive and rises sharply with vessel radius. |
| ArrheniusEquation | rateConstant_posrateConstant_increases_with_temp | Rate constant is positive and rises with temperature. |
| GibbsFreeEnergy | gibbs_neg_when_exothermic_and_entropy_posgibbs_decreases_with_temp | ΔG is negative for exothermic, entropy-positive reactions and falls with T. |
| DiffusionMapEntropy | entropy_nonneguniform_entropy | Diffusion-map entropy is non-negative and maximal for uniform weights. |
| Contract | Key theorems | What it proves |
|---|---|---|
| ProtonMotiveForce | pmf_pos_of_dominant_potentialpmf_linear_in_potential | Mitchell equation: PMF is positive when potential dominates, linear in it. |
| AtpSynthaseEfficiency | efficiency_posefficiency_le_oneefficiency_lt_one_strict | ATP-synthase efficiency lies in (0,1). |
| TranslationRate | translationRate_postranslationRate_increases_with_mRNA | Translation rate is positive and rises with mRNA abundance. |
| RibosomeDensity | coverage_nonnegcoverage_le_onecoverage_increases_with_ribosomes | TASEP coverage is a fraction in [0,1] rising with ribosome count. |
| CellCycleFraction | conservationg1_le_ones_le_onem_le_one | Cell-cycle phase fractions are each ≤ 1 and conserve to the whole. |
| MrnaHalfLife | halfLife_posmrnaAbundance_posmrnaAbundance_at_halflife | Half-life is positive; abundance is positive and halves at the half-life. |
| ProteinSteadyState | steadyState_possteadyState_increases_with_synthesis | Steady-state protein level is positive and rises with synthesis rate. |
| AutophagyFluxBalance | flux_nonnegnet_autophagy_nonnegstarvation_upregulates | Autophagy flux is non-negative; starvation upregulates net flux. |
| MitochondrialMembranePotential | healthy_potential_negpotential_lower_boundhealthy_range | Healthy membrane potential is negative and within a bounded range. |
| NADPlusRatio | nad_plus_posratio_posratio_decreasing | NAD+/NADH is positive and decreasing under the modeled stress. |
| Contract | Key theorems | What it proves |
|---|---|---|
| FirstOrderPK | concentration_posconcentration_decreasinghalflife_positive | First-order concentration is positive, decreasing, with positive half-life. |
| BodySurfaceArea | bsa_posbsa_nonneg | Mosteller BSA is positive. |
| PcrAmplification | copies_poscopies_increasing_in_cyclescopies_doubles_per_cycle | PCR copy number is positive and doubles each cycle. |
| DilutionSeries | concentration_posconcentration_decreasing | Serial dilution concentration is positive and strictly decreasing. |
| ShannonEntropy | entropy_at_halfentropy_symmetric | Binary Shannon entropy is symmetric and maximal at p = ½. |
| FluorescenceQuantumYield | quantumYield_posquantumYield_lt_onequantumYield_eq_one_iff_no_nonradiative | Quantum yield lies in (0,1), reaching one only without non-radiative decay. |
| Contract | Key theorems | What it proves |
|---|---|---|
| SynNotch | and_gate_logicand_gate_true_iff_bothand_gate_false_if_either_absent | SynNotch AND-gate activates iff both ligands are present. |
| Riboswitch | confidence_in_unit_intervalinsufficient_knowledge_when_low_confidence | Riboswitch design confidence stays in [0,1]; low confidence flags insufficient knowledge. |
| LongevityProtocol | pipeline_confidence_boundedvalid_age_rangeik_propagates_pipeline | The end-to-end pipeline keeps confidence bounded and propagates insufficient-knowledge. |
| CircularRNABacksplice | backsplice_score_nonnegcanonical_backsplice_positivehigher_score_preferred | circRNA backsplice scores are non-negative; canonical sites score positive. |
| IRESActivity | activity_mem_unit_intervalhigher_activity_more_translationinactive_ires_no_initiation | IRES activity lies in [0,1]; higher activity yields more translation. |
| RNAFoldingFreeEnergy | stable_implies_nonpos_energymore_negative_dg_more_stable | Stable folds carry non-positive ΔG; more negative ΔG is more stable. |
| StemLoopStability | hairpin_energy_nonposmore_pairs_more_stableloop_size_valid | Hairpin energy is non-positive; more base pairs increase stability. |
| ModifiedNucleotideRatio | ratio_nonnegratio_le_onefull_substitution_iff | Modified-nucleotide ratio lies in [0,1], one iff fully substituted. |
| PolyASiteStrength | strength_mem_unit_intervalcanonical_site_strength_onestronger_site_dominates | Poly-A site strength lies in [0,1]; canonical sites are maximal. |
| TranslationInitiationContext | kozak_score_mem_unit_intervalperfect_kozak_score_onebetter_kozak_not_worse | Kozak score lies in [0,1]; a perfect context scores one. |
| CodonAdaptationIndex | cai_poscai_le_onecai_eq_one_iff_optimal | CAI lies in (0,1], one iff fully codon-optimized. |
| Contract | Key theorems | What it proves |
|---|---|---|
| GPPosteriorVariance | posterior_variance_nonnegdirac_has_zero_variancevariance_zero_iff_dirac | Gaussian-process posterior variance is non-negative, zero iff Dirac. |
| PseudotimeOrdering | pseudotime_nonnegroot_pseudotime_zeroroot_is_minimal | Pseudotime is non-negative; the root cell is the unique minimum. |
| SparseApproximationBound | approx_error_nonnegmore_inducing_tightermax_budget_minimal_error | Sparse approximation error is non-negative and tightens with more inducing points. |
Every contract above is also served over HTTP by klean-server (Rust / Axum) on the Kenosian Protocol Platform. No Lean toolchain required. The endpoints below are live.
curl "https://kpp.kenosian.com/klean/v1/gc_content?sequence=ATCGATCG"
curl -X POST "https://kpp.kenosian.com/v1/michaelis_menten" \
-H "Content-Type: application/json" \
-d '{"substrate": 0.5, "km": 0.1, "vmax": 2.0}'
K-Lean is open infrastructure under Apache 2.0. New biology contracts, proof improvements, domain extensions, and corrections are all welcome, and we welcome scrutiny and pushback in equal measure.
Contributions & feedback welcome: info@kenosian.com