normalForm
plain-language theorem explainer
The normalForm definition reduces a word by bounded iteration of rewriteOnce until length stabilizes or the initial length in passes is exhausted. Mass-spectrum modelers in Recognition Science cite it to obtain canonical ribbon forms before length or primitivity checks. The implementation is a direct recursive descent that halts on fixed length or pass exhaustion.
Claim. For a word $w$, define its normal form by starting with $w$ and iteratively replacing the current word by its single rewrite until either the length no longer decreases or the number of iterations reaches the initial length of $w$.
background
In the Masses.Ribbons module, treated as a narrative scaffold for φ-ladder ribbon machinery, Word is the type of finite lists of Ribbon syllables. The normalForm operation relies on the sibling rewriteOnce to perform local reductions. Upstream results supply the convex J-cost structure (J(x) = (x + 1/x)/2 − 1) from PhysicsComplexityStructure and the discrete tiering of nuclear densities from NucleosynthesisTiers, both of which motivate length reduction as a proxy for energy minimization.
proof idea
The definition introduces an auxiliary recursive normalize that applies rewriteOnce and decrements a pass counter. Termination occurs on either zero remaining passes or when the rewritten word has unchanged length; the top-level call supplies the initial word and its length as the pass bound.
why it matters
normalForm supplies the reduced representative required by ell (reduced length) and by the Primitive structure in SectorPrimitive, where a word must already equal its normal form. It implements the length-reduction step on the φ-ladder that feeds the mass formula yardstick · φ^(rung − 8 + gap(Z)). As a model file the definition leaves open the full formalization of Recognition Science mass derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.