Add certified maximin allocation bounds

.gitattributes

@@ -0,0 +1 @@
+results/certified-maximin-design/paired-recovery/heuristic_allocation_source.csv -text -diff

docs/certified_maximin_paired_recovery.md

@@ -0,0 +1,20 @@
+# Paired heuristic-versus-certified recovery diagnostic
+
+The exact integer certificate maximizes the declared finite-grid worst ordered-pair
+residual. It does not follow that the certified allocation must outperform the earlier
+heuristic allocation in a finite held-out recovery simulation.
+
+`bayesian-ach-design-paired-recovery` therefore compares the chronologically locked
+heuristic N=60 allocation with the exact certified N=60 allocation. The comparison uses
+the same five seeds (`7, 11, 19, 23, 31`), 200 replicates per generating candidate and
+seed, a 0.35 held-out fraction, unit effect and noise scales, and an identically reset RNG
+stream for both allocations. Both source allocations are checksum-bound; the heuristic
+constructor and integer certificate are independently reverified before simulation.
+
+`bayesian-ach-design-paired-recovery-verify` rechecks every output checksum, both source
+allocations, certificate geometry, all 60 recovery rows, five seed summaries, and every
+headline allocation/recovery diagnostic by rerunning the deterministic simulation.
+
+This is a diagnostic sensitivity analysis. It does not replace the chronologically locked
+paper allocation, select a post-result schedule, establish empirical superiority, guarantee
+recovery power, or specify a physical trial, time-bin, or animal protocol.

docs/certified_maximin_paired_recovery_result.md

@@ -0,0 +1,22 @@
+# Frozen paired N=60 recovery result
+
+The checksum-bound paired diagnostic was produced from clean commit
+`c6dea54d1e8a1b702c212c83535af8a5de3ab3ea`. It compares the chronologically locked
+heuristic allocation (SHA-256 `a823be49faf6c6cbebf60b11d4b5ca895cf7734d6e9c577ee98f97a5907b69b2`)
+with the exact certified allocation (SHA-256
+`694a84107c1ba94f39146a05675def1b5813621fab486d7567f6711510a6fc08`).
+
+The schedules are materially different: allocation L1 distance 100, support 15 versus 12,
+support overlap 4, and maximum absolute cell change 9. With identical random streams for
+five seeds and 200 replicates per generating candidate, the minimum recovery rate changed
+from 0.750 for the heuristic schedule to 0.665 for the certified schedule. The certified
+schedule's minimum was lower for every seed.
+
+This result is a negative sensitivity boundary. The certificate remains an exact statement
+about the declared asymptotic worst-residual objective; it is not evidence that the certified
+schedule is superior under finite recovery. The diagnostic does not replace the locked
+heuristic schedule, select a post-result design, guarantee power, or define a physical
+trial, time-bin, or animal protocol.
+
+The frozen evidence is in `results/certified-maximin-design/paired-recovery/`. Its verifier
+recomputes both inputs, every recovery row, all headline diagnostics, and every checksum.

docs/optimal_design.md

@@ -202,6 +202,73 @@ closed-loop timing can be incorporated by replacing the candidate matrix with
 the corresponding forward-model predictions while retaining the same auditable
 finite-allocation structure.
 
