Accounting

Accounting

Lean4 axiomatic kernel for the financial domain. TREND + MOMENTUM + OPTIONS-RISK + SECTOR + DRAWDOWN over portfolios. Defined-risk options only — six strategies enforced at the Strategy enum type level and re-checked by the OPTIONS-RISK predicates. Each verifier run produces a per-predicate report.json + proof-DAG graph.json + intro-rule loci.json — surfaced here as the recent-runs table + latest-run diagram + predicate roster.

version bf1f52572b17

source accounting/lake-manifest.json@bf1f52572b17

built 2026-05-24T20:33:02Z

Frameworks — module readiness

Five frameworks. OPTIONS-RISK enforces the defined-risk allow-list at the type level (6 strategies). Focused = predicates + axioms compile under the current toolchain.

Verifier-run statistics

Aggregate over all examples/<id>/report.json artefacts.

Verifier runs

Portfolios elaborated against the kernel.

Accepted

Kernel verdict: ACCEPTED — every top-level judgment elaborates.

Rejected

Kernel verdict: REJECTED — at least one element disproved.

Latest run

31.1h ago

Balance

Recent verifier runs One row per portfolio elaborated against the kernel. Verdict pill reflects whether every top-level judgment type-checks; the expand row enumerates each kernel rejection's locus (or, when accepted, the judgments proved).
	ID	Portfolio	Frameworks	Judgments	Predicates	Verdict	Failures	Run at
	`balance_sample`	Balance (as of 2026-05-15)	DRAWDOWN · MOMENTUM · OPTIONS-RISK · SECTOR · TREND	is_uptrend, has_momentum, defined_risk_only, is_clean, no_violations, drawdown_disciplined	24 / 24 True	ACCEPTED	0	2026-05-23T13:24:48Z
Verdict accepted — no kernel rejections recorded. `proves_trend` ← `trend.is_uptrend` `proves_momentum` ← `momentum.has_momentum` `balance_legs_clean` ← `options-risk.defined_risk_only` `proves_options_clean` ← `options-risk.is_clean` `proves_no_sector_violations` ← `sector.no_violations` `proves_drawdown_disciplined` ← `drawdown.drawdown_disciplined`
	`hawk_sample`	Hawk (as of 2026-04-26)	OPTIONS-RISK · SECTOR · TREND	is_uptrend, has_violation, defined_risk_only, is_clean	7 / 8 True	ACCEPTED	0	2026-05-16T21:50:58Z
Verdict accepted — no kernel rejections recorded. `proves_trend` ← `trend.is_uptrend` `violates_sector` ← `sector.has_violation` `hawk_legs_clean` ← `options-risk.defined_risk_only` `proves_options_clean` ← `options-risk.is_clean`
	`single_ticker_sample`	Single-Aapl (as of 2026-04-26)	TREND	is_uptrend	4 / 4 True	ACCEPTED	0	2026-05-16T21:46:19Z
Verdict accepted — no kernel rejections recorded. `aapl_uptrend` ← `trend.is_uptrend`
Sorted by runFinishedAt, descending.

Balance — intro-rule shape across 5 judgment(s)

One node per kernel-required element, coloured by per-element verdict. Round nodes are derived structures/theorems; rectangles are predicate slots. The portfolio root is focused.

Predicate roster — Balance Per-predicate atomic view of the most recent run. Each row is one Bool the kernel consumed via Facts.lean; expand the row for evidence and uncertainty rationale.
	#	Predicate	Args	Value	Uncertainty	Evidence	Framework
DRAWDOWN
	22	`max_drawdown_leq`	`Balance 0.15`	True	stubbed	scripts/extract_facts.py — stubbed	DRAWDOWN
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `drawdown/max-drawdown-leq.md`
	23	`time_under_water_leq`	`Balance 90`	True	stubbed	scripts/extract_facts.py — stubbed	DRAWDOWN
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `drawdown/time-under-water-leq.md`
	24	`recovery_within`	`Balance 60`	True	stubbed	scripts/extract_facts.py — stubbed	DRAWDOWN
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `drawdown/recovery-within.md`
MOMENTUM
	5	`rsi_in_range`	`Balance 50.0 70.0`	True	low	Fetched RSI(14) via data/parquet/ta-reference/<symbol>.parquet for all balance_sample holdings	MOMENTUM
