Pith. sign in
module module moderate

IndisputableMonolith.Physics.QuarkCoordinateReconciliation

show as:
view Lean formalization →

Module separating core RS quark rung assignments (integer steps on the phi-ladder) from phenomenological quarter-step conventions used in some mass fits. Physicists comparing RS mass predictions to PDG light-quark masses cite the layer tags and the core up/down rung tables. Pure definitional infrastructure: inductive layer tags, conversion maps, and concrete integer rung lists; no deep proofs.

claimThe module introduces a model-layer tag distinguishing the core integer-rung quark ladder from a quarter-step phenomenological convention, together with the core up-quark and down-quark rung lists and the maps sending a quarter index to a real exponent or to the nearest integer rung.

background

In Recognition Science, particle masses sit on a geometric $\phi$-ladder: $m = \mathrm{yardstick}\cdot\phi^{rung-8+\mathrm{gap}(Z)}$. The core theory works with integer rungs. Some phenomenological fits have explored quarter-integer steps to fine-tune light-quark masses against experiment.

This module enumerates the two layers (core versus convention) and records the integer rungs used for up and down quarks in the core layer. It also supplies the conversion maps from a quarter-ladder index into a real exponent and into the nearest integer rung, so any quarter-step fit can be compared against the integer core without ambiguity of coordinates.

The only external dependency is the Constants module ($\tau_0=1$ tick and the golden ratio $\phi$).

proof idea

This is a definition module, no substantial proofs. It declares an inductive ModelLayer (core vs convention), a Convention type, boolean classifiers (core uses integer rungs; quarter ladder is hypothesis), the quarter-step size, conversion functions from quarter index to real and to nearest integer, and the concrete CoreUpQuarkRungs / CoreDownQuarkRungs tables with their list projections.

why it matters in Recognition Science

Quark mass predictions are a primary empirical test of the RS mass formula on the phi-ladder. Without an explicit layer tag, a reader cannot tell whether a quoted rung is forced by the forcing chain or is an ad-hoc quarter-step adjustment. The module supplies that tag and the core up/down tables so downstream mass theorems can state their hypotheses cleanly. No parent theorems are listed yet (used_by empty); the module is infrastructure for later Physics mass-comparison results.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (25)