From 16e325b63bfcc09dc49a9291aa07e8501f9b2f77 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Thu, 15 Oct 2026 10:31:48 +0100 Subject: [PATCH 1/2] docs: an Applications-in-practice section -- the discipline earned on a real pipeline Appends a worked real-world case to docs/EXPLAINME.adoc: the concrete situation in an amplicon-sequencing pipeline in production use where the type, the OND discipline or the algebra earns its keep -- and what the untyped or undisciplined alternative gets wrong. Documentation only; no code changes. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe --- docs/EXPLAINME.adoc | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc index c8ca0f6..a8032a8 100644 --- a/docs/EXPLAINME.adoc +++ b/docs/EXPLAINME.adoc @@ -116,3 +116,16 @@ Caveat: This project is licensed under the Mozilla Public License, v. 2.0. See the `LICENSE` file for details. SPDX-License-Identifier: CC-BY-SA-4.0 + +== Applications in practice + +The worked case is MetaManifold's occupancy reading: each pipeline stage's +measured bytes are typed to a peak in Agda (`TypedPeak`, `GradedStages`), +with this repository's HWM instance carrying the algebra -- the live-sum +boundaries, the drift between handovers, what a stage's end reclaims, and +the folded result matching the largest simultaneous peak. In production the +value is concrete: the pipeline's own memory probe produces numbers, and +the algebra makes those numbers *mean* something -- a stage cannot report +a peak its own window forbids, and the sum of the stage grades equals the +peak the whole run actually occupied. The day-to-day question "which stage +ate the machine?" gets an answer that survives an audit. From 5e36385eca92529cf12b7fc1a7db2ba0e5cdf1db Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Thu, 15 Oct 2026 10:41:25 +0100 Subject: [PATCH 2/2] docs: substantiate the production-measurement claims with the run's evidence CodeRabbit (PR #11) flagged the Applications-in-practice section for presenting the MetaManifold measurements as a production-validated result while Instances/HWM.agda records HWM as a proposal. The claim was real but unlinked, so: name the proposal status and its supersession rule up front, link the concrete case (docs/occupancy-2026-10.adoc, results-2026-10-14.yml, TypedPeak.agda, GradedStages.agda, scripts/check-occupancy.sh), give the measured numbers the typed peak reproduces (9192, 9204, 18380 KiB), and scope the equality to that run's observed interleaving rather than a general production guarantee. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe --- docs/EXPLAINME.adoc | 35 +++++++++++++++++++++++++++++------ 1 file changed, 29 insertions(+), 6 deletions(-) diff --git a/docs/EXPLAINME.adoc b/docs/EXPLAINME.adoc index a8032a8..405a99a 100644 --- a/docs/EXPLAINME.adoc +++ b/docs/EXPLAINME.adoc @@ -123,9 +123,32 @@ The worked case is MetaManifold's occupancy reading: each pipeline stage's measured bytes are typed to a peak in Agda (`TypedPeak`, `GradedStages`), with this repository's HWM instance carrying the algebra -- the live-sum boundaries, the drift between handovers, what a stage's end reclaims, and -the folded result matching the largest simultaneous peak. In production the -value is concrete: the pipeline's own memory probe produces numbers, and -the algebra makes those numbers *mean* something -- a stage cannot report -a peak its own window forbids, and the sum of the stage grades equals the -peak the whole run actually occupied. The day-to-day question "which stage -ate the machine?" gets an answer that survives an audit. +the folded result matching the largest simultaneous peak. Two things should +be said plainly. First, the HWM grade is this repository's proposal +(`Instances/HWM.agda`, STATUS: DESIGNED): it is proven against this +repository's definition, and occupancy-types' own R2-R3 algebra supersedes +it when that repo publishes one -- MetaManifold pins this instance by commit +and re-checks the pin, which is validation of the proposal, not adoption of +a settled standard. Second, "production" below means one measured run, and +the claims are what that run's checks demonstrate. + +The run (hyperpolymath/MetaManifold-WebUI: `docs/occupancy-2026-10.adoc`, +raw records `docs/occupancy/results-2026-10-14.yml`, Agda +`docs/occupancy/TypedPeak.agda` and `GradedStages.agda`, checked by +`scripts/check-occupancy.sh`): two vsearch searches measured under three +orders. Serially the stage's measured peak is the larger search's +(9192 and 9204 KiB); concurrently it is 18380 KiB, the two peaks' sum. The +typed peak -- computed by the HWM sequence law +`max (peak a) (drift a + peak b)` over the measured per-search peaks, the +first search still resident at the second's start -- reproduces all three +measured stage peaks exactly, and the check script re-verifies that +equality, the Agda type-check against the pinned commit, and the counted +bytes at every run. The concurrent equality is that run's observed +interleaving, not a law about interleavings: had the two searches' peaks +not overlapped, the measurement would have come in lower and the grade +would have said so. That is the value in practice: the pipeline's own +memory probe produces numbers, and the algebra makes those numbers *mean* +something -- a stage cannot report a peak its own window forbids, and the +fold that predicted each order's stage peak is the one the run confirmed. +The day-to-day question "which stage ate the machine?" gets an answer +that survives an audit.