Incorrect symbol `𝓢` used in documentation of

⚠️ 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/WicksTheorem.lean (around line 59) is incorrect.

Current text

1. `timeOrder_eq_maxTimeField_mul_finset` is used to write
  `𝓣(φ₀…φₙ)` as `𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` where `φᵢ` is
  the maximal time field in `φ₀…φₙ`

Why this is wrong

The documentation for the lemma timeOrder_eq_maxTimeField_mul_finset claims that 𝓣(φ₀…φₙ) is expressed using a term involving 𝓢(φᵢ, φ₀…φᵢ₋₁). This is incorrect because 𝓢 is not defined in the file and does not correspond to any standard notation in quantum field theory. In the context of time-ordered products, the correct symbol is 𝓣, which represents time-ordering.

The lemma's purpose is to decompose a time-ordered product into a term involving the maximal-time field and another time-ordered product. Using 𝓢 instead of 𝓣 introduces confusion and misrepresents the mathematical content. The correction replaces 𝓢 with 𝓣, aligning the documentation with both standard notation and the lemma's intended meaning.

The file uses 𝓣 consistently elsewhere for time-ordering, confirming that 𝓢 was a typographical error in this specific documentation. This change ensures clarity and correctness for users relying on the formalization.

Suggested correction

1. `timeOrder_eq_maxTimeField_mul_finset` is used to write
  `𝓣(φ₀…φₙ)` as `𝓣(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` where `φᵢ` is
  the maximal time field in `φ₀…φₙ`

Open Physlib/QFT/PerturbationTheory/WickAlgebra/WicksTheorem.lean around lines 59–61 and read the documentation for timeOrder_eq_maxTimeField_mul_finset. Verify the notation used elsewhere in the file, then replace the incorrect symbol in this sentence and confirm the documentation matches the lemma's intended time-ordering expression.