allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Add Builder-Judge-Warden Erdos-Szekeres example

Browse source
This commit is contained in:
Allaun Silverfox 2026-05-16 17:06:26 -05:00
parent d0999cf1d3
commit a49292418f
1 changed files with 62 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

62
shared-data/examples/famm_bjw_geodesic_cleanup_erdos_szekeres.example.json Normal file
View file

@ -0,0 +1,62 @@
{
"source_description": "Erdos-Szekeres monotone subsequence theorem cleanup",
"source_object": {
"problem": "Prove any sequence of distinct real numbers of length (r-1)(s-1)+1 has an increasing subsequence of length r or decreasing subsequence of length s.",
"raw_route": "search all subsequences"
},
"weights": {
"complexity": 1.0,
"residual": 1.2,
"scar": 1.5,
"invariant": 2.0,
"proof_burden": 0.8
},
"warden_threshold": 0.25,
"candidate_moves": [
{
"id": "builder_label_map",
"builder": {
"operation": "replace_subsequence_search_with_label_grid",
"proposal": "Map each term a_i to (I_i,D_i), longest increasing/decreasing subsequence ending at i.",
"delta_complexity": -0.86,
"delta_residual": -1.0
},
"judge": {
"invariant_preserved": true,
"receipt_pass": true,
"tests": [
"distinct input sequence",
"label injectivity",
"avoidance box capacity"
]
},
"warden": {
"penalty": 0.0,
"blocks": []
}
},
{
"id": "bad_infinite_generalization",
"builder": {
"operation": "generalize_to_infinite_sequences_without_boundary",
"proposal": "Claim same finite pigeonhole result for arbitrary infinite sequences.",
"delta_complexity": -0.2,
"delta_residual": 0.5
},
"judge": {
"invariant_preserved": false,
"receipt_pass": false,
"tests": [
"finite theorem boundary violated"
]
},
"warden": {
"penalty": 1.0,
"blocks": [
"overclaim",
"missing_boundary"
]
}
}
]
}