Incorrect type name in documentation for WickAlgebra grading

⚠️ Found by a local LLM, not a human. This was flagged by an automated documentation-mistake finder (qwen3:14b) and passed 10/10 independent verification runs before filing, but it has not been reviewed by a person. Please check it's a genuine error before acting on it.

Summary

The documentation in Physlib/QFT/PerturbationTheory/WickAlgebra/Grading.lean (around line 393) is incorrect.

Current text

For a field statistic `𝓕`, the algebra `𝓕.WickAlgebra` is graded by `FieldStatistic`.

Why this is wrong

The documentation comment claims that 𝓕 is a FieldStatistic, but the variable is actually a FieldSpecification. The file defines an instance WickAlgebraGrade : GradedAlgebra (A := 𝓕.WickAlgebra) statSubmodule where 𝓕 is bound as a FieldSpecification in the namespace FieldSpecification. This means the algebra 𝓕.WickAlgebra is graded by FieldStatistic, but the parameter 𝓕 itself is not a statistic – it's a specification containing field data. The correction replaces "field statistic" with "field specification" to match the actual type of 𝓕.

The error arises because FieldStatistic refers to an enum (bosonic/fermionic) used to classify fields, while FieldSpecification is a structure defining field properties. The grading mechanism uses FieldStatistic as the grading group, but the parameter 𝓕 must be a specification to contain the necessary data for computing statistics like 𝓕 |>ₛ φs. The fix aligns the documentation with the Lean code's type declarations and usage context.

The GradedAlgebra instance correctly grades 𝓕.WickAlgebra by FieldStatistic, but this depends on 𝓕 being a specification that can compute statistics. Referring to 𝓕 as a statistic in the documentation creates confusion between the grading group and the parameter's actual type.

Suggested correction

For a field specification `𝓕`, the algebra `𝓕.WickAlgebra` is graded by `FieldStatistic`.

Open Physlib/QFT/PerturbationTheory/WickAlgebra/Grading.lean around line 393 and read the surrounding FieldSpecification namespace and WickAlgebraGrade instance to confirm the parameter type. Update the comment to call 𝓕 a field specification while retaining FieldStatistic as the grading type, then check the documentation change against the declaration context.