V21: Add formalization variable explanation lint check

[ImChong]

Summary

Adds automated validation to ensure that formula variables in wiki/formalizations/ pages have corresponding physical meaning explanations in the document body. This is part of the V21 execution phase for improving semantic consistency in formalization documentation.

Key Changes

• New lint rule formalization_unexplained_vars in scripts/lint_wiki.py:

  • Extracts single uppercase Latin letters from display formulas ($$...$$) in formalization pages
  • Excludes function call patterns (e.g., R(s,a,s')) using negative lookahead (?![A-Za-z_(])
  • Validates each variable against 7 heuristic patterns for physical meaning explanations:
    • List items with colons (e.g., - $X$: meaning)
    • Inline colon definitions (e.g., $X$: meaning)
    • Table rows containing the variable
    • Verb-based explanations (是/为/表示/代表/denote/etc.)
    • "其中"/"where" clauses
    • Mathematical definitions (=, \in, \succeq, \succ, \equiv, \triangleq)
    • Bold paragraph context

• Documentation fixes in 6 formalization pages to satisfy the new rule:

  • bellman-equation.md: Clarified $R$ as immediate reward scalar
  • control-lyapunov-function.md: Added $A, B$ matrix definitions
  • ekf.md: Comprehensive matrix explanations ($A, B, C, Q, R, P, K, I$)
  • hjb.md: Added variable definitions for LQR special case
  • lqr.md: Explained $x, u, A, B$ in linear system model
  • tsid-formulation.md: Defined $S$ as actuation selection matrix

• Updated V21 checklist to mark the "自动化背链一致性 Lint" item as complete

Implementation Details

The variable extraction uses regex (?<![A-Za-z\\_^{])([A-Z])(?![A-Za-z_(]) to identify candidate variables while avoiding:

• Multi-letter identifiers
• Subscripts/superscripts
• Function calls like R(s,a,s')

Pattern matching is case-insensitive and multiline-aware to handle various documentation styles. Variables are reported with their containing file path for easy remediation.

https://claude.ai/code/session_01EuF6h7rZ7irF6ACREZ8iXs