SilverSight/formal/CoreFormalism
allaun f7858914b7 docs: fix documentation gaps + add pure math description
Fixed 5 undocumented Lean files:
- PVGS_DQ_Bridge/section5_quantum_sensing.lean — quantum sensing docs
- PVGS_DQ_Bridge/section2_hermite_sieve.lean — Hermite polynomial docs
- SilverSight/RRC/ReceiptDensity.lean — receipt density scoring docs
- SilverSight/PIST/SpectralWitness.lean — spectral witness docs
- CoreFormalism/FixedPoint.lean — stub redirect docs

Added docs/PURE_MATH_DESCRIPTION.md:
- Pure mathematical description of each module (no code)
- Why each module exists (problem/insight)
- What a graph calculator would need to implement each
- 10 modules covered: SidonSets, BraidEigensolid, BraidSpherionBridge,
  HachimojiLUT, ChentsovFinite, DynamicCanal, Schema, WireFormat,
  Receipt, Bind
2026-06-23 05:21:58 -05:00
..
Bind.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
BraidBracket.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
BraidCross.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
BraidEigensolid.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
BraidField.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
BraidSpherionBridge.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
BraidStrand.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
ChentsovFinite.lean fix(lean): address vacuous rfl proofs in Chentsov theorem and close Hermite sieve proofs 2026-06-23 05:11:04 -05:00
DynamicCanal.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
FixedPoint.lean docs: fix documentation gaps + add pure math description 2026-06-23 05:21:58 -05:00
HachimojiBase.lean Initial SilverSight: deterministic equation search via Fisher geometry 2026-06-21 18:02:05 +08:00
HachimojiBridging.lean feat(bmcte): N=20000 sweep on neon-64gb + Hachimoji bridge theorem 2026-06-22 14:17:31 -05:00
HachimojiCodec.lean docs(silversight): document λ(p) bosonic estimator results 2026-06-22 01:33:59 -05:00
HachimojiLUT.lean fix(dna): correct alphabet ordering ATGCBSPZ→ABCGPSTZ + proof cleanup 2026-06-22 23:20:16 -05:00
HachimojiManifoldAxiom.lean Initial SilverSight: deterministic equation search via Fisher geometry 2026-06-21 18:02:05 +08:00
InteractionGraphSidon.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
Q16_16Numerics.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
SidonSets.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
SieveLemmas.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
Tactics.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00