Lean good first issues

AI Summary: This issue proposes a strategy to process 251 specific routines that are loop-free but contain function calls. The approach involves composing existing contracts of called functions and then creating a prioritized worklist for parallel processing. Routines with un-contracted callees will contribute those missing contracts back to the work queue.

AI Summary: This issue proposes adding support for CIRCT's `verif.assume` and `verif.assert` operations to the Veir dialect. This involves creating a new `Verif` directory and defining the necessary operations and verifiers, initially focusing on cases where the property argument is an `i1`.

AI Summary: This issue proposes adding support for CIRCT's `seq` dialect within the Veir project. The initial goal is to implement parsing for the `seq.clock` type and the `seq.to_clock` and `seq.firreg` operations, enabling the representation of basic register circuits. Future enhancements include support for `seq.clock_inv` and `seq.shiftreg` operations.

AI Summary: This issue proposes adding support for the `hw.instance` operation in CIRCT, which is necessary for instantiating previously defined `hw.module` operations. The implementation will involve defining a new operation and verifier within Veir's HW dialect, with initial support focusing on core functionality and ignoring `inner_sym` and `doNoPrint` parameters.

AI Summary: This issue proposes to fix scoped notation for topological properties (like `IsOpen[T]`) so that they are correctly displayed in documentation generation. Currently, this notation is not rendered, making it difficult to understand the specific topology used in certain mathematical definitions within the documentation.

AI Summary: This issue proposes the creation of an API map for Lattice Quantum Field Theory (QFT). The goal is to document the primary results and functionalities that should be included in this API map.

AI Summary: This issue proposes creating a new top-level directory named 'LatticeQFT' within the repository. This directory will serve as a foundational stub, containing a 'Basic.lean' file that will later reference other directories related to Lattice Quantum Field Theory. The goal is to establish a central point for organizing and linking future Lattice QFT work.

AI Summary: This issue requires the creation of semantic specifications (spec triples) for seven RLP read routines in Lean. While string-to-program correspondence theorems exist, the actual computation of these routines is not yet defined. The encode side routines are considered higher value and can be addressed independently.

AI Summary: This issue requires a formal mathematical proof within a formal verification system (likely Lean) of the Glosten-Milgrom adverse-selection model. The proof should demonstrate how the bid-ask spread arises from informed traders and Bayesian updating, and confirm that the spread is positive under specific conditions. This involves implementing Bayesian probability and conditional expectations.

AI Summary: This issue reports an incorrect symbol `𝓢` used in the documentation of the `physlib` repository. The symbol appears to be a typo and should be `𝓣` (time-ordering) to accurately reflect the mathematical content of the lemma `timeOrder_eq_maxTimeField_mul_finset`. The suggested correction replaces the erroneous symbol with the correct one for clarity and consistency.

AI Summary: This issue reports a typo in the `physlib` documentation where a tensor product example incorrectly refers to an undefined variable `T1` instead of the declared tensor `T`. The suggested correction replaces `T1` with `T` to align the example with the surrounding text and maintain consistency with other documentation in the file.

AI Summary: The documentation in `Position.lean` incorrectly states that a section discusses generalized eigenvectors of the momentum operator. The actual content, specifically the lemma `positionStates_generalized_eigenvector_positionOperatorUnbounded`, demonstrates that these are generalized eigenvectors of the position operator. The suggested correction is to change the documentation header to accurately reflect this.

AI Summary: The documentation for a mapping function in the `physlib` repository incorrectly claims that anomaly cancellation is preserved. Upon investigation, there are no lemmas or proofs in the associated code that support this claim, while other documented properties like potential term presence and completeness are indeed supported. The suggested correction removes the erroneous claim about anomaly cancellation from the documentation.

AI Summary: The documentation for the `Renyi.lean` file incorrectly claims it covers α-Renyi entropy. Upon inspection, the file only contains definitions and theorems related to quantum relative entropy, with no mention or implementation of α-Renyi entropy. The suggested correction is to remove the false claim from the module docstring.

AI Summary: The documentation for `normPowerSeries` incorrectly identifies it as a power series. The issue points out that its definition `sqrt(‖x‖^2 + 1/(n+1))` is a sequence of functions, not a power series. The suggested correction replaces "power series" with "sequence of functions" to accurately reflect its mathematical nature.

