Skip to content

Commit ce7ed93

Browse files
committed
fix(lean): sync DSL pricing disclaimer + broaden gitignore
DSL.lean defaultRevenueShare comment carries the full disclaimer that 70/30 is a generic library default, NOT production pricing (90/10 standard, 95/5 founding) — prevents a "Nexbid takes 30%" misreading in the public repo.
1 parent 6df2e23 commit ce7ed93

2 files changed

Lines changed: 12 additions & 2 deletions

File tree

lean-verification/.gitignore

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,8 @@
1+
# Lean build artifacts
12
.lake/
2-
build/
33
*.olean
44
*.ilean
5+
*.c
6+
7+
# macOS
8+
.DS_Store

lean-verification/NexbidVerify/Commerce/DSL.lean

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,13 @@ structure RevenueShare where
99
shares_nonneg : 0 ≤ publisherShare ∧ 0 ≤ platformShare
1010
shares_sum_one : publisherShare + platformShare = 1
1111

12-
/-- Default 70/30 revenue share. -/
12+
/-- Default 70/30 revenue share — generic library default.
13+
Note: This is the example default for the RevenueShare structure,
14+
NOT the production tier-pricing. Nexbid's production AdCP match-revenue
15+
split uses 90/10 (PLATFORM_FEE_STANDARD = 0.10 in packages/shared/src/pricing.ts,
16+
Founding 95/5 via PLATFORM_FEE_FOUNDING = 0.05). Per-customer overrides
17+
are stored in the platform_pricing DB table. The proofs in this file are
18+
generic over any valid RevenueShare and do not depend on this default. -/
1319
def defaultRevenueShare : RevenueShare := {
1420
publisherShare := 7 / 10
1521
platformShare := 3 / 10

0 commit comments

Comments
 (0)