Worked examples

Holant: an explicit tractable language

A Boolean unary signature with weights [1, 2] and binary equality has an explicit one-factor tensor decomposition. The tutorial proves the arity-two tractability branch, supplies valid exact descriptors, and obtains a fixed-language polynomial-time evaluator. The output follows the original exact root representation.

Excerpt; requires the definitions and namespace in the complete Lean file.

import Counting.Flagships.Holant
import Paper2.ExactInput.Coverage

-- In the complete tutorial, after family_tractable is proved:
theorem fixed_language_inFP (L : Language) (hL : L.family = family) :
    Paper2.Problem.InFP .ordinary L := by
  apply Counting.HolantUnified.FullDichotomy.ordinary_inFP L
  rw [hL]
  exact family_tractable

ComplexCSP: repeated occurrences and structural collapse

The language has Boolean domain and one constant binary signature of weight 2. Two repeated occurrences, repeated ports, and an isolated hidden variable give partition value 16. The tutorial proves joint Block Orthogonality for every generated table, applies structural collapse, and obtains fixed-language tractability with an explicit rational basis.

Excerpt; requires the definitions and namespace in the complete Lean file.

-- Excerpt from Counting.Tutorial.ComplexCSP:
theorem repeated_instance_partition :
    repeatedInstance.partition Fin.elim0 = (16 : ℂ) := by
  rw [partition_formula]
  norm_num [repeatedInstance, Fintype.card_fun]

PlanarHom: a positive rank-one interaction

The matrix [[1, 2], [2, 4]] has positive rank-one factors 1 and 2. The tutorial constructs its algebraic-real language, proves membership in the tractable structural class, and applies Theorem 1.1. The result is an exact fixed-language bit machine on promised ordinary planar multigraph inputs. Loops, parallel edges, and isolated vertices remain permitted.

Excerpt; requires the definitions and namespace in the complete Lean file.

-- Excerpt from Counting.Tutorial.PlanarHom:
theorem fixed_planar_evaluation_inFP : twoColour.problem.InFP := by
  apply (MainDichotomyScope.theorem11 twoColour (fun _ => rfl) ?_ ?_).1
    structural_membership
  · intro i j
    exact mul_comm _ _
  · intro i j
    exact mul_nonneg (amplitude_positive i).le (amplitude_positive j).le

Matchgate width: an exact representation obstruction

Choose the rational qutrit family member at k = 16 and the actual ordered-planar instance class. The tutorial proves its rank and deficient-port premises, then rules out every width-two exact replacement, even over a different nonempty finite domain. This is an exact representation result; it carries no generic evaluation-time claim.

Excerpt; requires the definitions and namespace in the complete Lean file.

-- Excerpt from Counting.Tutorial.MatchgateWidth:
theorem sample_minimum_exceeds_two :
    2 < integerSourceMinimum orderedPlanarInstances 16 := by
  exact (Counting.MatchgateWidth.flag_family_unbounded
    orderedPlanarInstances orderedPlanar_contains).2.2 2

Three introductory clients

Compile the complete clients

The displayed flagship code is an excerpt: its definitions, namespace, and supporting lemmas are in the linked complete file. Run the checker from the source checkout to compile and audit all seven files.

python3 scripts/check_examples.py --scope all --workers 2