# Energy service, peroxide handling, and what a metabolic envelope leaves open This standalone package includes the **complete 19,620-column S7 source matrix**, the exact sparse primal and dual certificates, a reusable finite-horizon metabolic LP, a finite-carrier kinetic module, and a paired-signal inference model. It separates exact conditional exclusions from numerical solutions and synthetic kinetic illustrations. No fitted red-cell preparation or clinical threshold is supplied by the paper or invented here. ## Run and edit Python 3.11 was used. In a virtual environment: ```sh python -m pip install -r requirements.txt python example.py --output outputs python -m unittest -v ``` The default run takes about ten seconds in the development environment. It audits the full rational source, solves fresh numerical LPs, integrates the carrier and signal models, and writes results, CSVs, figures and hashes. `--skip-lp` runs the exact audits and smaller dynamic models without new optimizations. Edit the top of `example.py`: horizon, absolute service requirement, medium, chemical initial amounts/floors, illustrative carrier coefficients and initial redox fractions, and synthetic signal assumptions. All S7 chemical amounts and extents are mmol/gDW; rate bounds are mmol/gDW/hour before integration. The default one-hour zero-stock diagnostic is an algebraic relaxation, **not a viable initial cell**. Auxiliary allocation coordinates retain their encoded scales and are never treated as chemical pools. The exact published plateau audit always uses its frozen premises: restricted medium, one hour, zero chemical stocks/floors. Changing the numerical scenario does not transfer that theorem to the new scenario. Its output is labeled separately. The same dual weights can instead be re-evaluated against explicitly changed bounds, stocks and floors to obtain a new conditional upper certificate. ## Source and reusable components `s7_model.json` is a compact exact representation derived from the original S7 XML, retaining every column and row, source identifiers, decimal bounds, exact rational stoichiometry, row metadata and explicit import masks. `certificates.json` contains only sparse witness/weight entries extracted from the author's records; saved PASS flags and saved residual sums are discarded. `source_manifest.json` ties these files to hashes of the original XML and audit records. The loader checks hashes, dimensions, identifier uniqueness, classification, row references, bounds and independently reconstructed medium masks. Omitted sparse certificate entries mean exact zero; unknown identifiers fail. The optional `freeze_source.py` rebuilds these artifacts from the author workspace: ```sh python freeze_source.py --workspace PATH_TO_AUTHOR_WORKSPACE --output NEW_DIRECTORY ``` It requires the matching `sources/rbcgem_s7.xml`, `plateau_full_audit.json`, `finite_joint_certificate.json` and source license. The XML hash must match the paper. The package itself needs no author-local path or network download. Parsing and classifying XML remain external to the paper's Lean proof; the conversion script makes that step inspectable rather than silently treating it as formal. `SourceModel` handles source alignment and named media. `RationalAudit` checks every primal bound, chemical floor and auxiliary equality, and recomputes every dual residual and interval maximum. `LinearRelaxation` builds the full sparse matrix and exposes objective optimization, service floors, linear observable intervals, individual capacity changes and optional absolute-flux parsimony. `PlateauCertificate` applies the one-witness lemma to audited results. `CarrierPool` handles the separate finite pool, sharp envelope, saturated solution, bounded controls and inverse necessary inventory. `PairedRecovery` handles the separate paired-signal identity, deterministic errors and inference status. For example, to investigate another declared medium: ```python from pathlib import Path from metabolic_model import SourceModel, LinearRelaxation model, certificates, manifest = SourceModel.load(Path('.')) scenario = LinearRelaxation(model, medium='sulfur_closed', time=1, initial={}, floors={}) result = scenario.solve(required_service=1.0, capacity_fractions={'R_GTHOx': 0.5}) ``` Available media are `original`, `sulfur_closed`, `restricted`, and the explicitly artificial `internal_blocked` intervention. All close nonionic sink imports. Restricted additionally closes 56 sulfur-containing and 435 other carbon exchange imports; those sets overlap and must not be added. D-glucose, carbon dioxide and bicarbonate are retained by exact reaction ID. Separately encoded glucose anomers are not merged. Internal-blocked closes four reverse sulfur directions rather than their external supply, which is a different experiment. ## What is freshly certified For signed cumulative extents xi, the model has chemical floors x0+Nc*xi>=ell, auxiliary balances Na*xi=0, and integrated source bounds. Let M=xi_NaKt and Q=2*xi_CAT+xi_GTHP. For nonnegative chemical weights w, signed auxiliary weights y and nonnegative reverse charges alpha, each exact residual is ``` d_j = c_j + alpha_j + w^T Nc_j - y^T Na_j kappa = sum_j max(d_j L_j, d_j U_j) c^T xi <= w^T(x0-ell) + kappa*T + sum_j alpha_j max(-xi_j,0). ``` No solver optimality is trusted for this inequality. The full-source joint certificate yields kappa=25.439041943734505...<25.439042, 53 chemical and 290 auxiliary weights, and three reverse charges of 4 on CYSGLTH, LHCYSTIN and SSGTHRD. HTSULGTHST has zero charge. The code retains all 11 nonzero joint interval costs. The factor 4 is a certificate weight, not a universal ATP cost per peroxide, and w^T x is not Gibbs energy. Net reverse extent is not gross reverse turnover. In the restricted medium, the 1,580-entry exact witness has service 4421041890341877/4273504273504270 and turnover 9400187505686245981195327946603/1446075838260537275756274164820. Fresh upper audits give the exact turnover bound 81256006217701144379925098514861/12500000000000000000000000000000 and exact service ceiling 2586309736197958070773983682319/2500000000000000000000000000000. The turnover certificate retains all eight costs, including four small metabolic residuals; the service certificate has two. One witness at high service is feasible for every lower service demand, so the resulting band is uniform, not a sampled grid. At every demand up to 1.0345238, it implies ``` 6.50048030 <= optimal two-route turnover <= 6.50048050. ``` The exact witness gives a tighter variation allowance of 1.927360900...e-7. This tighter value uses its **unrounded** turnover; subtracting the displayed lower endpoint 6.50048030 would give about 1.97416e-7. Likewise, the gap from the printed service endpoint to the exact ceiling is 9.44791832...e-8; the gap from the exact witness service is 9.21391832...e-8. Both are saved distinctly. The exact ceiling is used for exclusion, not a truncated decimal. Between the witness and the ceiling, the query returns unresolved feasibility, not a fabricated plateau. The source audit also reconstructs HCYSTRDX+TRDRy-LHCYSTIN+GTHP-ESTRONEDHy. Its chemical sum is estradiol + peroxide -> estrone + 2 water. Sulfur, glutathione, thioredoxin and nicotinamide carriers cancel, but **eight enzyme-allocation terms remain**. This explains why a carrier-uptake budget need not bound carrier reuse; it is not a self-contained feasible cycle or an observed human pathway. ## Fresh numerical optimizations and peroxide fates The default scenario fixes service at least 1.0, then maximizes Q. It obtains Q about 6.500480497, peroxide import 1000 and terminal peroxide 993.499519503. The next LP holds service and Q within 1e-8 and minimizes terminal peroxide. This run keeps import 1000 but consumes the remainder through uncounted routes. The last LP minimizes total absolute extent and removes the gratuitous handling, reducing import to about 6.500480487. These are fresh solutions at the configured service, not copies of the paper's different saved vectors and service values. Degenerate optima and different solver versions can select other valid vectors. Every numerical result records the full peroxide-row contributions, internal production, import/export, counted and other consumption, terminal amount, minimum chemical-floor slack and maximum auxiliary residual. No negative numerical value is silently clipped into a feasibility certificate. Small residuals are numerical diagnostics; the separate exact witness establishes the plateau. The GTHOx upper-bound fractions 0, 1/2 and 1 give about 4.30108, 5.40078 and 6.50048 turnover at the same service. These three perturbations are not a measured activity response or a globally affine law. Shared reductase allocation is retained through all source rows. Numerical parsimony weights chemical and auxiliary extents equally in their encoded scales; it is a declared selection rule, not a unique physiological objective. A terminal floor does not bound the peroxide peak, cumulative exposure or damage. These amounts are not concentrations: the model supplies no compatible water volume per gDW. No dose, tolerance or protective endpoint is inferred. ## The missing finite-carrier constraint The independent two-state module has reduced carrier g, total C, oxidation v<=a*g and regeneration u<=b*(C-g), with g'=u-v. Its sharp integrated bound is ``` V(T) <= a*b*C*T/(a+b) + a/(a+b)*(g0-b*C/(a+b))*(1-exp(-(a+b)*T)). ``` The implementation uses `expm1` and a short-time series to preserve the quadratic startup term, and directly integrates saturated or user-supplied bounded controls. Saturated controls attain the bound. Zero carrier forces zero turnover. The long-time rate is the harmonic value C/(1/a+1/b), but an initially reduced pool can exceed that average over a short horizon by drawing down its stock. Restoring the initial pool gives the harmonic ceiling without that transient allowance. With illustrative a=2/h and b=1/h, one-hour turnover per unit carrier is about .45551, .66667 or 1.08898 when the reduced fraction is 0, 1/3 or 1. The default C=1 is an arbitrary normalization, not a physiological pool. The inverse method reports the necessary carrier for a target extent under these chosen coefficients; it is not a supported measurement of red cells. More carrier states, synthesis, export and substrate-dependent rates require extending the module. ## Paired-signal inference The synthetic untreated/treated equations are D'=q-kD and Cs'=r*q-kCs, with a shared initial peak and one constant r. Input q and effective reduction k vary with time in the generated example. Their difference cancels q, giving z=(Cs-rD)/((1-r)*peak)=exp(-integral k). This identifies integrated **effective** reduction under the model, not an intrinsic enzyme constant. An added treated-equation discrepancy e is integrated as Gamma=integral|e|/((1-r)*peak). The saved trace checks |z-exp(-K)|<=Gamma. Raw-error propagation includes uncertainty in the shared initial peak rather than treating normalized ratios as independent observations. Inference returns a bounded K interval only when the transformed lower endpoint is positive; otherwise it explicitly reports no finite upper identification or incompatibility. Log endpoints use interval arithmetic with outward float conversion. These are deterministic error allowances, not confidence intervals. The paper's synthetic pairs (.8,.5), then (.7,.6), with raw errors .01 and a common r in [0,.05], violate monotonicity: the later-minus-earlier numerator is at least .08+.08*r. The test preserves a common r, and an optional discrepancy allowance must be included before rejection. Passing a necessary consistency test does not validate the intervention or establish a future prediction. No donor data are used. ## Verification, files and licensing Seven scientific test groups check the entire source audit, malformed IDs/signs and an infeasible witness, medium distinctions and carrier cancellation, uniform versus unresolved service ranges, numerical source accounting, sharp carrier bounds including zero-stock and very-short-time cases, and paired-error inference. Fresh symbolic calculations check the adjoint, attaining trajectory, quadratic startup, harmonic limit and signal cancellation. The paper's formal proof receipts are not rerun or promoted to cover the XML parser or biological premises. `results.json` includes all exact audit quantities and nonzero residuals, numerical LP diagnostics and kinetic/inference results. `dual_costs.csv`, `carrier.csv` and `paired_signals.csv` expose the computations. PNG/SVG figures and `console.txt` summarize them. `run_metadata.json` hashes both model/code inputs and outputs. Paper SHA-256: `a8cd8efce97007780e7b88fc7f19dc94a31c3e7da20f22b66dbc3f1a0db97774`. Original S7 XML SHA-256: `b2703b5a730cf12890034f01df92506de5facd9ecea5751a795e982b88557f64`. The full paper, its check script, exact witness generator, certificate scripts and original local XML were inspected. Scientific source data are credited to Haiman, Key, D'Alessandro and Palsson, *RBC-GEM*, PLOS Computational Biology (2025), [doi:10.1371/journal.pcbi.1012109](https://doi.org/10.1371/journal.pcbi.1012109). The source repository's Creative Commons Attribution 4.0 International license is included unchanged in `RBC_GEM_LICENSE.md`; the model transformation is described above and in the manifest. This is an adaptation, with no source-author endorsement implied. MIT is proposed for the new example code pending the owner's choice; this README makes no new code license grant or change to third-party data terms.