RA-06: failure of the ordinary-sensitivity row-sampling guarantee
Recorded by the registry's curators from GitHub; the authors did not submit it here.
OpenAI Codex AI (Lean formalization and packaging)
A complete negative theorem for every real p>2, retaining the original independent Bernoulli sampling rule, expected-size budget, and simultaneous norm-power embedding assertion.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ 5487945, RA-06/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-ra-06-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 11 October 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:02:46.951798
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| RegistryProblems.Problem_OP_00239 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
| RegistryRecord.resolution | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
RegistryProblems.Problem_OP_00239
Prop
RegistryRecord.resolution
Not RegistryProblems.Problem_OP_00239
Build log
gy_le_complete' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2061/2073] Built NLA.Proofs.RA06.GraphCounting (4.0s) info: NLA/Proofs/RA06/GraphCounting.lean:172:0: 'NLA.Proofs.RA06.incident_card' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphCounting.lean:173:0: 'NLA.Proofs.RA06.edgePower_incident_eq' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphCounting.lean:174:0: 'NLA.Proofs.RA06.starEnergy_eq_sum_other' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphCounting.lean:175:0: 'NLA.Proofs.RA06.sum_differences_le_complete' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphCounting.lean:176:0: 'NLA.Proofs.RA06.completeEnergy_singleton_exact' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphCounting.lean:177:0: 'NLA.Proofs.RA06.weightedDegree_bounds_exact' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphCounting.lean:178:0: 'NLA.Proofs.RA06.positive_support_edge' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2062/2073] Built NLA.Proofs.RA06.GraphPower (3.6s) info: NLA/Proofs/RA06/GraphPower.lean:34:0: 'NLA.Proofs.RA06.abs_sub_rpow_le_two_legs' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2063/2073] Built NLA.Proofs.RA06.GraphSensitivity (8.4s) info: NLA/Proofs/RA06/GraphSensitivity.lean:56:0: 'NLA.Proofs.RA06.pairPower_le_complete' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2064/2073] Built NLA.Proofs.RA06.GraphSupport (8.5s) info: NLA/Proofs/RA06/GraphSupport.lean:106:0: 'NLA.Proofs.RA06.supportDegree_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphSupport.lean:107:0: 'NLA.Proofs.RA06.outside_card' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphSupport.lean:108:0: 'NLA.Proofs.RA06.supportDegree_pos' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphSupport.lean:109:0: 'NLA.Proofs.RA06.witness_at_center' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphSupport.lean:110:0: 'NLA.Proofs.RA06.witness_at_neighbor' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphSupport.lean:111:0: 'NLA.Proofs.RA06.witness_at_outside' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2065/2073] Built NLA.Proofs.RA06.GraphMatrix (4.8s) info: NLA/Proofs/RA06/GraphMatrix.lean:133:0: 'NLA.Proofs.RA06.graphMatrix_rowValue' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphMatrix.lean:134:0: 'NLA.Proofs.RA06.graphMatrix_fullColumnRank' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphMatrix.lean:135:0: 'NLA.Proofs.RA06.graphMatrix_inputEnergy' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphMatrix.lean:136:0: 'NLA.Proofs.RA06.graphMatrix_sensitivity_le' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphMatrix.lean:137:0: 'NLA.Proofs.RA06.graphMatrix_totalSensitivity_bound' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2066/2073] Built NLA.Proofs.RA06.GraphSampling (6.6s) info: NLA/Proofs/RA06/GraphSampling.lean:110:0: 'NLA.Proofs.RA06.sampleWeight_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphSampling.lean:111:0: 'NLA.Proofs.RA06.sampledEnergy_eq_weighted' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphSampling.lean:112:0: 'NLA.Proofs.RA06.embedding_to_weighted' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2067/2073] Built NLA.Proofs.RA06.GraphSupportCount (4.4s) info: NLA/Proofs/RA06/GraphSupportCount.lean:192:0: 'NLA.Proofs.RA06.graphMatrix_rows_pos' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphSupportCount.lean:193:0: 'NLA.Proofs.RA06.sampleWeight_positive_iff' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphSupportCount.lean:194:0: 'NLA.Proofs.RA06.sample_positiveEdgeCount_eq_retainedCount' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphSupportCount.lean:195:0: 'NLA.Proofs.RA06.sum_positiveIncidentCount_eq_two_edges' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphSupportCount.lean:196:0: 'NLA.Proofs.RA06.supportedNeighbor_iff_edgePositive' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphSupportCount.lean:197:0: 'NLA.Proofs.RA06.supportDegree_eq_positiveIncidentCount' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphSupportCount.lean:198:0: 'NLA.Proofs.RA06.sum_supportDegree_eq_two_edges' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphSupportCount.lean:199:0: 'NLA.Proofs.RA06.positiveEdgeCount_lower_of_all_degrees' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2068/2073] Built NLA.Proofs.RA06.GraphWitness (5.4s) info: NLA/Proofs/RA06/GraphWitness.lean:547:0: 'NLA.Proofs.RA06.edgeOfCross_injective' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphWitness.lean:548:0: 'NLA.Proofs.RA06.crossEnergy_le_complete' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphWitness.lean:549:0: 'NLA.Proofs.RA06.crossEnergy_constant' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphWitness.lean:550:0: 'NLA.Proofs.RA06.twoLevelCrossEnergy' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphWitness.lean:551:0: 'NLA.Proofs.RA06.witness_completeEnergy_lower_raw' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphWitness.lean:552:0: 'NLA.Proofs.RA06.inversePower_balance' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphWitness.lean:553:0: 'NLA.Proofs.RA06.witness_completeEnergy_lower' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphWitness.lean:554:0: 'NLA.Proofs.RA06.edgeWeight_le_neighborIncidence_of_mem' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphWitness.lean:555:0: 'NLA.Proofs.RA06.witness_edge_upper' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphWitness.lean:556:0: 'NLA.Proofs.RA06.witness_weightedEnergy_upper_degrees' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphWitness.lean:557:0: 'NLA.Proofs.RA06.witness_weightedEnergy_upper_raw' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphWitness.lean:558:0: 'NLA.Proofs.RA06.witness_weightedEnergy_upper' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphWitness.lean:559:0: 'NLA.Proofs.RA06.supportDegree_lower_of_approx' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2069/2073] Built NLA.Proofs.RA06.GraphFinite (4.0s) info: NLA/Proofs/RA06/GraphFinite.lean:71:0: 'NLA.Proofs.RA06.positiveEdgeCount_lower_of_approx' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphFinite.lean:72:0: 'NLA.Proofs.RA06.successful_retainedCount_lower' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/Proofs/RA06/GraphFinite.lean:73:0: 'NLA.Proofs.RA06.expectedSize_lower_from_graph_success' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [2070/2073] Built NLA.Proofs.RA06.Final (9.9s) info: NLA/Proofs/RA06/Final.lean:171:0: 'NLA.Proofs.RA06.target' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [2071/2073] Built Solution (3.7s) ✔ [2072/2073] Built RegistryRecord (3.6s) Build completed successfully (2073 jobs).