- Ported MultiSurfacePacker.lean from Research Stack to formal/SilverSight/PIST/MultiSurfacePacker.lean.
- Refactored coherenceOverlap to use custom getD and foldlIdx list helpers to ensure pure kernel reduction.
- Fixed a logical bug in legacy gcclSwapGate (incorrect swap direction comparison), aligning logic with expected rejection of cost-increasing expansions.
- Proved coherenceGateAcceptsIdentical, coherenceGateRejectsOrthogonal, and gcclRejectsExpansion theorems with zero sorrys.
- Registered MultiSurfacePacker in lakefile.lean and AGENTS.md.
Build: 3307 jobs, 0 errors (lake build)
- Created formal/SilverSight/PIST/CrossDomainSynthesis.lean defining superconductor critical ratios, spectral gap, and Rydberg quantum defect scaling.
- Proved superconductor ratios and spectral gap lie within the [1/8, 1/6] chaotic band.
- Proved these physical parameters deviate by less than 1.5% (raw 983) from the exact 1/7 threshold.
- Proved rydberg_defect_monotonic (monotonic decay of quantum defect with n) with zero sorrys.
- Registered CrossDomainSynthesis module in lakefile.lean and AGENTS.md.
Build: 3307 jobs, 0 errors (lake build)
- Created formal/SilverSight/PIST/Tdoku16D.lean defining State16D and constraint propagation engine step/cycle.
- Proved erdos_336_order (order = 2) and erdos_336_exact_order (exact_order = 3) theorems via native_decide (reflexive VM decision loop) with zero sorrys.
- Registered SilverSight.PIST.Tdoku16D in lakefile.lean roots.
- Documented PIST/Tdoku16D.lean status in AGENTS.md.
Build: 3307 jobs, 0 errors (lake build)
Added Q16_16 multiplication, division, and comparison operators to Prim
and Step semantics. Implemented static type checking (checkInstr,
checkProgram) in TypeCheck.lean and proved the step_preservation safety
theorem in TypeSafety.lean. Verified with new arithmetic execution
canaries in Run.lean.
Build: 3307 jobs, 0 errors (lake build)
UnifiedCovariant.lean:
- Quarantined Layer 2/2b: goldenEndomorphism, eigensolid_convergence,
crossingMatrix, and Sidon-orthogonality bypass sections removed due to
Mathlib 4.30.0-rc2 import path incompatibilities (Topology.*, LinearAlgebra.Basic)
- Wired Layer 2c: NR bracket MC equation (gate_C_d_CE_mu_zero from
CartanConnection.lean) and Yang-Baxter integrability
(layer_2d_yang_baxter_holds from YangBaxter.lean) with full docstrings
- Fixed Sidon lemma: revert+dec_trivial replaces direct dec_trivial
(fixes 'Expected type must not contain free variables' on Fin 8)
AGENTS.md:
- Added CartanConnection and YangBaxter to module status table
- Documented Layer 2c/2d architecture and Layer 2b quarantine
- Updated sorry counts (Layer 3 only, 7 geometric conjectures)
Build: 3299 jobs, 0 errors (lake build SilverSight.PIST.UnifiedCovariant)
Also verified: SilverSight.PIST.CartanConnection and
SilverSight.PIST.YangBaxter build cleanly
- CoreFormalism/ChentsovFinite.lean now tracked in module table
- Consolidated old sorry entries into single 'chentsov-core' entry
- Build verified: 3307 jobs, 0 errors
Add docs/hachimoji_torsor_consequences.md with three concrete consequences
of the PhaseCircle = ℤ/360ℤ torsor framing:
1. phaseEmbed_injective_on_canonical and BinaryLUT.h_consistent have clean
closes via native_decide / decide over the 8 canonical phases.
2. HachimojiTokenEmbed.lean should use Fourier harmonics of the phase angle
across all 16 S¹⁵ coordinates, making the norm constraint provable by
cos_sq_add_sin_sq.
3. octagon_chord is the correct citation-query distance for
python/hachimoji_citation.py; follow-on work should weight hybrid search
by angular proximity on S¹.
Also updates docs/GLOSSARY.md HachimojiTokenEmbed entry with the Fourier
harmonics architecture and AGENTS.md with a cross-reference.
Regenerate docs/PROJECT_MAP.* to track the new file.
Build: N/A (documentation only)
Ports three Research Stack RRC gates into formal/SilverSight/RRC/ using the existing CoreFormalism braid and Q16_16 surfaces.
Adds a Lean ↔ C ↔ Python Q16_16 roundtrip test:
- c/q16_canonical.c: canonical saturating Q16_16 C library
- exe/Q16_16Roundtrip.lean: Lake extern_lib linked executable
- tests/test_q16_roundtrip.py: Python ↔ C harness (revived from quarantine)
Updates lakefile.lean with q16-roundtrip executable and extern_lib q16_canonical.
Build: lake build SilverSightRRC 3006 jobs, 0 errors; q16-roundtrip 5949 jobs, 0 errors
- Convert placeholder paper references from type: article to type: unpublished
with honest notes about pending identifiers
- Remove fake journal/arXiv placeholder from Giani et al.
- Add CFF standards section to AGENTS.md with validation command and rules for
DOIs, preprints, non-academic sources, and et al. usage
Build: 2978 jobs, 0 errors (lake build)
