chore: switch CI runners to self-hosted

[Jonathangadeaharder]

Switch all GitHub Actions workflows from GitHub-hosted runners (ubuntu-latest, macos-latest) to self-hosted runner to reduce GitHub runner minute consumption.

Summary by CodeRabbit

• Chores
  • Migrated GitHub Actions workflow runners from cloud-hosted to self-hosted infrastructure across build and deployment jobs
  • Added new foundational formalization file containing mathematical structures, core definitions, and theoretical framework scaffolding

[gemini-code-assist]

Warning

You have reached your daily quota limit. Please wait up to 24 hours and I will start processing your requests again!

[coderabbitai]

📝 Walkthrough

Walkthrough

This PR introduces infrastructure changes to GitHub Actions workflows by switching two build job runners from cloud-hosted to self-hosted runners, adds a Lake build trace configuration file, and introduces a comprehensive new Lean formalization file implementing a Level-Based Theorem approach for analyzing r-local games.

Changes

CI/CD Runner Migration

Layer / File(s)	Summary
Workflow Runner Configuration .github/workflows/blueprint.yml, .github/workflows/ci.yml	Build and deploy jobs switch from ubuntu-latest/macos-latest to self-hosted runners across blueprint and CI workflows.
Build Configuration Artifacts .lake/config/[anonymous]/lakefile.olean.trace	New Lake trace file captures build metadata including platform, hash values, and configuration state.

LBT Coupling Formalization

Layer / File(s)	Summary
Core Structures & Data Shapes LBTCoupling.lean.bak	Introduces RLocalGame structure with fields for game parameters (f, h, n, r, S, R_k, epsilon) and F_hat batch-mean estimator definition.
Foundation Theorems LBTCoupling.lean.bak	Implements r_local_alignment and r_local_offset_bound theorems providing algebraic decomposition and residual bounding over sparsity maps.
Level-Based Theorem Scaffolding LBTCoupling.lean.bak	Defines Population type alias, level conditions (A_ge, ConditionG1/G2/G3), population transition kernel, and truncated/expected generation measures.
Runtime Bound Instantiation LBTCoupling.lean.bak	Establishes bitstring mutation machinery (BitString, p_mut, mutation_prob), measure/kernel definitions (parent_mut_measure, coea_measure, coea_kernel), and selection lemmas (sel_monotone_level, sel_amplification_bound).
Final Theorems & Bounds LBTCoupling.lean.bak	Proves r_local_G1, r_local_G2, r_local_G3_holds condition instantiations and states the main r_local_runtime_bound theorem; many proofs remain as placeholders.

Estimated code review effort

🎯 3 (Moderate) | ⏱️ ~20 minutes

Possibly related PRs

• Jonathangadeaharder/lean-runtime-analysis#6: Both PRs modify GitHub Actions workflow runner configurations in CI/CD files to switch from cloud-hosted to self-hosted runners.

Poem

🐰 A theorem bundled up so tight,
With games and couplings shining bright!
From r-local bounds to bitstring spins,
The formalization journey begins. ✨

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The PR title 'chore: switch CI runners to self-hosted' accurately summarizes the main change across the workflow files, which involve switching runners from ubuntu-latest and macos-latest to self-hosted runners.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch hotfix/self-hosted-runner

Tip

💬 Introducing Slack Agent: The best way for teams to turn conversations into code.

Slack Agent is built on CodeRabbit's deep understanding of your code, so your team can collaborate across the entire SDLC without losing context.

• Generate code and open pull requests
• Plan features and break down work
• Investigate incidents and troubleshoot customer tickets together
• Automate recurring tasks and respond to alerts with triggers
• Summarize progress and report instantly

Built for teams:

• Shared memory across your entire org—no repeating context
• Per-thread sandboxes to safely plan and execute work
• Governance built-in—scoped access, auditability, and budget controls

One agent for your entire SDLC. Right inside Slack.

👉 Get started

---

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

[coderabbitai]

Actionable comments posted: 2

🤖 Prompt for all review comments with AI agents

Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.

Inline comments:
In @.github/workflows/blueprint.yml:
- Line 19: The "Install LaTeX" workflow step uses apt-get (Linux-only) but the
self-hosted runner is macOS, so update the workflow to run platform-aware
installation: change the "Install LaTeX" step to detect runner OS (using if:
matrix.os or if: runner.os == 'Linux' / runner.os == 'macOS') and run apt-get
only on Linux, and use brew install or a macOS-appropriate installer (or skip if
TeX is preinstalled) on macOS; alternatively replace the step with a
cross-platform action such as actions/setup-tex or add distinct self-hosted
labels (e.g., self-hosted, linux) in runs-on to ensure apt-get is only executed
on Linux runners.

In `@LBTCoupling.lean.bak`:
- Around line 1-6: The file LBTCoupling.lean.bak is a backup/temporary Lean
formalization accidentally committed; either remove it from the PR or rename it
to LBTCoupling.lean if it is intended to be part of the project, and ensure the
CI configuration (the sorry-check exclusion) and the three documented `sorry`
occurrences are accounted for when renaming; if this is a draft/backup, delete
LBTCoupling.lean.bak from the branch and open a separate PR for the
formalization instead.

🪄 Autofix (Beta)

Fix all unresolved CodeRabbit comments on this PR:

• Push a commit to this branch (recommended)
• Create a new PR with the fixes

---

ℹ️ Review info

⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: aeac7f74-3fe1-4893-91a0-ca22a7eded6a

📥 Commits

Reviewing files that changed from the base of the PR and between fa0eaa0 and 6abfd59.

⛔ Files ignored due to path filters (1)

• .lake/config/[anonymous]/lakefile.olean.lock is excluded by !**/*.lock

📒 Files selected for processing (5)

• .github/workflows/blueprint.yml
• .github/workflows/ci.yml
• .lake/config/[anonymous]/lakefile.olean
• .lake/config/[anonymous]/lakefile.olean.trace
• LBTCoupling.lean.bak

[Copilot]

Copilot encountered an error and was unable to review this pull request. You can try again by re-requesting a review.