Further coordinated frame cuts on #186: conditional κ = 6.62651985348746e-4

.github/workflows/continued-frame-cuts-186.yml

@@ -0,0 +1,27 @@
+name: Verify continued frame cuts on PR186
+on:
+  push:
+    paths:
+      - 'research/continued-frame-cuts-186/**'
+      - 'research/coordinated-frames-and-entrance-banks/**'
+      - '.github/workflows/continued-frame-cuts-186.yml'
+  pull_request:
+    paths:
+      - 'research/continued-frame-cuts-186/**'
+      - 'research/coordinated-frames-and-entrance-banks/**'
+      - '.github/workflows/continued-frame-cuts-186.yml'
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  verify:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
+        with:
+          python-version: '3.13'
+      - run: python3 -B research/continued-frame-cuts-186/verify.py

research/balanced-nullity-banks-163/AUDIT-TARGETS.json

@@ -0,0 +1,54 @@
+[
+  "Mathproof.BeyondNLogN.TakeoverBit.partialSwap_apply",
+  "Mathproof.BeyondNLogN.TakeoverBit.partialSwap_zero",
+  "Mathproof.BeyondNLogN.TakeoverBit.partialSwap_comp_disjoint",
+  "Mathproof.BeyondNLogN.TakeoverBit.partialSwap_involutive",
+  "Mathproof.BeyondNLogN.TakeoverBit.partialSwap_id",
+  "Mathproof.BeyondNLogN.TakeoverBit.partialSwap_commute",
+  "Mathproof.BeyondNLogN.TakeoverBit.bankSwap_eq_sum",
+  "Mathproof.BeyondNLogN.TakeoverBit.bankSwap_full",
+  "Mathproof.BeyondNLogN.TakeoverBit.weighted_apply",
+  "Mathproof.BeyondNLogN.TakeoverBit.weighted_comp",
+  "Mathproof.BeyondNLogN.TakeoverBit.weighted_id",
+  "Mathproof.BeyondNLogN.TakeoverBit.weightedBank_eq",
+  "Mathproof.BeyondNLogN.TakeoverBit.weightedBank_full",
+  "Mathproof.BeyondNLogN.TakeoverBit.coordinateProjector_apply",
+  "Mathproof.BeyondNLogN.TakeoverBit.coordinateProjector_idempotent",
+  "Mathproof.BeyondNLogN.TakeoverBit.coordinateProjector_disjoint",
+  "Mathproof.BeyondNLogN.TakeoverBit.coordinateProjector_sum",
+  "Mathproof.BeyondNLogN.TakeoverBit.coordinateBank_full",
+  "Mathproof.BeyondNLogN.TakeoverBit.bankAddress_bijective",
+  "Mathproof.BeyondNLogN.TakeoverBit.bankAddress_roles_injective",
+  "Mathproof.BeyondNLogN.TakeoverBit.P12.selected_block_capacity",
+  "Mathproof.BeyondNLogN.TakeoverBit.P12.undeferred_block_capacity",
+  "Mathproof.BeyondNLogN.TakeoverBit.P12.selected_bank_full",
+  "Mathproof.BeyondNLogN.TakeoverBit.P12.undeferred_bank_full",
+  "Mathproof.BeyondNLogN.TakeoverBit.P12.inherited_rank_mass",
+  "Mathproof.BeyondNLogN.TakeoverBit.P12.removed_exterior_count",
+  "Mathproof.BeyondNLogN.TakeoverBit.P12.packed_rank_mass",
+  "Mathproof.BeyondNLogN.TakeoverBit.P12.packed_max_rank",
+  "Mathproof.BeyondNLogN.TakeoverBit.P12.normalized_volume",
+  "Mathproof.BeyondNLogN.TakeoverBit.P12.packed_deficit",
+  "Mathproof.BeyondNLogN.TakeoverBit.P12.actual_role_counts",
+  "Mathproof.BeyondNLogN.TakeoverBit.P12.selected_weighted_bank_full",
+  "Mathproof.BeyondNLogN.TakeoverBit.P12.undeferred_weighted_bank_full",
+  "Mathproof.BeyondNLogN.TakeoverBit.Contents.run_eq_address",
+  "Mathproof.BeyondNLogN.TakeoverBit.Contents.run_full",
+  "Mathproof.BeyondNLogN.TakeoverBit.Contents.p12_selected_contents",
+  "Mathproof.BeyondNLogN.TakeoverBit.Contents.p12_undeferred_contents",
+  "Mathproof.BeyondNLogN.TakeoverBit.PR161P12.inherited_rank_mass",
+  "Mathproof.BeyondNLogN.TakeoverBit.PR161P12.removed_exterior_count",
+  "Mathproof.BeyondNLogN.TakeoverBit.PR161P12.packed_rank_mass",
+  "Mathproof.BeyondNLogN.TakeoverBit.PR161P12.packed_max_rank",
+  "Mathproof.BeyondNLogN.TakeoverBit.PR161P12.normalized_volume",
+  "Mathproof.BeyondNLogN.TakeoverBit.PR161P12.packed_deficit",
+  "Mathproof.BeyondNLogN.TakeoverBit.PR161P12.actual_role_counts",
+  "Mathproof.BeyondNLogN.TakeoverBit.PR161P12.actual_bank_and_inventory_certificate",
+  "Mathproof.BeyondNLogN.TakeoverLiteralGuard20261008.literal_charge_lt",
+  "Mathproof.BeyondNLogN.TakeoverLiteralGuard20261008.finite_row_reserve",
+  "Mathproof.BeyondNLogN.TakeoverLiteralGuard20261008.row_reserve_value",
+  "Mathproof.BeyondNLogN.TakeoverBalanced16320261009.core_slacks_positive",
+  "Mathproof.BeyondNLogN.TakeoverBalanced16320261009.all_47_slacks_positive",
+  "Mathproof.BeyondNLogN.TakeoverBalanced16320261009.strengthened_public_margin",
+  "Mathproof.BeyondNLogN.TakeoverBalanced16320261009.all_47_concrete_guards"
+]