feat: Implementing TODO 6VZME Step 1 (the work seems to be pretty large so it has been divided to be done in multiple PRs)

[NicolaBernini]

Scope

This PR implements the first of three alternative initial condition parametrizations mentioned in TODO 6VZME. We deliberately took an incremental approach to keep the PR focused and reviewable.

Rationale for scope reduction:

1. InitialConditionsAtTime is the simplest case with no degeneracy issues
2. Most commonly needed in practice (time-shifted problems)
3. Establishes the pattern for future implementations
4. Keeps PR small and focused (~150-200 lines vs ~500-800)

What's Included

Implemented: InitialConditionsAtTime - Initial conditions specified at arbitrary time t₀

• Structure definition with fields t₀, x_t₀, v_t₀
• Extensionality lemma
• toInitialConditions conversion function using backward time evolution
• Three correctness lemmas (see status below)
• Comprehensive documentation in section A.2

What's Deferred to Future PRs

The following alternative parametrizations mentioned in the original TODO are intentionally deferred:

• TwoPositionConditions: Specify positions at two different times (requires handling degeneracy when times differ by half-period multiples)
• TwoVelocityConditions: Specify velocities at two different times (similar degeneracy issues)
• Amplitude-phase parametrization: Alternative representation using A·cos(ωt + φ)

---

⚠️ Issues Requiring Review

Two correctness lemmas have proof obligations that automatic tactics are struggling to close:

1. toInitialConditions_trajectory_at_t₀ (lines 477-489)

Goal: Prove that trajectory passes through x_t₀ at time t₀

Mathematical correctness: The proof is valid. After expanding and using cos²+sin²=1, the goal reduces to showing that coefficients of x_t₀ and v_t₀ are 1 and 0 respectively.

Issue: After field_simp, linarith fails to close the polynomial equality. Tried tactics:

• linarith - fails
• nlinarith - fails
• ring - "ring expressions not equal" (likely due to EuclideanSpace operations)
• linear_combination - fails

2. toInitialConditions_velocity_at_t₀ (lines 494-506)

Goal: Prove that velocity equals v_t₀ at time t₀

Same issue: Identical proof structure, same failure mode with automatic tactics.

[jstoobysmith]

This and your more recent PRs look great. Though they are not building (i.e. one of the linters is failing), which we unfortunately need to fix before merging.

[jstoobysmith]

Bit confused by this header, but otherwise looks great! Is this meant to be here?

[NicolaBernini]

Yes, I agree it's confusing, I have just pushed a commit that should clarify hopefully

[jstoobysmith]

Great! Many thanks for fixing this. The linter isn't a problem with your PR (I'm not sure why this is a problem at all, but I'm going to fix it now). You don't have to do anything else here, once I've fixed the linter, I will merge.

[jstoobysmith]

Merged