2 commits

Author	SHA1	Message	Date
allaun	b65ef756ca	fix(StrandCapacityBound): repair proofs + register in lakefile ... Registering required it to actually compile (it did not). Fixes: - capacity_bound_grid was FALSE at L₁=0 or L₂=0 (empty grid, nonempty image) and its `norm_num : 0 < (L₁:ℤ)` could not prove positivity of a variable. Added `0 < L₁, 0 < L₂` hypotheses; threaded through capacity_bound and chiral_capacity_bound. - mathlib name drift: emod_nonneg/emod_lt → Int.emod_nonneg (b ≠ 0) / Int.emod_lt_of_pos; Finset.card_Ico → Int.card_Ico; Finset.card_le_card_of_subset → Finset.card_le_card; Finset.image_subset → Finset.image_subset_iff.mpr. - replaced a `#eval` (broke on ℤ's noncomputable order instance) and its WRONG expected value (claimed 4 over {1..6}, actually 6) with two kernel-checked `decide` witnesses: {1,2,5,6}→4 (the Sidon set) and Ico 1 7→6. - registered CoreFormalism.StrandCapacityBound in lakefile. Verified: lake build OK (links into SilverSightFormal), #print axioms = {propext, Classical.choice, Quot.sound} (no sorryAx, no custom axiom), anti-smuggle --ci clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>	2026-07-03 15:19:47 -05:00
allaun	3362d554d1	feat(braid/dag): land untracked research WIP + register 4 formal libs; ignore build artifacts ... - lakefile.lean: register SilverSight.{AngrySphinx,CollatzBraid,GoldenSpiral,GCCL} - docs/research/: braid group action, iteration DAG/regime, Sidon preservation/creation, unified CRT-torus DAG notes - docs/diagrams/: DAG + heatmap + 8-strand search JSON/dot outputs - formal/CoreFormalism/StrandCapacityBound.lean: capacity bound (passes hardened anti-smuggle --ci) - scripts/, python/: braid word solver, collapse/DAG search + tuning, heatmap gen, YB search/verification, wrapping verifier - .gitignore: exclude rust/**/target and coq compiled artifacts (*.vo/*.vok/*.vos/*.glob/*.aux) that were polluting the tree Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>	2026-07-03 15:11:37 -05:00