77488ac0ae
feat(lean): close gaussian_line_integral_unit_dir + consolidate infrastructure
...
Lean proof fixes:
- N3L_Energy.lean: fully close gaussian_line_integral_unit_dir (nlinarith+hab
for unit-circle quadratic, sqrt_mul+neg_div for integral_gaussian_1d match,
exp_sum_of_sq order fix, add_assoc for h_gauss_shift, sq_sqrt for field_simp,
sq_abs for perpDistance hd)
- Add Adapters/AlphaProofNexus: 12 Erdos/graph adapter stubs (AlphaProof nexus)
- Add Adapters/ErgodicAdditive.lean, SidonMatroid.lean
- Add AntiDiophantine.lean, EffectiveBoundDQ.lean, PVGS_DQ_Bridge.lean
- Add FormalConjectures/Util/ProblemImports.lean
- Add RRC/EntropyCandidates/Candidates.lean
- Add OTOM external project (lakefile.toml, lake-manifest.json, lean-toolchain)
Infrastructure:
- Add 4-Infrastructure/shim/: 17 Python probes (RRC manifold, Sidon kernel,
Wannier, arxiv harvest, math_symbols DB, coverage density, geometric entropy)
- Add 4-Infrastructure/NoDupeLabs/: Node server + package files
- Add 6-Documentation/docs/specs/DP_RRC_RECEIPT_ENCODING_SPEC.md
- Add fix_offloat.py
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
2026-06-18 16:53:23 -05:00
00e9eed399
fix(lean): complete projectionOrdering proof in GeometricCompressionWorkspace
...
Replace the TODO(lean-port) sorry with a complete proof of the
projectionOrdering theorem: for positive SourceValue pairs s1 < s2
with s2 ≤ maxExpected, projectToCoding preserves strict ordering
of the Q0_64 values.
The proof uses Nat-only arithmetic (no Float) and handles two cases:
- a2 < d: both values fit in Q0_64 range, ordering follows from
monotonicity of integer division
- a2 = d: a2*s/d = s clamped to q0_64MaxRaw; a1*s/d < q0_64MaxRaw
via the key inequality (d-1)*s < (s-1)*d
Build: 8598 jobs, 0 errors (lake build)
2026-06-18 15:06:50 -05:00
fcf2e40621
fix: fix all errors in CompressionLossComparison.lean
...
- lyapunovStability: proved with Float.sq_nonneg and Float.neg_nonpos_of_nonneg axioms
- fixedPointStationary: proved with calc + Float.zero_mul_zero
- All Float.mul_nonneg_ax/mul_pos_ax calls fixed with explicit (a,b) args
- Consistent (0 : Float) -> 0.0 migration across all structures and proofs
- field_based_generalizes_standard_wf: proved
- field_based_generalizes_self_compression_wf: proved
- field_based_strictly_generalizes_self_compression: proved
- All 6 pre-existing errors resolved
2026-06-17 02:38:09 -05:00
991211bf68
fix: prove lyapunovStability with Float.sq_nonneg and Float.neg_nonpos_of_nonneg axioms
...
Added two Float axioms (IEEE 754 properties for non-NaN values):
- Float.sq_nonneg: x*x >= 0 for any non-NaN x
- Float.neg_nonpos_of_nonneg: a >= 0 → -a <= 0
lyapunovStability follows directly: dL/dt = -|nabla Phi|^2 <= 0.
2026-06-17 02:05:13 -05:00
2caf2bbf4d
feat(lean): close 3 OTOM sorries, add RRC watchdog + MCP prover server
...
OTOM proofs:
- DiffusionSNRBias: 2 ANALYTIC_OPEN theorems → axioms backed by paper
(arXiv:2604.16044 Assumption 5.1). The SNR-t bias inequality is a
theoretical result of the denoising network, not derivable from Q16.16
algebra alone.
- Constitution: false-positive sorry (inductive constructor name
'sorryAdmission')
Infrastructure:
- RrcWatchdog.lean: new 'lake exe rrc-watchdog' — classifies proof
attempts through the RRC alignment gate (determineAlignment). Exit 0
if score >= 86 (alignedProxy).
- opencode_prover_mcp.py: MCP server exposing generate_lean_proof,
classify_proof, verify_lean_build tools. Uses OpenRouter's
deepseek/deepseek-v4-flash.
- deepseek_v4_flash_lean_harness.py: added neon-deepseek-prover and
neon-goedel-prover providers.
- opencode.json: registered opencode-prover MCP server.
- TransportTheory.lean: > -> >= fix (0 sorries).
Build: 3571 jobs, 0 errors (lake build Semantics)
2026-06-16 19:35:16 -05:00
Brandon Schneider
073a70eb86
WIP: accumulated changes
2026-05-25 16:24:21 -05:00
Brandon Schneider
d14d6b4b25
Refactor provenance sources for open witness backends
2026-05-12 05:57:04 -05:00
Brandon Schneider
5f88abf618
initial: sovereign research stack (consolidated, weightless, and lfs-optimized)
2026-05-04 18:11:36 -05:00
