Stage: Cross-code mathematical verification inventory
Source language: Wolfram Language and Markdown
Manuals to read first: Markl dissertation DOI 10.3217/efp2p-0x485, complete table of contents and appendices; KIM/README.md; KiLCA/README; QL-Balance equations cited from the dissertation's quasilinear-transport chapter
Goal
Build the exhaustive formula index and convention ledger that every later derivation uses. Enumerate all displayed dissertation equations and every physics expression in KIM, KiLCA, QL-Balance, and shared input/preprocessing paths. No later issue may silently introduce a different sign, phase, velocity normalization, unit system, coordinate orientation, or Fourier measure.
Files to edit
verification/FORMULA_INDEX.md: NEW equation-to-code coverage table.
verification/mathematica/checklib.wl: NEW PASS/FAIL harness with nonzero exit on failure.
verification/mathematica/01_conventions_and_inventory.wl: NEW convention and identity checks.
Behavior to implement
Index thesis equation number/label, source page and chapter, assumptions, all consuming code symbols, and verification status. Also index formulas that exist only in Fortran. Lock CGS/Gaussian units; charge sign and species indexing; vT definition; gyrofrequency and Larmor-radius signs; Fourier transform pair and phase exp(+i(m theta+n phi)); every coordinate and field orientation; q and resonance convention; complex-amplitude/reality convention; time dependence; velocity-space measure; Bessel and plasma-dispersion definitions; collision-frequency normalization; and boundary/gauge conventions.
Scaffold
Needs["checklib`"];
phase[mm_, nn_] := Exp[I (mm theta + nn phi)];
check["Fourier conjugate reality", Simplify[mode[-mm,-nn] == Conjugate[mode[mm,nn]], assumptions]];
check["CGS gyrofrequency units", unitReduce[charge B/(mass c)] == inverseTime];
FinishChecks[];
Positive fixtures to add
- One indexed example from each code with a complete source-to-script-to-test chain.
- Automated counts for thesis displayed equations, indexed equations, Fortran formula sites, and classified sites.
Negative fixtures to add
- Duplicate symbol with incompatible definitions, missing code formula, missing thesis equation, or unclassified convention: the inventory script exits nonzero.
Makefile target
Add verify-mathematica-inventory or an equivalent repository target that runs the script and coverage check.
Success criteria
math -script verification/mathematica/01_conventions_and_inventory.wl
Every displayed thesis equation and physics-bearing code expression has an index row. Definitions and cited premises may be classified without rederivation, but their units, conventions, and applicability must be checked.
Non-goals
- Do not mark a formula verified merely because it is copied into the index.
- Do not include generic bookkeeping or I/O arithmetic without physical semantics.
Verification
math -script verification/mathematica/01_conventions_and_inventory.wl
Stage: Cross-code mathematical verification inventory
Source language: Wolfram Language and Markdown
Manuals to read first: Markl dissertation DOI
10.3217/efp2p-0x485, complete table of contents and appendices;KIM/README.md;KiLCA/README; QL-Balance equations cited from the dissertation's quasilinear-transport chapterGoal
Build the exhaustive formula index and convention ledger that every later derivation uses. Enumerate all displayed dissertation equations and every physics expression in KIM, KiLCA, QL-Balance, and shared input/preprocessing paths. No later issue may silently introduce a different sign, phase, velocity normalization, unit system, coordinate orientation, or Fourier measure.
Files to edit
verification/FORMULA_INDEX.md: NEW equation-to-code coverage table.verification/mathematica/checklib.wl: NEW PASS/FAIL harness with nonzero exit on failure.verification/mathematica/01_conventions_and_inventory.wl: NEW convention and identity checks.Behavior to implement
Index thesis equation number/label, source page and chapter, assumptions, all consuming code symbols, and verification status. Also index formulas that exist only in Fortran. Lock CGS/Gaussian units; charge sign and species indexing;
vTdefinition; gyrofrequency and Larmor-radius signs; Fourier transform pair and phaseexp(+i(m theta+n phi)); every coordinate and field orientation; q and resonance convention; complex-amplitude/reality convention; time dependence; velocity-space measure; Bessel and plasma-dispersion definitions; collision-frequency normalization; and boundary/gauge conventions.Scaffold
Positive fixtures to add
Negative fixtures to add
Makefile target
Add
verify-mathematica-inventoryor an equivalent repository target that runs the script and coverage check.Success criteria
Every displayed thesis equation and physics-bearing code expression has an index row. Definitions and cited premises may be classified without rederivation, but their units, conventions, and applicability must be checked.
Non-goals
Verification