theorem
proved
chain_unique_given_edge_pair
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Masses.StepValueEnumeration on GitHub at line 164.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
161
162/-- If the chain contains both E+1 and E-1 as adjacent values, the chain is
163 uniquely determined. -/
164theorem chain_unique_given_edge_pair
165 (a b c d : ℕ)
166 (h_chain_partition : a + 2*b + 2*c + d = 55)
167 (h_middle : b + c = 17)
168 (h_a_eq : a = 13) -- E+1
169 (h_b_eq : b = 11) -- E-1
170 :
171 a = 13 ∧ b = 11 ∧ c = 6 ∧ d = 8 := by
172 subst h_a_eq h_b_eq
173 have hc : c = 6 := by omega
174 have hd : d = 8 := by omega
175 exact ⟨rfl, rfl, hc, hd⟩
176
177/-- The chain (13, 11, 6, 8) is uniquely determined by the edge-pair filter
178 (13 = E+1, 11 = E-1) plus the partition and middle constraints.
179
180This is a CONDITIONAL UNIQUENESS result: given that the chain contains the
181edge-symmetric pair (E+1, E-1) as its leading two values, the remaining
182values are forced. -/
183theorem current_chain_unique_modulo_edge_pair_filter :
184 ∀ (a b c d : ℕ),
185 a + 2*b + 2*c + d = 55 →
186 b + c = 17 →
187 a = 13 → b = 11 →
188 (a, b, c, d) = (13, 11, 6, 8) := by
189 intro a b c d h_part h_mid h_a h_b
190 have ⟨_, _, hc, hd⟩ := chain_unique_given_edge_pair a b c d h_part h_mid h_a h_b
191 rw [h_a, h_b, hc, hd]
192
193/-! ## Constraint 5: The Euler-Characteristic Interpretation
194