Metadata-Version: 2.4
Name: kenoslean
Version: 0.1.0
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Science/Research
Classifier: Topic :: Scientific/Engineering :: Bio-Informatics
Classifier: Topic :: Scientific/Engineering :: Mathematics
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Rust
Classifier: Operating System :: POSIX :: Linux
Summary: Machine-verified computational biology contracts, Lean 4 kernel-checked, Rust-accelerated
Keywords: biology,bioinformatics,mRNA,longevity,formal-verification,lean4,rna
License: MIT
Requires-Python: >=3.8
Description-Content-Type: text/markdown; charset=UTF-8; variant=GFM
Project-URL: Homepage, https://kenosian.com

# kenoslean

**Machine-verified computational biology contracts — Lean 4 kernel-checked, Rust-accelerated, exposed to Python.**

Each function in this package corresponds to a contract whose mathematical
invariants are stated and proven in a Lean 4 module (`KLean.Contracts.*`). The
Rust implementation reproduces the algorithm; pre-condition violations raise
`ValueError`, and post-conditions are guarded with `debug_assert!` in debug
builds.

> **Naming.** The PyPI distribution is **`kenoslean`** (the name `klean` was
> already taken on PyPI by an unrelated project). The **import module name is
> `klean`**:
>
> ```bash
> pip install kenoslean      # distribution
> ```
> ```python
> import klean               # module
> ```

## Quick start

```python
import klean

klean.gc_content("ATGCGCATGC")                    # 0.5  — GCContent ∈ [0,1]
klean.mrna_halflife_concentration(100.0, 0.1, 5.0) # MrnaHalfLife > 0
klean.sequence_identity("ACGT", "ACGG")           # 0.75 — SequenceIdentity ∈ [0,1]
klean.nussinov("GGGAAACCC")                        # 3    — max non-crossing base pairs
```

## What is and is not proven (honest scope)

The Lean kernel checks are about **algorithmic correctness and bounds**, not
about closing open scientific problems. Specifically:

- **Nussinov (`nussinov`)**: the Lean theorem `nussinov_optimal` proves the DP
  recurrence returns *exactly* the maximum number of non-crossing canonical
  base pairs (sound + achievable). This is a proof about the **counting
  algorithm**, with a parameterized pairing cost. It is **not** a claim that
  RNA minimum-free-energy (MFE) structure is "solved": the realistic Turner
  nearest-neighbor energy table is left as open input, and stacking-rule
  optimality under the full Turner model is **not** proven here.
- **Real-valued contracts** (concentrations, kinetics, ages, etc.): the Lean
  proofs are over the reals (ℝ). The Rust/Python runtime uses IEEE-754 `f64`.
  A **formal floating-point error bound is not proven** — runtime values are
  numerically close but the gap between `f64` and ℝ is not certified here.

In one line: we prove **algorithm optimality / invariants (parameterized
cost)**; the empirical energy tables are open inputs, and Real-valued results
carry no proven floating-point error bound (only runtime closeness).

## Contracts

mRNA / Ribosome, sequence analysis, pharmacokinetics, longevity, statistics,
thermodynamics, enzyme kinetics, spectroscopy/transport, growth/population
dynamics, clinical/physiology, molecular biology, structural alignment, and RNA
secondary structure (Nussinov). See the module docstring in `klean` for the
full list and the backing Lean module names.

## Build from source

Requires a Rust toolchain and [maturin](https://github.com/PyO3/maturin).

```bash
maturin build --release          # produces target/wheels/kenoslean-*.whl
pip install target/wheels/kenoslean-*.whl
```

## HTTP server (separate binary)

The same contracts are also served over HTTP by the `klean-server` binary
(Rust/Axum), built with the `server` feature:

```bash
cargo build --release --bin klean-server --features server
./target/release/klean-server    # listens on 0.0.0.0:8090
```

Endpoints (each response carries `"verified": true`):

```
GET /health
GET /v1/gc_content?seq=ATGCATGC
GET /v1/sequence_identity?seq1=ACGT&seq2=ACGG
GET /v1/shannon_entropy?p=0.5
GET /v1/mrna_halflife_concentration?initial=100&decay_rate=0.1&time=5
GET /v1/mrna_halflife?decay_rate=0.1
GET /v1/ribosome_density?n_ribosomes=10&length=100
GET /v1/translation_rate?codon_rate=5&ribosome_density=0.5&mrna_copies=10
GET /v1/first_order_pk?c0=100&ke=0.1&time=5
GET /v1/ic50?ki=10&substrate=5&km=2
GET /v1/michaelis_menten?vmax=100&km=5&substrate=10
GET /v1/biological_age?pheno=45&telomere=42&epigenetic=48
GET /v1/telomere_length?age=50
GET /v1/gompertz_hazard?alpha=0.0001&beta=0.08&time=65
GET /v1/hardy_weinberg?p=0.6
```

## License

MIT

