module module moderate

`IndisputableMonolith.Physics.QuarkCoordinateReconciliation`

The QuarkCoordinateReconciliation module enumerates model layers and conventions for aligning quark coordinates with the Recognition Science phi-ladder. Physicists modeling up and down quark rungs cite these when applying the mass formula yardstick times phi to the power of rung minus eight plus gap. It is a definition module containing no proofs.

claimThe module enumerates model layers for quark coordinate reconciliation on the phi-ladder, including conventions for integer rungs and quarter-step hypotheses.

background

This module sits in the physics domain and imports the RS time quantum τ₀ = 1 tick. It introduces ModelLayer and Convention objects together with core integer-rung usage and quarter-ladder hypotheses. These definitions support mapping quark coordinates onto the phi-ladder used in the mass formula.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the layer enumeration required by downstream quark-mass theorems that invoke the phi-ladder mass formula. It connects directly to the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain. It leaves the quarter-ladder hypothesis open for later discharge.

scope and limits

Does not compute numerical quark masses.
Does not prove the quarter-ladder hypothesis.
Does not derive the phi-ladder mass formula.
Does not reference the alpha band or G constant.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (25)

inductive ModelLayer L92
inductive Convention L99
def convention_layer L105
theorem core_uses_integer_rungs L110
theorem quarter_ladder_is_hypothesis L114
def quarter_step L120
def quarter_to_real L123
def quarter_to_nearest_int L126
structure CoreUpQuarkRungs L131
structure CoreDownQuarkRungs L137
def core_up_rungs L143
def core_down_rungs L144
structure QuarkQuarterLadderPositions L149
def hypothesis_positions L158
theorem nearest_int_positions L161
theorem conventions_differ_top_quark L175
theorem conventions_differ_charm L181
theorem conventions_differ_bottom L187
def quark_fractional_rung_necessity L200
structure Resolution L206
def gap6_resolution L227
theorem gap6_resolved L230
def core_dependent_claims L235
def hypothesis_dependent_claims L243
theorem hypothesis_claims_properly_located L251