+## Certified continuous and integer follow-up
+
+The original `maximin_optimized` allocation is a deterministic greedy
+construction with at most three one-for-one exchanges. Its trace is auditable,
+but it is not a certificate of global optimality.
+
+`certify_maximin_design` supplies a separate global certificate. For each
+ordered pair,
+
+```math
+R_{k\mid l}(w)
+=
+\inf_{b,c}\sum_d w_d[x_k(d)-b-cx_l(d)]^2.
+```
+
+For any fixed `(b,c)`, the loss is linear in the allocation. The certificate
+iteratively solves a HiGHS LP or MILP master problem, evaluates exact weighted
+least squares for all ordered pairs, and adds every violated loss cut. The
+finite master gives an upper bound; the directly evaluated allocation gives a
+feasible lower bound. Results report both bounds and stop as certified only
+when their declared tolerance is met.
+
+The integer mode certifies the stated budget and per-cell count cap. The
+continuous mode certifies the capped-simplex relaxation and therefore also
+provides an upper bound for every integer allocation. Neither mode constructs a
+sequential behavioral history. The 240 cells are independently instantiated
+belief conditions; reset, washout, carry-over, and physical ordering constraints
+must be encoded before calling any count vector an executable protocol.
+
+```bash
+bayesian-ach-design-certify \
+  --output results/certified-design-n60 \
+  --code-sha <exact-commit> \
+  --budget 60 \
+  --mode integer \
+  --require-certificate
+```
+
+Certificate artifacts are versioned separately from the previously frozen
+greedy/exchange evidence. A changed certified allocation must trigger new
+recovery evidence; it must never silently replace the earlier artifact.
+
+Objective certification and planning-index certification are reported
+separately. If rigorous residual bounds are `[R_L,R_U]`, monotonicity of the
+profiled Gaussian gap gives
+
+```math
+\left\lceil\frac{B}{G(R_U)}\right\rceil
+\le N_{\mathrm{eff}} \le
+\left\lceil\frac{B}{G(R_L)}\right\rceil.
+```
+
+The rounded `N_eff` index is certified when these endpoints agree, even if a
+continuous objective run has not met a much tighter numerical residual-gap
+tolerance. This does not relabel that continuous objective as certified. The
+claim-bearing finite schedules use exact integer certificates.
+
+Frozen integer packages can be independently checked against their SHA-256
+table, allocation budget and cap, canonical 240-cell geometry, objective gap,
+cut trace, and `N_eff` rounding:
+
+```bash
+bayesian-ach-design-certificate-verify \
+  results/certified-maximin-design/n60 \
+  results/certified-maximin-design/n45
+```
+
 ## Use
 
 ```bash

pyproject.toml

@@ -70,6 +70,10 @@ plot = ["matplotlib>=3.8"]
 [project.scripts]
 bayesian-ach = "bayesian_ach.cli_ext:main"
 bayesian-ach-design = "bayesian_ach.design_cli:main"
+bayesian-ach-design-certificate-verify = "bayesian_ach.design_certificate_verify:main"
+bayesian-ach-design-certify = "bayesian_ach.design_certificate_cli:main"
+bayesian-ach-design-paired-recovery = "bayesian_ach.design_paired_recovery:main"
+bayesian-ach-design-paired-recovery-verify = "bayesian_ach.design_paired_recovery_verify:main"
 bayesian-ach-replay = "bayesian_ach.replay_cli:main"
 
 [tool.setuptools.packages.find]

results/certified-maximin-design/n45/SHA256SUMS.csv

@@ -0,0 +1,4 @@
+file,bytes,sha256
+certificate_summary.json,1970,b527c4373533650c9259e92846ad7680e7cff7d7b7cb169885aeba3663dae2f7
+certified_allocation.csv,2382,bbd0796cc7c767c3388cd6c3b9522cebaed78993586aa5dfd3b353e856abe856
+cut_trace.csv,1702,4d365c5f8635fbc17c2d39390326ceeace7ddc1db4a2eb9ca3529252859289ba

results/certified-maximin-design/n45/certificate_summary.json

@@ -0,0 +1,50 @@
+{
+  "absolute_gap": 2.7755575615628914e-16,
+  "candidate_names": [
+    "innovation_l2",
+    "surprise",
+    "gain",
+    "update_l2",
+    "information_gain",
+    "change_probability"
+  ],
+  "certified": true,
+  "certified_improvement_over_heuristic": 0.0025656042479573204,
+  "code_repository": "IPS-Stuttgart/Bayesian-ACh",
+  "code_sha": "e82f48d335fb3f17f843d16bf2442693b6c83eef",
+  "config": {
+    "absolute_gap_tolerance": 1e-08,
+    "budget": 45,
+    "cut_violation_tolerance": 1e-09,
+    "integer": true,
+    "master_mip_relative_gap": 1e-09,
+    "master_time_limit_s": 120.0,
+    "max_iterations": 100,
+    "max_point_fraction": 0.15,
+    "relative_gap_tolerance": 1e-07
+  },
+  "cut_count": 53,
+  "direct_geometry_matches_lower_bound": true,
+  "experiment": "certified_finite_grid_maximin_allocation",
+  "grid_point_count": 240,
+  "heuristic_lower_bound": 0.24983023368504692,
+  "iterations": 7,
+  "last_master_message": "Optimization terminated successfully. (HiGHS Status 7: Optimal)",
+  "last_master_status": 0,
+  "lower_bound": 0.25239583793300424,
+  "population_n_eff": {
+    "effect_size": 1.0,
+    "index_certified": true,
+    "interpretation": "Population observation-equivalent index under effectively independent Gaussian observations; not a physical trial, time-bin, session, or animal count.",
+    "lower_index_from_residual_upper_bound": 45,
+    "noise_std": 1.0,
+    "target_log_score_gap": 5.0,
+    "upper_index_from_residual_lower_bound": 45
+  },
+  "relative_gap": 2.7755575615628914e-16,
+  "schema_version": 1,
+  "scipy_version": "1.15.3",
+  "scope": "This certificate is conditional on the independently instantiated finite grid, global candidate standardization, budget, and per-cell cap. The allocation is a count target, not a validated sequential protocol; no history constructor, washout, reset, or carry-over feasibility is implied.",
+  "solver": "scipy.optimize.milp (HiGHS) with OLS cutting planes",
+  "upper_bound": 0.2523958379330045
+}

results/certified-maximin-design/n45/certified_allocation.csv

@@ -0,0 +1,16 @@
+point_id,observed_probability,residual_shape,concentration,reset_observed_probability,hazard,innovation_l2,surprise,gain,update_l2,information_gain,change_probability,allocation
+5,0.05,0.5,2.0,0.95,0.15,1.1635076278220096,2.995732273553991,0.3333333333333333,0.3878358759406699,1.6491929980444475,0.7702702702702702,1
+10,0.05,0.5,8.0,0.95,0.01,1.1635076278220096,2.995732273553991,0.1111111111111111,0.1292786253135566,0.793706251013266,0.16101694915254236,4
+13,0.05,0.5,32.0,0.05,0.15,1.1635076278220096,2.995732273553991,0.030303030303030304,0.03525780690369727,0.2655001957924723,0.15,1
+16,0.05,0.5,32.0,0.95,0.01,1.1635076278220096,2.995732273553991,0.030303030303030304,0.03525780690369727,0.2655001957924723,0.16101694915254236,4
+120,0.35,0.9,2.0,0.05,0.01,0.8768979416100827,1.0498221244986778,0.3333333333333333,0.29229931387002756,0.3355856642737046,0.0014409221902017292,1
+123,0.35,0.9,2.0,0.5,0.15,0.8768979416100827,1.0498221244986778,0.3333333333333333,0.29229931387002756,0.3355856642737046,0.20134228187919462,3
+125,0.35,0.9,2.0,0.95,0.15,0.8768979416100827,1.0498221244986778,0.3333333333333333,0.29229931387002756,0.3355856642737046,0.32386363636363635,2
+128,0.35,0.9,8.0,0.5,0.01,0.8768979416100827,1.0498221244986778,0.1111111111111111,0.09743310462334258,0.10687049253534275,0.014224751066856332,1
+129,0.35,0.9,8.0,0.5,0.15,0.8768979416100827,1.0498221244986778,0.1111111111111111,0.09743310462334258,0.10687049253534275,0.20134228187919462,7
+130,0.35,0.9,8.0,0.95,0.01,0.8768979416100827,1.0498221244986778,0.1111111111111111,0.09743310462334258,0.10687049253534275,0.026685393258426966,5
+143,0.35,0.9,128.0,0.95,0.15,0.8768979416100827,1.0498221244986778,0.007751937984496124,0.0067976584620936574,0.007218032071614644,0.32386363636363635,2
+197,0.9,0.5,2.0,0.95,0.15,0.12247448713915887,0.10536051565782628,0.3333333333333333,0.0408248290463862,0.023123169408776692,0.15702479338842976,7
+201,0.9,0.5,8.0,0.5,0.15,0.12247448713915887,0.10536051565782628,0.1111111111111111,0.013608276348795313,0.006640070861282682,0.08928571428571429,4
+207,0.9,0.5,32.0,0.5,0.15,0.12247448713915887,0.10536051565782628,0.030303030303030304,0.0037113480951260457,0.0017170260888290656,0.08928571428571429,2
+211,0.9,0.5,128.0,0.05,0.15,0.12247448713915887,0.10536051565782628,0.007751937984496124,0.000949414628985708,0.00043283472005928303,0.00970873786407767,1

results/certified-maximin-design/n45/cut_trace.csv

@@ -0,0 +1,8 @@
+iteration,status,message,cut_count,master_incumbent,master_upper_bound,global_upper_bound,candidate_lower_bound,best_lower_bound,absolute_gap,relative_gap,violated_pair_count,new_cut_count
+1,0,Optimization terminated successfully. (HiGHS Status 7: Optimal),40,0.29969132172795643,0.29969132172795643,0.29969132172795643,0.018338177433384985,0.24983023368504692,0.04986108804290951,0.04986108804290951,10,10
+2,0,Optimization terminated successfully. (HiGHS Status 7: Optimal),43,0.2736078369096001,0.2736078369096001,0.2736078369096001,0.20997088490389842,0.24983023368504692,0.02377760322455319,0.02377760322455319,3,3
+3,0,Optimization terminated successfully. (HiGHS Status 7: Optimal),46,0.2601656411587341,0.2601656411587341,0.2601656411587341,0.2472594709475595,0.24983023368504692,0.010335407473687164,0.010335407473687164,3,3
+4,0,Optimization terminated successfully. (HiGHS Status 7: Optimal),50,0.25432101764237947,0.25432101764237947,0.25432101764237947,0.16308942112856467,0.24983023368504692,0.004490783957332545,0.004490783957332545,4,4
+5,0,Optimization terminated successfully. (HiGHS Status 7: Optimal),51,0.2523958379330045,0.2523958379330045,0.2523958379330045,0.2216371103803767,0.24983023368504692,0.002565604247957598,0.002565604247957598,1,1
+6,0,Optimization terminated successfully. (HiGHS Status 7: Optimal),53,0.2523958379330047,0.2523958379330047,0.2523958379330045,0.23336287252923216,0.24983023368504692,0.002565604247957598,0.002565604247957598,2,2
+7,0,Optimization terminated successfully. (HiGHS Status 7: Optimal),53,0.2523958379330047,0.2523958379330047,0.2523958379330045,0.25239583793300424,0.25239583793300424,2.7755575615628914e-16,2.7755575615628914e-16,0,0

results/certified-maximin-design/n60/SHA256SUMS.csv

@@ -0,0 +1,4 @@
+file,bytes,sha256
+certificate_summary.json,1968,7c89b45552568665fd22103feaa301d9d69030bc1a5101b20c3ce6d438b3743c
+certified_allocation.csv,1925,694a84107c1ba94f39146a05675def1b5813621fab486d7567f6711510a6fc08
+cut_trace.csv,1264,34d2b9598f96960ca483bfc4054f5fc975c4aecbdf0fade0a02d28f734ac759f

results/certified-maximin-design/n60/certificate_summary.json

@@ -0,0 +1,50 @@
+{
+  "absolute_gap": 5.551115123125783e-17,
+  "candidate_names": [
+    "innovation_l2",
+    "surprise",
+    "gain",
+    "update_l2",
+    "information_gain",
+    "change_probability"
+  ],
+  "certified": true,
+  "certified_improvement_over_heuristic": 0.0028311171816116643,
+  "code_repository": "IPS-Stuttgart/Bayesian-ACh",
+  "code_sha": "e82f48d335fb3f17f843d16bf2442693b6c83eef",
+  "config": {
+    "absolute_gap_tolerance": 1e-08,
+    "budget": 60,
+    "cut_violation_tolerance": 1e-09,
+    "integer": true,
+    "master_mip_relative_gap": 1e-09,
+    "master_time_limit_s": 120.0,
+    "max_iterations": 100,
+    "max_point_fraction": 0.15,
+    "relative_gap_tolerance": 1e-07
+  },
+  "cut_count": 52,
+  "direct_geometry_matches_lower_bound": true,
+  "experiment": "certified_finite_grid_maximin_allocation",
+  "grid_point_count": 240,
+  "heuristic_lower_bound": 0.25003654826964467,
+  "iterations": 5,
+  "last_master_message": "Optimization terminated successfully. (HiGHS Status 7: Optimal)",
+  "last_master_status": 0,
+  "lower_bound": 0.25286766545125633,
+  "population_n_eff": {
+    "effect_size": 1.0,
+    "index_certified": true,
+    "interpretation": "Population observation-equivalent index under effectively independent Gaussian observations; not a physical trial, time-bin, session, or animal count.",
+    "lower_index_from_residual_upper_bound": 45,
+    "noise_std": 1.0,
+    "target_log_score_gap": 5.0,
+    "upper_index_from_residual_lower_bound": 45
+  },
+  "relative_gap": 5.551115123125783e-17,
+  "schema_version": 1,
+  "scipy_version": "1.15.3",
+  "scope": "This certificate is conditional on the independently instantiated finite grid, global candidate standardization, budget, and per-cell cap. The allocation is a count target, not a validated sequential protocol; no history constructor, washout, reset, or carry-over feasibility is implied.",
+  "solver": "scipy.optimize.milp (HiGHS) with OLS cutting planes",
+  "upper_bound": 0.2528676654512564
+}

results/certified-maximin-design/n60/certified_allocation.csv

@@ -0,0 +1,13 @@
+point_id,observed_probability,residual_shape,concentration,reset_observed_probability,hazard,innovation_l2,surprise,gain,update_l2,information_gain,change_probability,allocation
+0,0.05,0.5,2.0,0.05,0.01,1.1635076278220096,2.995732273553991,0.3333333333333333,0.3878358759406699,1.6491929980444475,0.01,1
+3,0.05,0.5,2.0,0.5,0.15,1.1635076278220096,2.995732273553991,0.3333333333333333,0.3878358759406699,1.6491929980444475,0.6382978723404256,1
+7,0.05,0.5,8.0,0.05,0.15,1.1635076278220096,2.995732273553991,0.1111111111111111,0.1292786253135566,0.793706251013266,0.15,2
+11,0.05,0.5,8.0,0.95,0.15,1.1635076278220096,2.995732273553991,0.1111111111111111,0.1292786253135566,0.793706251013266,0.7702702702702702,6
+16,0.05,0.5,32.0,0.95,0.01,1.1635076278220096,2.995732273553991,0.030303030303030304,0.03525780690369727,0.2655001957924723,0.16101694915254236,3
+121,0.35,0.9,2.0,0.05,0.15,0.8768979416100827,1.0498221244986778,0.3333333333333333,0.29229931387002756,0.3355856642737046,0.02459016393442623,5
+134,0.35,0.9,32.0,0.5,0.01,0.8768979416100827,1.0498221244986778,0.030303030303030304,0.02657266489727523,0.02843542878084193,0.014224751066856332,6
+139,0.35,0.9,128.0,0.05,0.15,0.8768979416100827,1.0498221244986778,0.007751937984496124,0.0067976584620936574,0.007218032071614644,0.02459016393442623,9
+140,0.35,0.9,128.0,0.5,0.01,0.8768979416100827,1.0498221244986778,0.007751937984496124,0.0067976584620936574,0.007218032071614644,0.014224751066856332,9
+197,0.9,0.5,2.0,0.95,0.15,0.12247448713915887,0.10536051565782628,0.3333333333333333,0.0408248290463862,0.023123169408776692,0.15702479338842976,4
+205,0.9,0.5,32.0,0.05,0.15,0.12247448713915887,0.10536051565782628,0.030303030303030304,0.0037113480951260457,0.0017170260888290656,0.00970873786407767,5
+210,0.9,0.5,128.0,0.05,0.01,0.12247448713915887,0.10536051565782628,0.007751937984496124,0.000949414628985708,0.00043283472005928303,0.0005608524957936063,9

results/certified-maximin-design/n60/cut_trace.csv

@@ -0,0 +1,6 @@
+iteration,status,message,cut_count,master_incumbent,master_upper_bound,global_upper_bound,candidate_lower_bound,best_lower_bound,absolute_gap,relative_gap,violated_pair_count,new_cut_count
+1,0,Optimization terminated successfully. (HiGHS Status 7: Optimal),36,0.3003019448952873,0.3003019448952873,0.3003019448952873,1.8899792520920073e-32,0.25003654826964467,0.05026539662564261,0.05026539662564261,6,6
+2,0,Optimization terminated successfully. (HiGHS Status 7: Optimal),40,0.2746209089988777,0.2746209089988777,0.2746209089988777,0.1998940141548362,0.25003654826964467,0.024584360729233035,0.024584360729233035,4,4
+3,0,Optimization terminated successfully. (HiGHS Status 7: Optimal),43,0.2625384062229467,0.2625384062229467,0.2625384062229467,0.1845235932375922,0.25003654826964467,0.012501857953302054,0.012501857953302054,3,3
+4,0,Optimization terminated successfully. (HiGHS Status 7: Optimal),45,0.2556738948533919,0.2556738948533919,0.2556738948533919,0.25286766545125633,0.25286766545125633,0.002806229402135596,0.002806229402135596,2,2
+5,0,Optimization terminated successfully. (HiGHS Status 7: Optimal),52,0.2528676654512564,0.2528676654512564,0.2528676654512564,0.166514444222626,0.25286766545125633,5.551115123125783e-17,5.551115123125783e-17,7,7

results/certified-maximin-design/paired-recovery/SHA256SUMS.csv

@@ -0,0 +1,6 @@
+file,bytes,sha256
+heuristic_allocation_source.csv,14450,a823be49faf6c6cbebf60b11d4b5ca895cf7734d6e9c577ee98f97a5907b69b2
+paired_recovery.csv,5515,c04675c240b34a110be3c6a2376775ced4381396026240e96a756bf4e1c94c3c
+seed_summary.csv,644,0893d3da81d6d26cd94121dfefc6b19c406edf068184019e1d51a363adff44c8
+summary.json,2309,2abde4359fcf9e6ada150931e9dbb6b74e70cd06ea989998dfe25e42ee7191ed
+artifact_manifest.json,1954,b20585a4e29c1a0776a0b327f25bd38c493800f54fbcc0f81b64a5a5feaa4296