CostConnected
plain-language theorem explainer
CostConnected defines an inductive reachability relation on Boolean assignments for a given CNF formula, linking two assignments when a path exists through single-bit flips each carrying positive J-cost edge weight. Researchers analyzing the J-cost Laplacian quadratic form or SAT encoding complexity would cite this relation to track connectivity on the hypercube. The definition is supplied directly by two constructors: a reflexive base case and a step rule that extends along positive-weight edges.
Claim. For a CNF formula $f$ on $n$ variables and assignments $a,b : [n]→{0,1}$, the relation CostConnected$(f,a,b)$ holds when either $a=b$, or there exists $k$ with $w(f,a,k)>0$ (where $w$ is the absolute difference of satJCost values) such that CostConnected$(f, a$ flipped at $k, b)$ holds.
background
The module JCostLaplacian equips each CNF formula with a weighted graph on the Boolean hypercube whose vertices are assignments (Fin n → Bool) and whose edges are Hamming-distance-1 flips. Edge weight is given by jcostEdgeWeight, the absolute difference |satJCost f a − satJCost f (flipBit a k)|. CNFFormula is the structure holding a list of clauses together with the variable count. CostConnected is the smallest relation containing the reflexive pairs and closed under extension by any positive-weight edge.
proof idea
The declaration is an inductive definition. It is introduced by the two constructors refl (base case) and step (inductive case that requires a positive jcostEdgeWeight and recurses on the flipped assignment). No lemmas or tactics are invoked; the inductive type itself encodes the transitive closure of the positive-weight adjacency relation.
why it matters
CostConnected supplies the connectivity notion required to interpret the kernel and spectrum of the J-cost Laplacian quadratic form Q_J. It is invoked by the downstream reflexivity theorem costConnected_refl. Within the Recognition Science framework the definition supports the complexity-domain analysis that precedes the derivation of constants such as ħ = ϕ⁻⁵ and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.