Pith. sign in
module module moderate

IndisputableMonolith.Verification.QuarkCoordinateUnification

show as:
view Lean formalization →

Unifies two coordinate presentations of quark masses on the phi-ladder: a core-exponent form and a residue form. Shows they recover the same mass when the residue is positive, so either bookkeeping system may be used. Downstream quark forward pipelines cite the equivalence to keep Convention A predictions independent of coordinate choice.

claimTwo mass coordinates on the $\varphi$-ladder are equivalent: the core-exponent mass $m=y\,\varphi^{e}$ and the residue form built by extracting residue $r$ from the core and recovering the yardstick. For positive residue, core mass equals residue mass, the residue recovers the core exponent, and the coordinate systems are interchangeable.

background

In Recognition Science, masses sit on a geometric $\varphi$-ladder: mass equals a sector yardstick times $\varphi$ raised to an integer rung offset by a charge-band gap. For quarks, two bookkeeping conventions appear. The core-exponent form packages rung and gap into a single exponent $e$. The residue form isolates a residual coordinate $r$ and recovers the yardstick from that residue.

This Verification module imports only Constants (RS-native units and $\varphi$). Sibling definitions introduce coreExponent, coreMass, residueMass, maps between them (residueFromCore, yardstickFromResidue), and the equality lemmas that identify the two systems. The local setting is algebraic identity, not phenomenology: no PDG inputs enter.

proof idea

Definition layer first: core exponent and core mass, residue mass, and the two conversion maps (residue from core; yardstick from residue). Equality lemmas then discharge the identification: core mass equals residue mass when the residue is positive; residue recovers the core; a recovery lemma rebuilds the residue coordinate; a top-level statement asserts the coordinate systems are equivalent. Structure is definitional scaffolding plus short algebraic equalities, not a deep tactic chain.

why it matters in Recognition Science

Feeds the unified quark forward pipeline (QuarkForwardPipeline), which predicts all six quark masses under Convention A only: sector yardsticks from cube geometry, integer rungs from generation torsion, and gap$(Z)$ from the charge-band map, with the explicit property of no PDG targeting. Coordinate unification lets that pipeline switch between core-exponent and residue presentations without changing numerical output. Anchors the RS mass formula (yardstick $\times\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) in a dual-coordinate, machine-checked form used by later verification stages.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (9)