Fetched RSI(14) via data/parquet/ta-reference/.parquet for all balance_sample holdings AAPL (7.58% weight): RSI=75.66 (2026-05-15) — overbought MSFT (7.45% weight): RSI=57.90 (2026-05-15) — in range V (7.59% weight): RSI=54.77 (2026-05-14, latest) — in range COST (7.25% weight): RSI=63.20 (2026-05-14, latest) — in range AMZN (3.87% weight): RSI=62.90 (2026-05-14, latest) — in range SPY (7.10% weight): RSI=78.54 (2026-05-14, latest) — overbought RSP (2.83% weight): RSI=58.40 (2026-05-14, latest) — in range Portfolio equity weight: 43.67% (56% cash per portfolio comment) Weighted RSI(14) = (7.58×75.66 + 7.45×57.90 + 7.59×54.77 + 7.25×63.20 + 3.87×62.90 + 7.10×78.54 + 2.83×58.40) / 43.67 = 65.15 Verdict: 65.15 ∈ [50.0, 70.0] → TRUE `momentum/rsi-in-range.md`
	6	`macd_bullish_cross`	`Balance`	True	low	Portfolio: balance_sample (7 equity holdings, as_of: 2026-05-15, window: 1Y = 2025-05-15..2026-05-15)	MOMENTUM