AI Summary: The documentation for `realLorentzTensor` in `Basic.lean` incorrectly states it's for complex Lorentz tensors. The surrounding code and context clearly indicate it's for real Lorentz tensors, and the suggested correction updates the docstring to accurately reflect this.

AI Summary: The documentation for the Euler-Lagrange equations in the `physlib` repository incorrectly states that the variational derivative of the Lagrangian itself is equal to the `eulerLagrangeOp`. The actual theorem proves that the variational derivative of the action functional (the integral of the Lagrangian over time) yields the Euler-Lagrange operator. The suggested correction clarifies this by referring to the integral of the Lagrangian.

AI Summary: The documentation for the MSSM in the `physlib` repository incorrectly claims support for right-handed neutrinos (RHNs). The actual code implements anomaly cancellation conditions only for the standard MSSM without RHNs, lacking any definitions for RHN-specific species or charges. The suggested correction removes the mention of RHNs from the documentation to align it with the code's capabilities.

AI Summary: The documentation for Lorentz tensors in `Metrics/Basic.lean` incorrectly labels them as 'complex' when they are actually real-valued, as indicated by the `ℝT` type. The suggested correction is to change 'complex' to 'real' in the documentation to accurately reflect the tensor's type and mathematical context.

AI Summary: This issue reports a documentation error in the `physlib` repository regarding the Levi-Civita tensor. The current documentation incorrectly states that `ε4` represents a rank-four Levi-Civita tensor in 3-dimensional space. The actual tensor is rank-three and exists in 4-dimensional space, as indicated by the code's use of `Fin 4` indices.

AI Summary: The documentation for WickAlgebra grading in `Grading.lean` incorrectly states that the parameter `𝓕` is a `FieldStatistic`. In reality, `𝓕` is a `FieldSpecification`, which is a structure containing field data. The documentation should be updated to reflect this distinction to avoid confusion between the grading group (`FieldStatistic`) and the parameter's type.

AI Summary: The documentation for the Galilean action on space in `physlib/Physlib/SpaceAndTime/GalileanGroup/Basic.lean` incorrectly states it acts on space at a fixed time. The function `actSpace` actually depends on a `Time` parameter `t`, as shown in its implementation and the module's definition of Galilean transformations. The suggested correction clarifies that the action depends on the given time `t`.

AI Summary: The documentation for `ZModCharges` in `ZMod.lean` incorrectly initializes the set `S`. The current initialization creates a set with a single element instead of the intended set of all possible charge spectra. The suggested correction uses `Finset.univ.filter` to correctly generate the desired set.

AI Summary: This issue proposes formalizing key-rate (partial) duration in a financial modeling library. It involves defining the sensitivity of a bond's price to changes in specific spot rates and proving that the sum of these key-rate durations equals the effective duration under a parallel yield curve shift. This extends existing single-factor duration calculations to a multi-factor framework.

AI Summary: This issue requires formalizing the Arbitrage Pricing Theory (APT) in a Lean mathematical proof assistant. Specifically, it asks to derive the exact-factor APT pricing relation E[Rᵢ]−r = Σₖ βᵢₖ λₖ from the no-arbitrage hypothesis, given a linear factor model for asset returns. The derivation should involve a finite-dimensional annihilator argument and generalize the existing CAPM formalization.

AI Summary: This issue proposes formalizing the life-contingent annuity present value, denoted as ä_x:n, in the Lean mathematical library. The goal is to define this survival-weighted sum and prove its basic properties, such as nonnegativity and its reduction to the certain annuity when survival is guaranteed.

AI Summary: This issue aims to formally prove that an American put option is strictly more valuable than a European put option when interest rates are positive. This is achieved by demonstrating a scenario within a binomial tree model where immediate exercise of the American put yields a higher payoff than holding it for one more step and then exercising.

AI Summary: This issue presents Green's Open Problem #82, which asks for the number of real numbers $\theta$ (modulo 1) for which the sum of cosines of elements in a given finite set of integers $A$ equals zero. The problem is related to number theory and analysis, with AMS categories 11 and 42.

AI Summary: This issue reports a typo in the documentation of the `physlib` repository. The word 'FiedOpAlgebra' was used instead of the correct term 'FieldOpAlgebra' in a section heading. The suggested correction is to replace the misspelled term with the correct one to ensure documentation accuracy and consistency.