def
definition
color_offset
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Masses.BaselineDerivation on GitHub at line 188.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
185the edge count of one face: c = 2^(D−1) = 4. -/
186
187/-- **B-25 DERIVED**: Color offset from face edge count. -/
188def color_offset : ℕ := edges_per_face D
189
190theorem color_offset_eq : color_offset = 4 := by
191 exact edges_per_face_at_D3
192
193/-- Color offset equals quark baseline (same geometric origin). -/
194theorem color_offset_eq_quark_baseline : color_offset = quark_baseline := rfl
195
196/-! ## B-14: Generation torsion ordering 0 < E_pass < W
197
198The three generations have torsion offsets {0, E_pass, W}.
199The ordering 0 < E_pass < W is a consequence of cube arithmetic:
200E_pass = E − 1 = D·2^(D−1) − 1 and W = E_pass + F = E_pass + 2D.
201Since F = 2D > 0, we have W > E_pass.
202Since D ≥ 1 implies E ≥ 1, we have E_pass ≥ 0; for D ≥ 2, E_pass > 0. -/
203
204/-- **B-14 DERIVED**: Generation torsion is strictly ordered. -/
205theorem generation_ordering :
206 (0 : ℕ) < passive_field_edges D ∧
207 passive_field_edges D < wallpaper_groups := by
208 constructor
209 · -- 0 < 11
210 native_decide
211 · -- 11 < 17
212 native_decide
213
214/-- The ordering generalizes: for any D ≥ 2, 0 < E_pass(D) < W(D). -/
215theorem generation_ordering_general (d : ℕ) (hd : 2 ≤ d) :
216 0 < passive_field_edges d ∧
217 passive_field_edges d < passive_field_edges d + cube_faces d := by
218 constructor