[qazW12345]

Theorem

For every Boolean path into the Stern–Brocot tree, the sum of the regular continued-fraction coefficients of its represented positive rational is exactly the number of path edges plus one:

theorem regularCoefficients_sum_eq_length_succ (path : List Bool) :
    (regularCoefficients path).sum = path.length + 1

This quantifies the classical correspondence between the depth of a Stern–Brocot rational and the total size of the quotients in its Euclidean/continued-fraction expansion. The empty-root convention and the leading zero for fractions less than one are handled uniformly.

Mathematical integration

The proof substantively consumes accepted LeanFrontier infrastructure:

• pathQuotients_eq_runLengthEncode: the terminal Euclidean quotient is the final maximal run length plus one;
• expandRuns_runLengthEncode: the encoded runs expand exactly to the original path;
• regularCoefficients_runs: the correct regular continued-fraction coefficients, including the initial-zero convention;
• a local list-sum lemma for incrementing the last list element.

There is only one public theorem entrypoint. Three small technical lemmas are private; the submission adds no redundant alternative path encoding and does not depend on other unmerged pull requests.

Files and provenance

Exactly two new files; no modifications to accepted or trusted files:

• LeanFrontier/NumberTheory/SternBrocot/ContinuedFractionDepth.lean
• Submissions/stern-brocot-continued-fraction-depth.json

The user asked GPT-6 to autonomously find and formalize another target; all formal Lean statements and proofs were independently produced by GPT-6. The pinned Mathlib version is v4.35.0.

Trusted validation

The exact source and claim blobs passed the fork's full receiver on the previous upstream head:

• Success: fork trusted receiver
• accepted: true, diagnostics: []
• Lean build and kernel replay passed, Python passed, no disallowed axioms.

Because upstream's automation advanced main again while the receiver was running, this branch has been reparented onto the latest main commit without changing either submission file. Please use this upstream PR's checks for independent acceptance against the new base.