Module definition 

## Define block AST — a vernacular-logic predicate definition (Rung 0a).

A definition introduces a new predicate (the definiendum) as an abbreviation for a formula over its parameters (the definiens), written as a biconditional sentence:

## Define
x is a bachelor if and only if x is unmarried and x is a man.

The parser splits the biconditional: the LHS Predicate supplies the definiendum name and its parameter symbols; the RHS is the definiens. The proof layer registers this as a δ-unfoldable kernel definition, so the predicate becomes a reusable, citable node — not an inlined expansion.

Structs

DefinitionBlock

A ## Define block: <definiendum>(params) if and only if <definiens>.