allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
SilverSight/BREAKGLASS_LOG.md
allaun 8ac5ce0c6f feat(lean): Sidon-orthogonality bypass closes operator-norm gap 
Replaces the spectral-radius operator norm bound (left as
TODO(lean-port: operator_norm_bound)) with a computable L_infinity
row-sum norm over Fin 8, discharged by dec_trivial.

Key changes:
- crossingMatrix: Matrix (Fin 8) (Fin 8) Q with explicit Sidon entries
- maxRowSum: L_infinity row-sum norm, computed by Finset.sup
- crossing_matrix_norm_bound: maxRowSum <= 1775/1792 (dec_trivial)
- braid_operator_contractive: ||C*s||_oo <= r * ||s||_oo for r=1775/1792
- Removes deprecated EigensolidConvergenceHypothesis (now a theorem)
- Standalone formula doc: docs/reviews/SIDON_ORTHOGONALITY_BYPASS_FORMULA.md
- CONJECTURE_UPGRADE_ROADMAP.md updated (conjecture 1 resolved)
- BREAKGLASS_LOG.md: entry 2 logged

Sidon uniqueness (I4) guarantees at most 2 non-zero entries per row,
making the row-sum a concrete rational — no spectral theory required.

Build: 3307 jobs, 0 errors (lake build SilverSight)
2026-06-26 23:36:55 -05:00

754 B
Raw Blame History

Breakglass Fusion — Merge Log

YYYY-MM-DD | Module                     | Summary                                                              | Reviewer    | Gates
2026-06-26 | UnifiedCovariant.lean      | eigensolid_convergence hypothesis → theorem (0 sorries, 3307 jobs)   | breakglass  | A B C all pass
2026-06-26 | UnifiedCovariant.lean      | Sidon-orthogonality bypass: replaces spectral-radius operator norm   | breakglass  | A B C all pass
                             |                            | with computable L∞ row-sum bound (crossingMatrix + maxRowSum         |             |
                             |                            | + norm_num). Removes EigensolidConvergenceHypothesis @[deprecated].  |             |