current_chain_distinct
plain-language theorem explainer
The four generation-step integers 13, 11, 6 and 8 are pairwise distinct. A physicist enumerating mass-ladder chains under Q₃ cube invariants at D=3 would cite this to confirm the structural filter selects a repetition-free set. The proof is a one-line term-mode wrapper that refines the six-way conjunction and discharges each inequality by norm_num.
Claim. $13, 11, 6, 8$ are pairwise distinct: $13 ≠ 11 ∧ 11 ≠ 6 ∧ 6 ≠ 8 ∧ 13 ≠ 6 ∧ 13 ≠ 8 ∧ 11 ≠ 8$.
background
The Step Value Enumeration module narrows Gap A in the forcing chain by treating the four values {13, 11, 6, 8} as Q₃ cube invariants at D=3. Here 13 equals E+1 (edge plus one), 11 equals E-1 (edge minus one), 6 equals the face count F, and 8 equals the vertex count V, with E=12 the base edge count from the Euler characteristic on the boundary of the 3-cube. The module enumerates finite alternatives under the endpoint sum constraint N₃=55 and middle sum W=17, then isolates the current choice by additional natural filters. Upstream, the Chain structure supplies the minimal relation axioms used to define cyclic step sequences, while foundational arithmetic lemmas supply the integer comparison operators.
proof idea
The proof is a term-mode proof. Refine splits the top-level conjunction into six separate goals; norm_num then reduces each numerical inequality to a decidable statement and closes it.
why it matters
The theorem supplies one of the structural constraints required to show that the chain (13, 11, 6, 8) is the unique selection satisfying the E±1 filter inside the cube-invariant set. It therefore advances the module’s goal of making the modeling choice explicit rather than hidden, feeding directly into the enumeration of middle and endpoint pairs. In the broader Recognition framework it supports the identification of generation steps with the eight-tick octave and D=3 spatial dimensions (T7, T8) while leaving open the question of whether the cube-invariant filter itself follows from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.