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/formal/CoreFormalism
History
allaun 635d83a90d fix(transform): rewrite CharacterTransform.lean — 0 native_decide, 0 sorries, 0 axioms 
Replaced native_decide with:
- decide (finite enumeration of 4096 Sidon quadruples)
- fin_cases i <;> decide (8×4 character computation)
- norm_num (integer arithmetic)
- omega (integer inequalities)

Proofs:
§1: sidonLabels8_is_sidon — decide (8⁴ = 4096 cases)
§2: charVec_range — omega (range checks)
§3: gram_self/gram_adjacent/gram_cross_pair — fin_cases + decide
§4: cartanWeight — structural equalities (rfl, simp)
§5: block_eigenvalues — norm_num
§6: spectral_gap_chain — norm_num

Clean chain: Sidon → Z₂⁴ character → Cartan → gap. All ℤ/ℚ.
2026-06-30 20:32:51 -05:00
..
Bind.lean refactor(core): typed Invariant/TensorType migration, CartanConnection cleanup 2026-06-28 00:11:28 -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 refactor(core): typed Invariant/TensorType migration, CartanConnection cleanup 2026-06-28 00:11:28 -05:00
BraidField.lean refactor(core): typed Invariant/TensorType migration, CartanConnection cleanup 2026-06-28 00:11:28 -05:00
BraidSpherionBridge.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
BraidStateN.lean verify(character): integer-only Z₂⁴ transform — 12/12 consensus, zero floats 2026-06-30 20:24:19 -05:00
BraidStrand.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
CharacterTransform.lean fix(transform): rewrite CharacterTransform.lean — 0 native_decide, 0 sorries, 0 axioms 2026-06-30 20:32:51 -05:00
ChentsovFinite.lean chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -05:00
DynamicCanal.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
E8Sidon.lean docs: Hopf Portability Criterion + Ingest Bridge — 4-agent synthesis 2026-06-30 19:53:58 -05:00
FixedPoint.lean feat(lean): Add FisherRigidity bridge for parabola focal-chord to Fisher-Rao 2026-06-24 10:24:54 -05:00
GoormaghtighEnumeration.lean feat(phi): Hachimoji N=8 foundation, Phi pipeline, AVMIsa audit report 2026-06-28 00:11:39 -05:00
HachimojiBase.lean chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -05:00
HachimojiBridging.lean chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -05:00
HachimojiCodec.lean chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -05:00
HachimojiLUT.lean chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -05:00
HachimojiManifoldAxiom.lean feat(lean): add PhiPipelineReceipt, HachimojiManifoldAxiom; quarantine PVGS 2026-06-30 04:54:14 -05:00
HopfFibration.lean verify(character): integer-only Z₂⁴ transform — 12/12 consensus, zero floats 2026-06-30 20:24:19 -05:00
InteractionGraphSidon.lean feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
Q16_16Numerics.lean chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -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