leanprover-community/physlib

We should add an API-map for Lattice QFT including the main results that we would want to include there.

⚠️ 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/Relativity/Tensors/Elab.lean (around line 31) is incorrect. Current text Suppose `T2` is a tensor with color `![c3]`. Then `{T | μ ν ⊗ T2 | σ}ᵀ` is `prodNode (tensorNode T1) (tensorNode T2)`. Why this is wrong The documentation example claims that {T | μ ν ⊗ T2 | σ}ᵀ elaborates to prodNode (tensorNode T1) (tensorNode T2). This is incorrect because the preceding sentence introduces T, not T1, as the tensor with color ![c3]. The use of T1 refers to an undefined variable, while T is explicitly mentioned in the context. The correction replaces T1 with T, aligning the example with the declared tensor name. This matches the structure of other examples in the file, whi

⚠️ 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 pr

⚠️ 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/Particles/SuperSymmetry/SU5/ChargeSpectrum/Map.lean (around line 21) is incorrect. Current text There are various properties which are preserved under this mapping: - Anomaly cancellation. - The presence of a specific term in the potential. - Being complete. Why this is wrong The documentation in physlib/Physlib/Particles/SuperSymmetry/SU5/ChargeSpectrum/Map.lean incorrectly states that "anomaly cancellation" is preserved under the map function, but no lemma in the file supports this assertion. The module defines properties like map_allowsTerm and map_isComplete_iff, which correspond to the documented preservation of potential terms and completeness, respectively. However, ther

⚠️ 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/Relativity/Tensors/RealTensor/Basic.lean (around line 67) is incorrect. Current text /-- The tensor structure for complex Lorentz tensors. -/ Why this is wrong The docstring for realLorentzTensor incorrectly claims it defines "complex Lorentz tensors", but the declaration's name and surrounding context clearly indicate it is for real tensors. The file's comments explicitly mention "Real Lorentz tensors" and the definition uses Lorentz.ContrMod/Lorentz.CoMod, which are real vector spaces. This discrepancy arises because the docstring was not updated when the definition was renamed from a complex variant to a real one. The correction aligns the documentation with the actual purpo