Portfolio: balance_sample (7 equity holdings, as_of: 2026-05-15, window: 1Y = 2025-05-15..2026-05-15) Data source: scripts/data_view.py TA-Lib reference via canonical data/parquet/ta-reference/*.parquet hub MACD calculation: TA-Lib MACD(12,26,9) with EMA-alignment quirk (both fast & slow realigned to slow-1 per reference_talib_macd) Bullish-voted holdings (MACD > signal at as_of AND recent cross within window): AAPL (7.58%): MACD=9.456928 > Signal=7.710739, most recent cross 2026-03-31 COST (7.25%): MACD=7.471947 > Signal=4.577225, most recent cross 2026-05-12 (MOST RECENT OVERALL) SPY (7.10%): MACD=15.424270 > Signal=14.114271, most recent cross 2026-04-02 Subtotal: 21.93% weighted Non-bullish holdings (MACD ≤ signal at as_of): MSFT (7.45%): MACD=3.375477 < Signal=4.687453 (stale cross 2026-04-06 not decisive; signal above) V (7.59%): MACD=3.256186 < Signal=3.367399 (stale cross 2026-03-31; signal crossed above since) AMZN (3.87%): MACD=9.701490 < Signal=11.294106 (stale cross 2026-04-01; signal above) RSP (2.83%): MACD=1.471932 < Signal=1.608763 (stale cross 2026-04-02; signal above) Subtotal: 21.74% weighted Voting tally: 21.93% ÷ 43.67% = 50.22% ≥ 50% threshold → BULLISH MAJORITY Decision rubric met: (1) weighted majority ≥50% ✓ (2) most recent cross within window ✓ (3) MACD above signal at as_of ✓ `momentum/macd-bullish-cross.md`
	7	`roc_positive`	`Balance`	True	low	Computed 1Y ROC for 7 holdings	MOMENTUM
Computed 1Y ROC for 7 holdings Window: 2025-05-15 to 2026-05-15 Holdings with data: AAPL, MSFT, V, COST, AMZN, SPY, RSP AAPL: price_start=210.6144, price_end=300.2300, roc=0.4255 (42.55%), weight=7.58%, weighted_roc=0.032253 AMZN: price_start=205.1700, price_end=267.2200, roc=0.3024 (30.24%), weight=3.87%, weighted_roc=0.011704 COST: price_start=1004.8137, price_end=1041.2500, roc=0.0363 (3.63%), weight=7.25%, weighted_roc=0.002629 MSFT: price_start=450.5129, price_end=421.9200, roc=-0.0635 (-6.35%), weight=7.45%, weighted_roc=-0.004728 RSP: price_start=175.2957, price_end=203.6600, roc=0.1618 (16.18%), weight=2.83%, weighted_roc=0.004579 SPY: price_start=583.7679, price_end=748.1700, roc=0.2816 (28.16%), weight=7.10%, weighted_roc=0.019995 V: price_start=359.4607, price_end=322.5200, roc=-0.1028 (-10.28%), weight=7.59%, weighted_roc=-0.007800 Weights normalized: 43.67% Weighted ROC sum: 0.058632 Portfolio ROC (renormalized): 0.134261 (13.43%) Decision: Portfolio ROC > 0? True `momentum/roc-positive.md`
	8	`momentum_percentile_geq`	`Balance GicsSectorsUniverse 60.0`	True	stubbed	scripts/extract_facts.py — stubbed	MOMENTUM
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `momentum/momentum-percentile-geq.md`
OPTIONS-RISK
	9	`no_naked_short_options`	`Balance`	True	stubbed	scripts/extract_facts.py — stubbed	OPTIONS-RISK
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `options-risk/no-naked-short-options.md`
	10	`debit_only`	`Balance`	True	stubbed	scripts/extract_facts.py — stubbed	OPTIONS-RISK
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `options-risk/debit-only.md`
SECTOR
	11	`cap_respected`	`Balance Accounting.GicsSector.InformationTechnology 0.30`	True	stubbed	scripts/extract_facts.py — stubbed	SECTOR
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `sector/cap-respected.md`
	12	`cap_respected`	`Balance Accounting.GicsSector.ConsumerDiscretionary 0.30`	True	stubbed	scripts/extract_facts.py — stubbed	SECTOR
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `sector/cap-respected.md`
	13	`cap_respected`	`Balance Accounting.GicsSector.Financials 0.30`	True	stubbed	scripts/extract_facts.py — stubbed	SECTOR
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `sector/cap-respected.md`
	14	`cap_respected`	`Balance Accounting.GicsSector.HealthCare 0.30`	True	stubbed	scripts/extract_facts.py — stubbed	SECTOR
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `sector/cap-respected.md`
	15	`cap_respected`	`Balance Accounting.GicsSector.ConsumerStaples 0.30`	True	stubbed	scripts/extract_facts.py — stubbed	SECTOR
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `sector/cap-respected.md`
	16	`cap_respected`	`Balance Accounting.GicsSector.Industrials 0.30`	True	stubbed	scripts/extract_facts.py — stubbed	SECTOR
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `sector/cap-respected.md`
	17	`cap_respected`	`Balance Accounting.GicsSector.Energy 0.30`	True	stubbed	scripts/extract_facts.py — stubbed	SECTOR
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `sector/cap-respected.md`
	18	`cap_respected`	`Balance Accounting.GicsSector.Utilities 0.30`	True	stubbed	scripts/extract_facts.py — stubbed	SECTOR
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `sector/cap-respected.md`
	19	`cap_respected`	`Balance Accounting.GicsSector.Materials 0.30`	True	stubbed	scripts/extract_facts.py — stubbed	SECTOR
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `sector/cap-respected.md`
	20	`cap_respected`	`Balance Accounting.GicsSector.RealEstate 0.30`	True	stubbed	scripts/extract_facts.py — stubbed	SECTOR
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `sector/cap-respected.md`
	21	`cap_respected`	`Balance Accounting.GicsSector.CommunicationServices 0.30`	True	stubbed	scripts/extract_facts.py — stubbed	SECTOR
scripts/extract_facts.py — stubbed — v0 stub — replace with claude -p `sector/cap-respected.md`
TREND
	1	`sma_cross_up`	`Balance`	True	low	computed via data_view.py ta --symbol <SYM> --start 2025-07-19 --end 2026-05-15 — 5 of 7 holdings show SMA(50) > SMA(200) as of 2026-05-15	TREND
computed via data_view.py ta --symbol --start 2025-07-19 --end 2026-05-15 — 5 of 7 holdings show SMA(50) > SMA(200) as of 2026-05-15 — weighted majority test: 65.6% of portfolio weight exhibits golden-cross regime final bar 2026-05-15 from data_view.py ta --symbol AAPL — AAPL: sma50=266.19 > sma200=259.13, weight=7.58%, vote=1.0 — SMA cross-up confirmation per TA-Lib final bar 2026-05-15 from data_view.py ta --symbol MSFT — MSFT: sma50=399.06 < sma200=463.13, weight=7.45%, vote=0.0 — SMA cross-up confirmation per TA-Lib final bar 2026-05-15 from data_view.py ta --symbol V — V: sma50=311.73 < sma200=331.34, weight=7.59%, vote=0.0 — SMA cross-up confirmation per TA-Lib final bar 2026-05-15 from data_view.py ta --symbol COST — COST: sma50=1000.12 > sma200=953.90, weight=7.25%, vote=1.0 — SMA cross-up confirmation per TA-Lib final bar 2026-05-15 from data_view.py ta --symbol AMZN — AMZN: sma50=235.80 > sma200=229.25, weight=3.87%, vote=1.0 — SMA cross-up confirmation per TA-Lib final bar 2026-05-15 from data_view.py ta --symbol SPY — SPY: sma50=688.88 > sma200=675.55, weight=7.10%, vote=1.0 — SMA cross-up confirmation per TA-Lib final bar 2026-05-15 from data_view.py ta --symbol RSP — RSP: sma50=198.09 > sma200=193.43, weight=2.83%, vote=1.0 — SMA cross-up confirmation per TA-Lib `trend/sma-cross-up.md`
	2	`slope_positive`	`Balance`	True	medium	window: 2025-05-15 to 2026-05-15 (exactly 1 year)	TREND
window: 2025-05-15 to 2026-05-15 (exactly 1 year) 7 symbols fetched: AAPL(252 bars), MSFT(252), V(251), COST(251), AMZN(251), SPY(251), RSP(251) Per-symbol log(close) OLS slopes: AAPL=+0.001298, MSFT=-0.001058, V=-0.000606, COST=+0.000025, AMZN=+0.000365, SPY=+0.000632, RSP=+0.000503 Weights renormalized to sum=43.67 (equities only; ~56% cash not modeled) Weighted slope calculation: (0.001298×7.58 - 0.001058×7.45 - 0.000606×7.59 + 0.000025×7.25 + 0.000365×3.87 + 0.000632×7.1 + 0.000503×2.83) / 43.67 Weighted portfolio slope: +0.000111 (strictly positive ✓) `trend/slope-positive.md`
	3	`r_squared_geq`	`Balance 0.5`	True	low	Fetched 252 bars for AAPL (2025-05-15..2026-05-15): R²=0.6889, slope=+0.00130, 251 trading days	TREND
Fetched 252 bars for AAPL (2025-05-15..2026-05-15): R²=0.6889, slope=+0.00130, 251 trading days Fetched 252 bars for MSFT: R²=0.5175, slope=-0.00106, 252 trading days Fetched 251 bars for V: R²=0.6931, slope=-0.00061, 251 trading days Fetched 251 bars for COST: R²=0.0014, slope=+0.000025 (flat), 251 trading days Fetched 251 bars for AMZN: R²=0.1418, slope=+0.000365 (noisy), 251 trading days Fetched 251 bars for SPY: R²=0.7301, slope=+0.000632, 251 trading days Fetched 251 bars for RSP: R²=0.8099, slope=+0.000503, 251 trading days Portfolio weight coverage: 43.67% (7 equity holdings, rest cash) Weighted-average R² = (0.6889×7.58 + 0.5175×7.45 + 0.6931×7.59 + 0.0014×7.25 + 0.1418×3.87 + 0.7301×7.10 + 0.8099×2.83) ÷ 43.67 = 0.5123 Decision: 0.5123 ≥ 0.5 threshold → TRUE `trend/r-squared-geq.md`
	4	`adx_geq`	`Balance 20.0`	True	low	ADX(14) as of 2026-05-15 for balance_sample holdings: AAPL=29.584, MSFT=44.252, V=29.004, COST=23.065, AMZN=22.549, SPY=25.468, RSP=14.521	TREND
ADX(14) as of 2026-05-15 for balance_sample holdings: AAPL=29.584, MSFT=44.252, V=29.004, COST=23.065, AMZN=22.549, SPY=25.468, RSP=14.521 Weights: AAPL=7.58%, MSFT=7.45%, V=7.59%, COST=7.25%, AMZN=3.87%, SPY=7.10%, RSP=2.83% (total=43.67%) Weighted-average ADX(14) = 28.6347 All holdings have non-null ADX values (300-day window 2025-08-10 to 2026-05-15 fully populated) `trend/adx-geq.md`
DRAWDOWN · MOMENTUM · OPTIONS-RISK · SECTOR · TREND — 24 of 24 True.

Metrics

frameworkCount: 5
frameworksPresent: 5
runsTotal: 3
runsAccepted: 3
runsRejected: 0
latestRunId: balance_sample
latestRunAt: 2026-05-23T13:24:48Z
latestVerdict: ACCEPTED
latestProofGraphUrl: https://qresev.quantapix.com/proof-graph/run/balance_sample/

Frameworks — module readiness

Verifier-run statistics

Verifier runs

Accepted

Rejected

Latest run

Balance — intro-rule shape across 5 judgment(s)

Balance

Trend.is_uptrend

smaCross

slope

rSquared

adx

Momentum.has_momentum

rsi

macd

roc

rank

OptionsRisk.is_clean

OptionsRisk.defined_risk_only

noNaked

debitOnly

Sector.no_violations

∀ s, cap_respected

Drawdown.drawdown_disciplined

maxDD

tuw

recovers

Metrics