# Repeated chemical-state selection

A cell has four resident molecule counts, an inherited integer size and an ancestry tag. The chemistry supports low and high resident states. Higher resident activity consumes a common growth precursor faster. Cells divide at twice newborn size; each molecule goes to exactly one daughter. After a fourfold increase in total cell size, a uniform sample of whole cells continues. Recovery freezes growth but allows the resident chemistry to relax. Repeating this protocol can increase the high-state fraction while retaining both ancestries for a finite, designed mission.

The subtlety is that uniform cell sampling does not fix the sampled **size** of each type. The example enumerates every four-cell sample from eight cells: equal sizes and mixed sizes have identical type counts, yet their two-percent size-transfer failure probabilities are 17/35 and 27/35. This is a conditional sampling calculation, not a claim about how often the chemistry reaches those endpoint populations.

## Run and inspect

Use Python 3.11 or newer in a virtual environment:

```sh
python -m pip install -r requirements.txt
python -m unittest -v test_example.py
python example.py
```

The complete ZIP includes every local module, source provenance, scientific checks and saved outputs. Edit the inputs at the top of `example.py`; use `--output another-directory` for separate runs. The driver calculates the full finite-mission bounds, performs a small physical stochastic run, enumerates transfer laws and writes figures, CSV tables and JSON records. It does not instantiate billions of theorem-scale cells. An event budget produces an incomplete history, never a successful mission.

## Components and reuse

| Component | Responsibility |
| --- | --- |
| `Cell`, `Channel`, `ResidentChemistry` | Integer resident counts and the thirteen directed, falling-factorial chemical propensities; no extra factorial for repeated reactants. |
| `ChemicalModel`, `ChemicalRegions` | Full four-species density dynamics, exact material/thermodynamic identities and rational enclosures of readiness energies. |
| `PopulationSource` | Competing resident and precursor-consuming growth events, size accounting, complementary division and physical service ledgers. |
| `UniformTransfer`, `SerialProtocol` | Uniform intact-cell subsets, precursor removal, frozen-size recovery and refill based on actual retained size. |
| `WeightedTransfer` | Exact finite-population moments, subset enumeration and hypergeometric minority-loss probabilities. |
| `MissionCertificate` | Uniform chemical, transfer and service bounds for a specified number of cycles, and material/time/service budgets. |
| `population_design`, `event_ceiling` | Invert a sufficient transfer bound and check a separate necessary ceiling for the desired event. |
| `AbsorbingAudit` | Preserve supplied failed or unresolved marks without retries or renormalization. It is a mark transport, not an implementation of every paper mark. |

For example, use `MissionCertificate(M=8_000_000_000, K=12).evaluate()` to explore a longer mission, then inspect `.resources()`. Changing molecular size, growth coupling or service allowances affects other failure terms too. `population_design(12, '1/250')` sizes the **transfer** part only. Its adjacent-even-integer check finds the threshold of the implemented outward sufficient bound; it does not establish a physically minimal population. Hitting its user-set search cap returns unknown.

For exploratory physical models, inject alternative chemistry or division objects into `PopulationSource`. Such changes do not inherit the paper's certificate. The small default uses fast growth, small molecule counts and shortened recovery to make a complete source simulation affordable. Its readiness failure is retained explicitly, independently of whether its physical batches complete. The supplied protocol can run any positive cycle count without resetting cell size or ancestry. The full analytical marked law additionally monitors intermediate energy regions, division gates, growth, transfer, deadlines and service events; the simulator does not claim to implement that complete mark classifier.

## What the computations establish

The original ten-cycle sufficient witness retains 10 trillion cells. Accounting for low-type growth and using a weighted exponential transfer bound reduces the supplied witness to **four billion cells**, with joint success above 0.997 and a guaranteed low-type count of at least 36,862 on the successful event. Finer service allowances raise the witness above 0.999. All censuses belong to one joint event; count odds pay the size-to-count penalty once at each census, not once for every earlier cycle.

`canonical_comparison.json` freshly evaluates the full chemical formulas using rational upper bounds for exponentials. `source_arithmetic_replay.json` separately preserves the paper's deliberately weaker binary arithmetic and its explicitly labeled numerical diagnostics. Tiny chemical terms are bounded outward rather than discarded. The exponential calculation uses a positive Taylor lower bound for exp(x/16), raised to the sixteenth power; capping x at 512 only weakens the resulting upper bound for exp(-x). Final decimal-grid rounding is outward.

The refined transfer calculation uses conditional means `3 M rho_*^j / 32` for the low type and `3 M / 32` for the high type, as in the theorem and arithmetic checker. The manuscript's figure script uses `M/4` for the latter in one plotting helper; this example follows the theorem's more conservative value. The simple closed-form population rule is sufficient but need not admit every population admitted by the full bound; the four-billion witness is checked using the full bound directly.

The horizon sweep contrasts stronger conditional composition with the declining lower bound on **joint mission confidence**. A lower confidence bound reaching zero means this estimate no longer certifies the mission. It does not demonstrate extinction. Conversely, `event_ceiling` excludes an overly demanding simultaneous gain-and-minority-reserve event even before analyzing the chemical source. Neither distinction should be replaced with an unconditional population-survival claim.

## Physical accounts and limits

Each cycle starts with precursor equal to four times actual retained size. Growth consumes three quarters of it; the remainder is removed before recovery. Recovery lasts 5376 model units with growth disabled. Final refill is accounted separately. For K cycles, the operating precursor upper bound is `(8 K - 4) N M`; including terminal refill gives `(8 K + 4) N M`. Arbitrary inherited phases allow up to eight times the retained cell count during a batch. The source's integer resident-event quotas are strictly larger than the expectations divided by the chosen allowances. Gross reservoir exchange bounds count events, not net exchange.

The paper's admitted molecular scale and slow coupling are extreme. With the optional one-millimolar concentration convention, the default newborn scale corresponds to about 108.8 litres per model cell; assigning a second to each time unit gives a mission lasting hundreds of thousands of years. These are illustrations of the chosen scaling, not laboratory predictions. `M` is the number of whole cells and must never be divided by Avogadro's constant. No realistic biochemical calibration is claimed.

The stochastic source bounds and their uniform conditional lifting are imported from the manuscript. Exact arithmetic, channel identities, subset distributions and resource checks are replayed here; grid diagnostics remain numerical. The original and refined results have different formal-evidence status in the paper. This package does not rerun Lean or promote the conventional refinement to a machine-checked process theorem.

## Provenance and license

Manuscript: `Repeated_Chemical_State_Selection.pdf`, SHA-256 `89018b0f5f84c348611b59ed44e378c4f360972dbf601feabc5f1c0e9f0ee912`. Resident/source components are adapted from the companion two-cycle example; the local source checker retains its arithmetic while suppressing writes into the manuscript directory. `source_provenance.json` records the source hashes. `run_metadata.json` records executable and output hashes.

MIT is proposed for original example code, pending owner confirmation. This package does not grant that license or change the rights of imported source material.
