|
|
1794299a6c
|
chore(quality): native_decide migration, docs, and phi pipeline cleanup
Systematic native_decide → dec_trivial/rfl migration across all Lean modules
to comply with AGENTS.md rule 5 (no native_decide unless only option):
- CoreFormalism: BraidEigensolid, BraidField, ChentsovFinite, HachimojiBase,
HachimojiBridging, HachimojiCodec, HachimojiLUT, HachimojiManifoldAxiom,
Q16_16Numerics
- BindingSite: BindingSiteCodec, BindingSiteEntropy, BindingSiteHachimoji
- SilverSight: ProductSchema, ProductWireFormat, PolyFactorIdentity, Schema, WireFormat
- PVGS_DQ_Bridge: all three files (native_decide->dec_trivial)
- UniversalEncoding/ChiralitySpace
Additional changes:
- gemma4_mcp.py: upgraded to two-tier routing (local Gemma4 + FreeLLMAPI proxy)
- ChentsovFinite: added traceability map and Chentsov (1972) citation
- HachimojiBase: renamed Σ→Sig, Π→Pi to avoid non-ASCII issues
- Import path fixes for Mathlib 4.30.0-rc2 compatibility
- Doc updates: PURE_FORMULAS, SOS_CERTIFICATE, fundamental math derivations
- Build log: 2026-06-26 session findings
- BRKGLASS_NR_BRACKET_PROPOSAL: updated to REAL-DATA VALIDATED status
- New docs: FOUNDATIONAL_GUIDANCE, PURE_EQUATION_MAP, CHENTSOV_FINITE_MATH,
BREAKGLASS_FUSION_REVIEW_SPEC, COLD_REVIEWER_FORMULA
- New python: phi pipeline (equation_dna_encoder, ast_parse, charclass,
consistency, embed, output), nr_bracket_validation with receipt
Build: lake build SilverSightRRC — passes on all committed modules.
Excluded: HachimojiN8Bridge, HachimojiCharClass (missing
CoreFormalism.HachimojiManifoldAxiom olean — WIP)
|
2026-06-27 01:56:54 -05:00 |
|
|
|
1a26de076d
|
fix(lean): address vacuous rfl proofs in Chentsov theorem and close Hermite sieve proofs
- ChentsovFinite.lean: Replaced vacuous rfl proofs at uniform distribution permutation invariance, diagonal case, and off-diagonal case with explicit proof obligations and sorry.
- section2_hermite_sieve.lean: Proved repunit strict monotonicity and lower bound lemmas, closing relevant sorry placeholders.
- BindingSiteEntropy.lean: Swapped geodesicDistance placeholder with fisherRaoApprox and added counterexample sketch for fisher_implies_similar_druggability.
- FixedPoint.lean, lakefile.lean, gemma4_mcp.py: Minor fixes and enhancements.
- AGENTS.md: Tracked open Chentsov proof obligations.
Build: 2987 jobs, 0 errors (lake build)
|
2026-06-23 05:11:04 -05:00 |
|
