An eight-port ordinary signal ring

Eight binary implications follow the perimeter of [20,220]², forcing all eight variables to agree. Every variable has two internal literal occurrences, leaving one external occurrence for its paired access. Unused accesses introduce no freedom. The sixteen incidence routes are straight and have total Manhattan length 800.

Main definitions

• Variable, cyclicOrder, formula: the fixed implication ring.
• variablePosition, clausePositions, incidenceRoutes: its explicit drawing.

Main results

• eval_formula_iff, eval_constant: all ports carry one freely chosen bit.
• internal_occurrences: exactly two internal literal occurrences per port.

References

This fixed template is original and reuses CNF.implicationCycle.

@[reducible, inline]

abbrev Cslib.Complexity.SAT.OrdinaryRing.Variable : Type

One variable for each side and lane of the common paired-port interface.

def Cslib.Complexity.SAT.OrdinaryRing.cyclicOrder : List Variable

Cyclic geometric order, traversing the inner square clockwise.

def Cslib.Complexity.SAT.OrdinaryRing.formula : Logic.PL.CNF Variable

The eight directed implications closing the signal ring.

def Cslib.Complexity.SAT.OrdinaryRing.variablePosition (v : Variable) : Orthogonal.Point

The eight common inner access positions.

def Cslib.Complexity.SAT.OrdinaryRing.clausePositions : List Orthogonal.Point

Clause positions in precisely the order of the eight implications.

def Cslib.Complexity.SAT.OrdinaryRing.clausePosition (i : ℕ) : Orthogonal.Point

Indexed clause position, with an irrelevant out-of-range default.

def Cslib.Complexity.SAT.OrdinaryRing.incidenceRoutes : List (ℕ × Variable × Orthogonal.Route)

The sixteen clause-to-variable incidences, in clause and literal order.

def Cslib.Complexity.SAT.OrdinaryRing.commonEndpoints (e f : ℕ × Variable × Orthogonal.Route) : List Orthogonal.Point

Common graph endpoints are the only permitted contacts between distinct incidences.

theorem Cslib.Complexity.SAT.OrdinaryRing.mem_cyclicOrder (v : Variable) : v ∈ cyclicOrder

All eight port variables occur in the cycle.

theorem Cslib.Complexity.SAT.OrdinaryRing.eval_formula_iff (σ : Variable → Bool) : Logic.PL.CNF.eval σ formula = true ↔ ∀ (v : Variable), σ v = σ (0, 0)

The ring holds exactly when every port carries the value of the first port.

theorem Cslib.Complexity.SAT.OrdinaryRing.eval_constant (b : Bool) : Logic.PL.CNF.eval (fun (x : Variable) => b) formula = true

Either constant assignment satisfies the ring.

theorem Cslib.Complexity.SAT.OrdinaryRing.internal_occurrences (v : Variable) : List.count v formula.vars = 2

Every port has exactly two internal literal occurrences.

theorem Cslib.Complexity.SAT.OrdinaryRing.formula_sizes : List.length formula = 8 ∧ ∀ c ∈ formula, List.length c = 2

The formula has eight clauses, each of width two.

theorem Cslib.Complexity.SAT.OrdinaryRing.variables_used (v : Variable) : v ∈ formula.vars

Every variable is actually used, including variables with no external access in a client.

theorem Cslib.Complexity.SAT.OrdinaryRing.incidenceRoutes_cover : List.map (fun (e : ℕ × Variable × Orthogonal.Route) => (e.1, e.2.1)) incidenceRoutes = List.flatMap (fun (ci : Logic.PL.Clause Variable × ℕ) => List.map (fun (l : Logic.PL.Literal Variable) => (ci.2, l.1)) ci.1) (List.zipIdx formula)

All literal incidences occur exactly once, in formula order.

theorem Cslib.Complexity.SAT.OrdinaryRing.drawing_sizes : clausePositions.length = 8 ∧ incidenceRoutes.length = 16

There are eight clause positions and sixteen incidence routes.

theorem Cslib.Complexity.SAT.OrdinaryRing.variablePosition_injective : Function.Injective variablePosition

