paper-companion-style

name	paper-companion-style
description	Keep ComputationalPaths modules suitable as book/paper companion material with clear mathematical narrative, named constructions, and meaningful computational-path evidence.

Paper Companion Style

Use this skill when adding or deepening modules intended to accompany the ComputationalPaths paper or book-style exposition.

Module Shape

Each substantial module should have:

• a short module docstring explaining the mathematical object
• references or background when the topic is standard
• named structures for the main constructions
• named certificates or theorems for computational-path evidence
• minimal imports consistent with the topic

Evidence Style

Prefer statements that expose computational content:

structure PresentationCertificate where
  generators : Nat
  relations : Nat
  generator_count : Path generators expectedGenerators
  relation_count : Path relations expectedRelations
  coherence : RwEq (Path.trans generator_count (Path.refl expectedGenerators)) generator_count

Avoid book-companion anti-patterns:

• theorem statements that only prove reflexivity
• True fields with no surrounding mathematical data
• string witnesses instead of typed data
• opaque names like foo_theorem_1
• broad imports used only to make a file look substantial

Naming

• Types and structures: PascalCase
• Definitions: camelCase or established local convention
• Theorems and certificates: descriptive snake_case if the file already uses theorem-style naming
• Certificate records: FooCertificate, FooCoherence, or FooRewriteCertificate

Validation

For code changes, run the smallest meaningful build:

lake build ComputationalPaths.Path.Area.ModuleName

For documentation-only companion edits, run:

git diff --check