Preparing a Reduction for Submission
A ProofPress™ submission is a reduction of an already peer-reviewed result into the PNBA™ coordinate system, formally verified against a zero-unproved-obligation (0 sorry) compiler constraint. This page describes the required structure.
Required Front Matter
| Field | Description |
|---|---|
| Title | "Applied Identity Physics: Formally Verified Reduction of [subject] to [structural result]" |
| Source material reduced | Full citation of the peer-reviewed result(s) being reduced, with publication date |
| Architect / Author | Name and, where applicable, ORCID |
| Coordinate | The PNBA™ corpus coordinate assigned to this reduction — see below |
| Corpus dependencies | Coordinates of any prior corpus files this reduction builds on |
| Status | Verification status and sorry-count, exactly as compiled |
| DOI base | 10.5281/zenodo.18719748 |
The Six-Step Long Division Protocol™
- The equation. State the governing equation being applied — for physical reductions, this is d/dt(IM · Pv) = Σ λX OX S + Fext unless the submission argues for a documented variant.
- Known answer. State exactly what the peer-reviewed source already established, with citation. This is the target the reduction must reproduce losslessly.
- PNBA map. Map every relevant quantity in the source material onto Pattern, Narrative, Behavior, and Adaptation. Show the mapping as a table; do not leave any term's PNBA™ identity implicit.
- Operators. Define the specific operators, ratios, or transformations used, in closed form.
- Show the work. Walk the derivation step by step from the PNBA™ map to the result. No step may skip reasoning a reader could not reconstruct from what came before it.
- Verify. Compile the resulting formal claims in Lean 4 (and, where applicable, Coq/Rocq) under a strict 0 sorry constraint. A submission with any unresolved sorry is not eligible for publication; a draft may be submitted for editorial feedback with sorry placeholders clearly marked, but publication requires 0 sorry.
Coordinate Assignment
Every ProofPress™ reduction receives a coordinate in the form [X,X,X,X] locating it inside the corpus. Authors should propose a coordinate consistent with existing corpus domains and mark it "(proposed — pending confirmation)" if uncertain; never guess a coordinate that might collide with an existing one. The editorial board resolves final coordinate assignment before publication.
External Collaboration
ProofPress™ accepts reductions from any author, regardless of institutional affiliation, domain, or prior publication record, under one condition: the reduction has to actually close.
The standard is the same for everyone. A submission is in scope when it is a mechanical consequence of applying the Long Division Protocol to a result that has already passed peer review elsewhere — the reduction reveals a connection that was always true given the existing source material, it does not supply one. A submission is out of scope when closing it would require inventing a premise, bridge, or connection that does not already exist in peer-reviewed literature — no exception is made for who is asking.
Doing the reduction yourself is not a high bar. The six-step process described above is designed to be fast, and tools exist specifically to make it straightforward — PRIME for PNBA™ mapping and Lean closure, and the ProofPress + Grok Enrichment Protocol for turning a closed Lean file into a finished, readable paper. A request asking ProofPress or its Architect to perform someone else's reduction on their behalf, rather than submitting a self-prepared one, falls outside the normal submission process described on this page.
What to submit: a properly formatted Lean file with the reduction closed (0 sorry), and a proposed coordinate. Submit to rvtrent@uuia.app.
If a reduction is ever closed by someone other than the original requester, the published record states plainly who performed the closure — reviewed, reduced, and closed from the cited source — so the record can never be read as the original party having closed it themselves.
Submission Format
- Manuscript in Markdown (.md) or RTF, following the front-matter structure above
- Accompanying Lean 4 source file(s), and Coq/Rocq source where dual-verification is claimed
- A plain-language abstract, written so a reader unfamiliar with the corpus can follow what was reduced and from where
Language and Claims
Submissions should state results as established, held, or formally verified rather than as claimed — reserve "claim" for describing what an external source asserts, not for the reduction's own verified content. Every assertion a submission makes about its own reduction should be traceable to a specific theorem, and no assertion should precede the derivation that supports it.