mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
35bb1274e0
Two defects in the pushed Tier-1 Layer-3 work (8c5ee2aa/ba8ee111), both
invisible to single-file LSP checks but caught by a clean `lake build`:
1. BUILD-BLOCKER: `import Mathlib.LinearAlgebra.Matrix.Adjoints` — no such
mathlib module (the real one is `Matrix.Adjugate`), and nothing in the file
used it. Dead + wrong import; `lake build SilverSight.PIST.UnifiedCovariant`
failed with "bad import" until removed. The file did NOT compile on main.
2. HONESTY: `admits_Cartan_connection` / `has_SO_1_6_holonomy` were
`def ... := Nonempty (M -> M)`, trivially inhabited by `id` -- a stealth-True.
The docstrings falsely claimed "neither True nor provable." Reverted to
opaque `axiom ... : Type -> Prop` signatures (assert nothing; tagged
HONESTY CLASS: OPAQUE). Companion conjectures can now ONLY be closed by
their CONJECTURE sorry, not a silent `<id>`. Scanner blind spot for this
pattern (Nonempty (M->M), not literal := True) noted for a follow-up.
Verified: `lake build` green (3299 jobs). Axiom footprint matches the §7
whitelist -- goldenCP7_is_Kaehler = {propext, Classical.choice, Quot.sound,
sorryAx}; Cartan_connection_on_J1_exists adds only the OPAQUE
admits_Cartan_connection. No stray custom axioms.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
||
|---|---|---|
| .. | ||
| BindingSite | ||
| CoreFormalism | ||
| PVGS_DQ_Bridge | ||
| RRCLib | ||
| SilverSight | ||
| UniversalEncoding | ||