theorem
proved
conventions_differ_bottom
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.QuarkCoordinateReconciliation on GitHub at line 187.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
184 norm_num
185
186/-- The conventions also differ for bottom quark -/
187theorem conventions_differ_bottom :
188 (core_down_rungs.b : ℚ) ≠ hypothesis_positions.bottom := by
189 simp only [core_down_rungs, hypothesis_positions]
190 norm_num
191
192/-! ## Hypothesis marker (no axiom) -/
193
194/-- **HYPOTHESIS**: Quarks require fractional rungs for sub-percent accuracy.
195
196This is an EMPIRICAL observation, not a derived theorem:
197- The core integer-rung model predicts quark masses with larger errors
198- The quarter-ladder hypothesis achieves <2% accuracy for heavy quarks
199- This definition is a *marker* for hypothesis-dependent claims; it is **not** an `axiom`. -/
200def quark_fractional_rung_necessity : Prop :=
201 (core_up_rungs.t : ℚ) ≠ hypothesis_positions.top
202
203/-! ## Resolution Status -/
204
205/-- Formal resolution of Gap 6 -/
206structure Resolution where
207 /-- Status: RESOLVED by layer separation -/
208 status : String := "RESOLVED_BY_LAYER_SEPARATION"
209 /-- Resolution method: explicit layer assignment, not equivalence -/
210 method : String := "Layer separation (Core vs Hypothesis)"
211 /-- Core convention: integer rungs -/
212 core_convention : Convention := .IntegerRung
213 /-- Hypothesis convention: quarter-ladder -/
214 hypothesis_convention : Convention := .QuarterLadder
215 /-- Whether equivalence was proved: NO (and not required) -/
216 equivalence_proved : Bool := false
217 /-- Reason equivalence not needed -/