feat(NumberTheory): add ordered Markov-tree descent

[qazW12345]

One ordinary extension submission: Submissions/markov-tree-descent.json plus one new subject module, LeanFrontier/NumberTheory/MarkovTree.lean.

Subject

This extends the accepted Markov-equation Vieta-jumping submission with the local descent step that its source explicitly left for separate Markov-tree work.

For a positive ordered Markov triple x ≤ y ≤ z, excluding (1, 1, 1), the existing Vieta jump in the largest coordinate satisfies

• 0 < jump x y z,
• jump x y z ≤ y, and therefore
• jump x y z < z.

The proof imports and uses the accepted MarkovEquation API, in particular jump_pos and mul_jump_eq; it does not add the two coordinate-permuted jump variants.

Entrypoint

LeanFrontier.MarkovTree.jump_descends_ordered_positive

Edge-case / boundary review

The exceptional root is necessary: at (1,1,1) the jump is 2, so descent fails. The non-strict middle bound is also necessary: (1,1,2) is a valid ordered solution and its jump is 1 = y. The proof separately shows that an ordered positive solution with y = z must be the root, so every non-root candidate has y < z before the descent comparison is used.

Provenance

The producing agent surveyed several extension directions, recommended Markov-tree descent, and the human operator selected that recommendation from the agent's shortlist. The human did not author or materially edit the formal Lean statement or proof, so both origins remain machine; the selection process is recorded in source_context.

Receiver evidence

Validated against current main 9f708c18fccb311646b10af124c60ca70e41857b, with candidate head ca6a1c3b092e56a24292d424c4ba389df72c63c6.

Fork CI on that exact head:

• test: success (run 34775490375)
• validate-submission: success (run 34775490324)
• trusted preflight: accepted, no diagnostics
• restricted formal validation: accepted, no diagnostics
• build: pass
• kernel recheck: pass
• downstream import smoke: pass
• Mathlib exact matches: 0

The receiver observed only the two ordinary submission files as changed.