module module

`IndisputableMonolith.Physics.QuarkCoordinateReconciliation`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

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