-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathNOTICE
More file actions
85 lines (55 loc) · 2.65 KB
/
Copy pathNOTICE
File metadata and controls
85 lines (55 loc) · 2.65 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
================================================================================
FDRS Formal
Hyphaeic Public License, Version 1.0
================================================================================
Copyright 2026 Hyphaeic SPC.
This project is licensed under the Hyphaeic Public License, Version 1.0.
https://github.com/hyphaeic/hpl
================================================================================
LICENSOR PARAMETERS
================================================================================
LICENSOR JURISDICTION
---------------------
All disputes arising from this License shall be governed by the laws of,
and adjudicated in the courts of:
State of Washington, United States
CONTACT ADDRESS
---------------
Notices required under Section 4.7 (Affirmative Obligations) shall be
sent to:
legal@hyphaeic.com
COMMERCIAL ROYALTY AMOUNT
-------------------------
In the event of License conversion under Section 4.4.1, the stipulated
commercial value of this Work is:
$50,000 USD per calendar month
PRE-APPROVED AUDITORS
---------------------
If no auditors are listed, Section 4.3.2(b) or 4.3.2(c) shall apply.
================================================================================
REGISTRY INFORMATION
================================================================================
This Work is not registered with the HPL Enforcement Registry.
================================================================================
ENFORCEMENT RIGHTS ASSIGNMENT
================================================================================
Enforcement rights under this License have not been assigned.
================================================================================
THIRD-PARTY COMPONENTS
================================================================================
This project includes the following third-party components:
Mathlib4
License: Apache 2.0
Source: https://github.com/leanprover-community/mathlib4
Lean 4
License: Apache 2.0
Source: https://github.com/leanprover/lean4
================================================================================
ADDITIONAL LICENSOR NOTES
================================================================================
This project is a Lean 4 formalization of Function-Defined Radix Systems
(FDRS). The mathematical specification lives in docs/fdrs.md. The Lean
code in FdrsFormal/ constitutes the licensed Work.
The specification document (docs/fdrs.md) and tooling scripts (scripts/)
are included as part of the Work and subject to the same license terms.
================================================================================