ci: block merging PRs that increase technical debt unless reviewed

[kim-em]

This PR adds a merge gate for technical debt increases.

When the existing technical debt metrics script reports an increase, the build job adds an increases-technical-debt label. A check-technical-debt job then adds blocked-by-increases-technical-debt, which blocks bors.

A reviewer can add allow-increases-technical-debt to unblock after confirming the increase is acceptable.

Fail-closed detection

The detection greps for the safe patterns (Decrease in tech debt: / No changes to technical debt.) rather than for Increase. If mathlib-ci changes the script's output wording, the label is added (fail closed) rather than silently skipped (fail open).

Labels (three-label pattern, same as #38225)

Label	Managed by	Purpose
increases-technical-debt	build job (tech debt script)	Factual: this PR increases debt
blocked-by-increases-technical-debt	check-technical-debt job	Operational: blocks bors
allow-increases-technical-debt	Reviewer	Override: reviewer approves the increase

Bors's block_labels has no conditional logic, so we need the derived blocked-by-increases-technical-debt label to express the conjunction "increases-technical-debt AND NOT allow-increases-technical-debt".

False positives can be reported on the mathlib4 Zulip.

🤖 Prepared with Claude Code

[github-actions]

PR summary 98261a9c88

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

---

⚠️ Workflow documentation reminder

This PR modifies files under .github/workflows/.
Please update docs/workflows.md if the workflow inventory, triggers, or behavior changed.

Modified workflow files:

• .github/workflows/PR_summary.yml

[jcommelin]

I think this might need to be more fine-grained, with an allow- and/or deny-list.
Otherwise we risk that adding the allow- label becomes routine, whereas we want it to be for exceptional cases.

Eg, long files tech debt is currently working really well. So I would like to take it out of this feature.