Updated 2026-10-17. This is a set of testable product hypotheses, not evidence of demand, revenue, scientific validation, or a broad theorem-proving product.
The public lab demonstrates two toy models. Its strongest mathematical workflow today is a narrow, inspectable certificate for the mean-versus-median comparison of 3–21 stipulated readings under a target interval and bounded one-reading-at-a-time changes. Exact receipts classify reachable outcomes, quantify attained squared-error gaps, locate first tie thresholds from the original readings, and map every decision region with a checkable linear tie rule; odd and even samples are supported. It also lets visitors compose a restricted conditional claim, find exact counterexamples, or verify four established algebraic implications. Four corresponding real-number inequalities have been checked in Lean; v2–v6 proof receipts identify a theorem declaration and pinned source revision, while independent browser and Python checkers validate the mapping. V3–v6 receipts carry independently replayed counterexamples for the other 16 supported universal claims, even when a visitor’s finite grid misses them. V6 uses two explicit endpoint sample families, whose algebra works for every sample size at least three. For each supported count, this is a complete classification of a restricted 20-pair language, not a general conjecture engine. Lean does not inspect the JSON or authenticate measurements. Both the builder and separate browser inspectors are usable on a phone and can check a shared JSON record without Python. The local archive keeps these formats, rechecks stored results, filters proof status explicitly, and exports a portable collection that a second device or separate Python verifier can check before import. The project provides local JSON exports, browser inspection, Node and independent Python verification, teaching activities, and a seeded differential CI gate. It has no hosted customer accounts, generalized symbolic algebra engine, general proof-assistant integration, developer API, enterprise controls, or validated physical/psychological measurement.
The separate Joint Reading Box v1 receipt covers simultaneous, heterogeneous rational uncertainty for 3–5 readings, includes even medians, and gives a constructive tie or a conservative squared-error lead. This is a broader inspectable workflow than the five-reading Target Lens uniform-drift setting; it remains a bounded conditional model. A pilot should test whether prospective users actually need simultaneous perturbations and understand the exact assumptions before making product or pricing commitments.
The new target-horizon receipt adds an inverse question a prospective research or education pilot can inspect: which reference targets preserve a strict Mean or Median result against every permitted one-reading perturbation, and which targets admit a constructive tie? It handles the degenerate case where one movement makes the estimators equal for every target. This is a demonstrable modeling and audit feature; its commercial demand and fitness for any professional domain still require interviews and domain validation.
| Existing option | Publicly described scope | Implication for an INWARD trial |
|---|---|---|
| Desmos | Free math tools and graphing | A generic graphing subscription has a strong free substitute. Test whether inspectable uncertainty receipts solve a distinct problem. |
| GeoGebra | Free noncommercial calculators, classroom activities, and interactive mathematics; commercial use has separate terms | Compete on a specific teachable verification workflow, not the breadth of classroom tools. Do not reuse its assets or embed its tools without checking applicable terms. |
| Mathematica | Commercial, academic, student, and group licensing categories | A narrow browser verifier is not a substitute for a general computation platform. Explore interoperability only for workflows users identify. |
| Lean and Mathlib | Formalized mathematical library and proof-assistant ecosystem | Future formalization should use established tools when the theorem and customer need justify the engineering cost. Current receipts are independently checked by two programs, not Lean-checked proofs. |
These references describe the vendors' own products as checked on the date above. No customer interviews or competitive performance tests have been completed for INWARD here.
- Teaching pilot: a reproducible mean-versus-median lesson with printable worksheets and an instructor guide. Ask instructors whether students can compose a conditional claim, distinguish a counterexample from an unrefuted finite search and a general argument, and independently check a receipt on a phone. Keep the public lab freely accessible during the trial; do not assume schools will pay for content that overlaps free tools.
- Research-methods pilot: an offline workflow for teams comparing estimators under explicit target uncertainty. Ask whether exporting and independently checking a receipt saves review time or catches a decision error. Record the exact use case and sample-size scope; the conditional builder supports 3 through 7 readings, the exact single-reading reversal certificate supports 3 through 21 readings including even central-pair medians, and other tools may remain five-reading.
- Developer verification service: consider a versioned API for validating the current receipt format only after a real integration request. A service would need authentication, resource limits, rate limits, privacy terms, versioned schemas, audit logs, incident response, and support ownership. The CLI is available today; the API is not.
Subscription, university/site licensing, and enterprise verification are pricing models to investigate with buyers, not current products. Do not publish a price or revenue forecast until interviews and pilots establish willingness to pay and delivery cost.
- Observe users completing a real task without developer guidance; record where the assumptions or proof status are misunderstood.
- Collect written, permissioned examples of the workflow and independently reproduce every reported result. Separate hypothetical examples from measured data.
- Ask the buyer who controls budget, what the existing alternative costs them, what security/accessibility procurement requires, and whether they would commit to a scoped pilot. Track refusals as carefully as interest.
- For any paid pilot, specify each tool’s supported sample-size scope, limitations, support channel, retention policy, success metric, and acceptance test in writing.
- Review the repository's MIT license and notices before packaging. Preserve the copyright notice naming Daniel Jacob Read IV and the
CITATION.cffauthorship of Daniel Jacob Read IV and Shane Travis Horman. Inventory rights in images, fonts, and any new integration. Get professional review for trademark, patent, contributor, and licensing questions before asserting exclusive rights.
If teaching pilots produce repeatable learning gains, improve accessible diagrams, facilitator materials, and classroom export. If research teams show a repeated verification need, formalize the stability-edge certificate and verify it independently before expanding the API surface. If neither occurs, keep the lab as an open research and teaching demonstration while gathering better evidence.