Pith. sign in
module module moderate

IndisputableMonolith.Verification.QuarkCoordinateUnification

show as:
view Lean formalization →

Unifies two coordinate presentations of quark masses on the integer-rung φ-ladder: a core-exponent form and a residue form. Supplies the maps between them and proves they recover identical masses when the core is positive. The forward quark pipeline imports this so Convention A can switch coordinates without changing predictions.

claimOn the $\varphi$-ladder, the core-exponent mass $m_{\mathrm{core}}=y\,\varphi^{e}$ and the residue mass built from a residue coordinate $r$ are equivalent: for positive core data the residue recovered from the core equals the core, and the yardstick recovered from the residue restores the original mass. The two coordinate systems therefore predict the same quark masses.

background

Recognition Science places particle masses on a discrete $\varphi$-ladder. The native mass formula is yardstick times $\varphi$ to an integer power fixed by rung, generation torsion, and a charge-band gap $g(Z)$. Two bookkeeping conventions appear in the quark sector: a core exponent that packages the full power in one integer, and a residue coordinate that isolates the fractional or sector-relative piece after a fixed offset.

This module lives in the Verification domain and only imports Constants (for the RS tick and related native units). It introduces the core exponent, the core and residue mass maps, the residue-from-core and yardstick-from-residue recoveries, and the algebraic identities that relate them. No PDG targets enter; the objects are pure ladder arithmetic.

The local goal is coordinate hygiene: show that switching between core and residue presentations does not change the predicted mass, so a single forward pipeline can use either form.

proof idea

Definition layer first: coreExponent, coreMass, residueMass, residueFromCore, and yardstickFromResidue fix the two coordinate charts and the recovery maps. Equivalence is then pure algebra on positive reals and integer powers of $\varphi$: core_eq_residue_of_positive and residue_eq_core show the round-trip on the exponent side; recover_residue_coordinate closes the residue recovery; coordinate_systems_equivalent packages the full equivalence of the two mass presentations. No analytic estimates or external data; only field and exponent arithmetic.

why it matters in Recognition Science

The sole downstream consumer is Verification.QuarkForwardPipeline, the unified six-quark forward predictor that uses Convention A only (sector yardsticks from cube geometry, integer rungs from generation torsion, gap from the charge-band map) and explicitly forbids PDG targeting. That pipeline needs a single, convention-stable mass coordinate; this module supplies the proof that core and residue charts agree, so the pipeline can compute in whichever form is convenient without splitting predictions.

In the broader RS chain the result sits under the mass-ladder layer (yardstick $\times\varphi^{\mathrm{rung}-8+g(Z)}$), not under T5–T8 forcing. It is bookkeeping infrastructure that keeps the quark sector auditable and free of hidden dual conventions.

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)