Pith. sign in
module module moderate

IndisputableMonolith.Verification.QuarkSectorAudit

show as:
view Lean formalization →

Audit module for the two competing coordinate conventions that place quarks on the Recognition Science φ-ladder. Convention A uses absolute rungs; Convention B uses residues. A particle physicist checking RS mass predictions lands here to see why light-quark accuracy and generation spacing disagree across frames, and that no reconciliation is closed yet.

claimThe module records two quark coordinate conventions on the $\varphi$-ladder: Convention A (absolute rungs) and Convention B (residues), comparison facts (distinct references, rung types, and generation spacing), light-quark and skeleton-only accuracy flags, and the status that the conventions are not yet reconciled.

background

In Recognition Science, masses sit on a discrete $\varphi$-ladder via the yardstick formula $\mathrm{yardstick}\cdot\varphi^{rung-8+\mathrm{gap}(Z)}$. Quarks therefore need a coordinate convention assigning each flavor a rung (or residue) and a generation index.

This verification module isolates two conventions present in the codebase. Convention A indexes by absolute rung numbers; Convention B indexes by residues. Sibling declarations record that the frames use different references and rung types, that generation spacing differs, and that light-quark versus skeleton-only accuracy statements are tracked separately.

The sole external import is Constants (RS-native units, including the time quantum $\tau_0=1$ tick). No forcing-chain step is re-proved here.

proof idea

Definition and status module, not a theorem package. It introduces a QuarkConvention type, the two concrete conventions (rungs vs residues), a UnifiedQuarkSector bundle, comparison facts (different references, different rung types, generation spacing differs), accuracy flags (light quarks, skeleton-only), and a currentStatus / no_reconciliation_yet marker with a ReconciliationProof placeholder. There is no closed proof equating the frames.

why it matters in Recognition Science

Quark masses are a primary empirical test of the RS $\varphi$-ladder. Until the two coordinate conventions are shown equivalent (or one is selected), sector predictions remain convention-dependent. The module's no-reconciliation status marks that open verification gap. No downstream theorems currently import it (used_by is empty); consumers of a unified quark sector would need this audit closed before citing a unique RS quark spectrum. It does not touch T5–T8, RCL, or the $\alpha$ band directly.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)