Spaces:
Running
Running
deploy(hf): sync szl-holdings/a11oy@main derived COPY set
Browse filesReusable Dockerfile-COPY-derived deploy from szl-holdings/a11oy main.
Files: 779 Pruned: 0
Derived from Dockerfile COPY sources (NO hand-maintained allowlist).
Signed-off-by: SZL Holdings <noreply@szlholdings.ai>
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
- data/genome.json +1 -1
data/genome.json
CHANGED
|
@@ -599,7 +599,7 @@
|
|
| 599 |
}
|
| 600 |
],
|
| 601 |
"tag": "honest-N/A",
|
| 602 |
-
"lean_ref": "Lutar/Puriq/Formulas/F23_Uniqueness.lean::f23_unconditional_is_underdetermined (L194, = Lutar.Round13.maxAgg_ne_Lambda — proves the UNCONDITIONAL claim FALSE); conditional theorems lutar_is_geomean_of_factors (L152) and lambda_unique_under_A6 (L181) are CLOSED but conditional; monotone_additive_linear (L101) has open sorry (L128). axiom A6_bisymmetric declared L172.",
|
| 603 |
"powers": "Would (if true) upgrade Λ from advisory to canonical — it does NOT, by doctrine",
|
| 604 |
"notes": "CONJECTURE 1. NEVER tag LOCKED-PROVEN (brief binding rule). The file is explicit: 'No conjecture is upgraded to a theorem here.' A6_bisymmetric is a declared optional non-core axiom, fully disclosed, never folded into the core kernel-clean set {propext, funext, Classical.choice, Quot.sound}.",
|
| 605 |
"_quadrant": "Q1"
|
|
|
|
| 599 |
}
|
| 600 |
],
|
| 601 |
"tag": "honest-N/A",
|
| 602 |
+
"lean_ref": "Lutar/Puriq/Formulas/F23_Uniqueness.lean::f23_unconditional_is_underdetermined (L194, = Lutar.Round13.maxAgg_ne_Lambda — proves the UNCONDITIONAL claim FALSE, so unconditional Λ uniqueness = Conjecture 1); conditional theorems lutar_is_geomean_of_factors (L152) and lambda_unique_under_A6 (L181) are CLOSED but conditional; monotone_additive_linear (L101) has open sorry (L128). axiom A6_bisymmetric declared L172.",
|
| 603 |
"powers": "Would (if true) upgrade Λ from advisory to canonical — it does NOT, by doctrine",
|
| 604 |
"notes": "CONJECTURE 1. NEVER tag LOCKED-PROVEN (brief binding rule). The file is explicit: 'No conjecture is upgraded to a theorem here.' A6_bisymmetric is a declared optional non-core axiom, fully disclosed, never folded into the core kernel-clean set {propext, funext, Classical.choice, Quot.sound}.",
|
| 605 |
"_quadrant": "Q1"
|