Inner positions identify the eight variables.

theorem Cslib.Complexity.SAT.OrdinaryRing.clausePositions_nodup : clausePositions.Nodup

Clause positions are distinct.

theorem Cslib.Complexity.SAT.OrdinaryRing.variablePosition_not_mem_clauses (v : Variable) : variablePosition v ∉ clausePositions

Variables and clauses have different positions.

theorem Cslib.Complexity.SAT.OrdinaryRing.incidenceEndpoints_nodup : (List.map (fun (e : ℕ × Variable × Orthogonal.Route) => (e.1, e.2.1)) incidenceRoutes).Nodup

The sixteen labeled incidences are distinct.

theorem Cslib.Complexity.SAT.OrdinaryRing.incidence_endpoints (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → e.1 < 8 ∧ List.head? e.2.2 = some (clausePosition e.1) ∧ List.getLast? e.2.2 = some (variablePosition e.2.1)

Every incidence has its prescribed clause and variable endpoints.

theorem Cslib.Complexity.SAT.OrdinaryRing.incidence_pair (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → e.2.2 = [clausePosition e.1, variablePosition e.2.1]

All sixteen incidence routes are straight segments.

theorem Cslib.Complexity.SAT.OrdinaryRing.incidence_orthogonal (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → Orthogonal.IsOrthogonal e.2.2

Every incidence is properly orthogonal.

theorem Cslib.Complexity.SAT.OrdinaryRing.incidence_points_nodup (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → List.Nodup e.2.2

Listed incidence vertices are distinct within each route.

theorem Cslib.Complexity.SAT.OrdinaryRing.incidence_isSimple {e : ℕ × Variable × Orthogonal.Route} (he : e ∈ incidenceRoutes) : Orthogonal.IsSimple e.2.2

Every incidence is continuously simple.

theorem Cslib.Complexity.SAT.OrdinaryRing.core_bounds (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → ∀ p ∈ e.2.2, 20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220

All listed core points lie in [20,220]².

theorem Cslib.Complexity.SAT.OrdinaryRing.variable_bounds (v : Variable) : 20 ≤ (variablePosition v).1 ∧ (variablePosition v).1 ≤ 220 ∧ 20 ≤ (variablePosition v).2 ∧ (variablePosition v).2 ≤ 220

Every variable lies in the inner core square.

theorem Cslib.Complexity.SAT.OrdinaryRing.clause_bounds (p : Orthogonal.Point) : p ∈ clausePositions → 20 ≤ p.1 ∧ p.1 ≤ 220 ∧ 20 ≤ p.2 ∧ p.2 ≤ 220

Every clause lies in the inner core square.

theorem Cslib.Complexity.SAT.OrdinaryRing.core_support_interior {e : ℕ × Variable × Orthogonal.Route} (he : e ∈ incidenceRoutes) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support e.2.2) : 0 < p.1 ∧ p.1 < 240 ∧ 0 < p.2 ∧ p.2 < 240

The full continuous core support lies strictly inside the outer cell.

theorem Cslib.Complexity.SAT.OrdinaryRing.routes_contact_check (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → ∀ f ∈ incidenceRoutes, e ≠ f → Orthogonal.routeContactCheck (commonEndpoints e f) e.2.2 f.2.2 = true

Finite certificate of all permitted contacts between distinct incidences.

theorem Cslib.Complexity.SAT.OrdinaryRing.routes_contact {e f : ℕ × Variable × Orthogonal.Route} (he : e ∈ incidenceRoutes) (hf : f ∈ incidenceRoutes) (hne : e ≠ f) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support e.2.2) (hq : p ∈ Orthogonal.support f.2.2) : ∃ q ∈ commonEndpoints e f, p = Orthogonal.realPoint q

Continuous contacts between distinct incidences are shared graph endpoints.

theorem Cslib.Complexity.SAT.OrdinaryRing.variable_avoidance_check (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → ∀ (v : Variable), v ≠ e.2.1 → Orthogonal.routeContactCheck [] e.2.2 [variablePosition v] = true

Finite certificate excluding nonincident variable vertices.

theorem Cslib.Complexity.SAT.OrdinaryRing.clause_avoidance_check (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → ∀ (i : Fin 8), ↑i ≠ e.1 → Orthogonal.routeContactCheck [] e.2.2 [clausePosition ↑i] = true

Finite certificate excluding nonincident clause vertices.

theorem Cslib.Complexity.SAT.OrdinaryRing.variable_not_mem_support {e : ℕ × Variable × Orthogonal.Route} (he : e ∈ incidenceRoutes) {v : Variable} (hv : v ≠ e.2.1) : Orthogonal.realPoint (variablePosition v) ∉ Orthogonal.support e.2.2

Incidences avoid every nonincident variable over their full real support.

theorem Cslib.Complexity.SAT.OrdinaryRing.clause_not_mem_support {e : ℕ × Variable × Orthogonal.Route} (he : e ∈ incidenceRoutes) {i : Fin 8} (hi : ↑i ≠ e.1) : Orthogonal.realPoint (clausePosition ↑i) ∉ Orthogonal.support e.2.2

Incidences avoid every nonincident clause over their full real support.

theorem Cslib.Complexity.SAT.OrdinaryRing.access_contact_check (s : Fin 4) (l : Fin 2) (e : ℕ × Variable × Orthogonal.Route) : e ∈ incidenceRoutes → Orthogonal.routeContactCheck (if e.2.1 = (s, l) then [variablePosition (s, l)] else []) (Orthogonal.PairedPorts.accessRoute s l) e.2.2 = true

Finite certificate that access touches the core only at its own variable.

theorem Cslib.Complexity.SAT.OrdinaryRing.access_contact {s : Fin 4} {l : Fin 2} {e : ℕ × Variable × Orthogonal.Route} (he : e ∈ incidenceRoutes) {p : ℝ × ℝ} (hp : p ∈ Orthogonal.support (Orthogonal.PairedPorts.accessRoute s l)) (hq : p ∈ Orthogonal.support e.2.2) : e.2.1 = (s, l) ∧ p = Orthogonal.realPoint (variablePosition (s, l))

Every access/core contact is its designated variable endpoint.

theorem Cslib.Complexity.SAT.OrdinaryRing.access_variable_avoidance_check (s : Fin 4) (l : Fin 2) (v : Variable) : v ≠ (s, l) → Orthogonal.routeContactCheck [] (Orthogonal.PairedPorts.accessRoute s l) [variablePosition v] = true

Finite certificate excluding every other variable from an access.

theorem Cslib.Complexity.SAT.OrdinaryRing.access_clause_avoidance_check (s : Fin 4) (l : Fin 2) (p : Orthogonal.Point) : p ∈ clausePositions → Orthogonal.routeContactCheck [] (Orthogonal.PairedPorts.accessRoute s l) [p] = true

Finite certificate excluding every clause from every access.

theorem Cslib.Complexity.SAT.OrdinaryRing.access_variable_not_mem {s : Fin 4} {l : Fin 2} {v : Variable} (hv : v ≠ (s, l)) : Orthogonal.realPoint (variablePosition v) ∉ Orthogonal.support (Orthogonal.PairedPorts.accessRoute s l)

Access avoids every other variable over its full real support.

theorem Cslib.Complexity.SAT.OrdinaryRing.access_clause_not_mem {s : Fin 4} {l : Fin 2} {p : Orthogonal.Point} (hp : p ∈ clausePositions) : Orthogonal.realPoint p ∉ Orthogonal.support (Orthogonal.PairedPorts.accessRoute s l)

Access avoids every clause over its full real support.

theorem Cslib.Complexity.SAT.OrdinaryRing.route_sizes : (List.map (fun (e : ℕ × Variable × Orthogonal.Route) => (List.consecutivePairs e.2.2).length) incidenceRoutes).sum = 16 ∧ (List.map (fun (e : ℕ × Variable × Orthogonal.Route) => Orthogonal.wireLength e.2.2) incidenceRoutes).sum = 800

The sixteen incidence segments have total Manhattan length 800.