Skip to content

docs: an Applications-in-practice section #11

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 2 commits into from
Oct 15, 2026
Merged

docs: an Applications-in-practice section #11

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
16e325b
docs: an Applications-in-practice section -- the discipline earned on…
hyperpolymath Oct 15, 2026
5e36385
docs: substantiate the production-measurement claims with the run's e…
hyperpolymath Oct 15, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 36 additions & 0 deletions docs/EXPLAINME.adoc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,3 +116,39 @@ 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. 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.
Loading