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. The axiomatize-trading program strip reads the committed universe rollup — encoded S&P 500 symbols tiered A/B/C and their share of the GICS universe.

version bf1f52572b17

source accounting/lake-manifest.json@bf1f52572b17

built 2026-07-24T09:25:07Z

DEGRADED

Correction · 2026-07-14

Agreement-tier figures withdrawn pending re-verification

What we found. Our own adversarial review lane found leak channels in the cross-axis agreement oracle that classifies our Tier-A/B/C figures. The fan-out agents that are supposed to agree independently could, in principle, see each other's work — so blind agreement was never established for any wave.

What survives. Kernel soundness is unaffected and mechanically re-checked: every lake build, every sorry-free proof still stands. You cannot leak your way into a green build — the encoded work is real. Only the agreement-based confidence is in question.

What is withdrawn. The agreement-based tier counts (proving's Tier-A/B/C and accounting's) are withdrawn — shown as "withheld", restated provisional as of 2026-07-14. Sections-encoded, universe %, sector census and the soundness panels are mechanical and remain.

The schedule. Re-earning a tier means a fresh blind re-slice under the now-closed contracts, not a re-score of the old one. It is sequenced cheapest-first: the operational axis re-attacks first, the financial axis re-slices next, and the textual re-slice is a multi-week program. This notice updates as each axis re-earns its figure.

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

4.7d ago

Refuses Hedging Judgment Sample

Axiomatize-trading program

Universe coverage from accounting/coverage.json (dat-cross rollup).

Symbols encoded

S&P 500 GICS universe symbols with a committed sorry-free confluence encoding (Bridge.lean), across all axes.

Tier-A

withheld

Agreement-tier confidence withdrawn 2026-07-14 — the cross-axis agreement oracle is under re-verification (blind re-slice pending). Encoded-symbol and soundness figures are unaffected.

Sectors touched

4/11

Distinct GICS sectors with ≥1 encoded universe symbol.

Of S&P 500 universe

1.90%

Share of the 526-symbol GICS universe encoded so far.

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	Predicates	Verdict	Failures	Run at
	`refuses_hedging_judgment_sample`	Refuses Hedging Judgment Sample (as of 2026-07-16)	0 / 2 True	ACCEPTED	0	2026-07-19T15:43:36Z
Verdict accepted — no kernel rejections recorded for this run.
	`hedging_judgment_sample`	Hedging Judgment Sample (as of 2026-07-16)	5 / 5 True	ACCEPTED	0	2026-07-19T15:41:14Z
Verdict accepted — no kernel rejections recorded for this run.
	`refuses_hedging_deriv_sample`	Refuses Hedging Deriv Sample (as of 2026-07-16)	0 / 2 True	ACCEPTED	0	2026-07-19T15:13:20Z
Verdict accepted — no kernel rejections recorded for this run.
	`hedging_deriv_sample`	Hedging Deriv Sample (as of 2026-07-16)	2 / 2 True	ACCEPTED	0	2026-07-19T15:11:54Z
Verdict accepted — no kernel rejections recorded for this run.
	`refuses_hedging_off_sample`	Refuses Hedging Off Sample (as of 2026-07-16)	0 / 1 True	ACCEPTED	0	2026-07-19T14:55:51Z
Verdict accepted — no kernel rejections recorded for this run.
	`hedging_off_sample`	Hedging Off Sample (as of 2026-07-16)	1 / 1 True	ACCEPTED	0	2026-07-19T14:54:42Z
Verdict accepted — no kernel rejections recorded for this run.
	`refuses_hedging_gates_sample`	Refuses Hedging Gates Sample (as of 2026-07-16)	0 / 4 True	ACCEPTED	0	2026-07-17T21:23:35Z
Verdict accepted — no kernel rejections recorded for this run.
	`hedging_gates_sample`	Hedging Gates Sample (as of 2026-07-16)	4 / 4 True	ACCEPTED	0	2026-07-17T21:20:15Z
Verdict accepted — no kernel rejections recorded for this run.
	`refuses_hedging_beta_sample`	Refuses Hedging Beta Sample (as of 2026-07-16)	0 / 1 True	ACCEPTED	0	2026-07-17T21:00:35Z
Verdict accepted — no kernel rejections recorded for this run.
	`hedging_beta_sample`	Hedging Beta Sample (as of 2026-07-16)	1 / 1 True	ACCEPTED	0	2026-07-17T20:59:33Z
Verdict accepted — no kernel rejections recorded for this run.
Sorted by runFinishedAt, descending.

Balance — intro-rule shape across 4 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
	18	`max_drawdown_leq`	`Balance 0.15`	True	low	portfolio-equity-curve returned 252 rows spanning 2025-05-15 → 2026-05-15 from financial/parquet/ohlcv-equities/	DRAWDOWN
portfolio-equity-curve returned 252 rows spanning 2025-05-15 → 2026-05-15 from financial/parquet/ohlcv-equities/ running-peak equity = 0.49455467 (pre-trough); trough equity = 0.42675960 on 2026-03-27 max_drawdown = -0.11430803 (i.e. -11.43% peak-to-trough) abs(max_drawdown) = 0.1143 ≤ bound 0.15 → PASS by margin of 0.0357 `drawdown/max-drawdown-leq.md`
	19	`time_under_water_leq`	`Balance 90`	False	low	scripts/data_view.py portfolio-equity-curve --path examples/balance_sample/portfolio.json --start 2025-05-15 --end 2026-05-15 → 252 rows	DRAWDOWN
scripts/data_view.py portfolio-equity-curve --path examples/balance_sample/portfolio.json --start 2025-05-15 --end 2026-05-15 → 252 rows equity curve walked with running peak; strictly-below-peak streaks measured longest_uw_days = 126 (first_eq=0.4367, last_eq=0.49455) 126 > daysCap 90 → underwater stretch exceeds cap `drawdown/time-under-water-leq.md`
	20	`recovery_within`	`Balance 60`	True	low	equity curve over 1Y window (2025-05-15 → 2026-05-15): 252 trading bars	DRAWDOWN
equity curve over 1Y window (2025-05-15 → 2026-05-15): 252 trading bars worst drawdown = -11.43% (trough at index 217, date 2026-03-27) prior_peak (running) = 0.48; trough_equity = 0.43 recovered = true; recovery_days = 24 (first bar at/above prior_peak, index 241) recovery_days 24 <= daysCap 60 -> within cap (margin 36 days) elapsed_since_trough = 34 bars, but recovery already completed before as_of `drawdown/recovery-within.md`
OPTIONS-RISK
	5	`no_naked_short_options`	`Balance`	True	low	portfolio.option_legs[0..1] — 1 short leg scanned (QQQ 2026-06-12 685P side=short qty=1); collateralized by long QQQ 2026-06-12 700P qty=1 (strike 700 > 685, same expiry, equal qty) = debit put spread	OPTIONS-RISK
portfolio.option_legs[0..1] — 1 short leg scanned (QQQ 2026-06-12 685P side=short qty=1); collateralized by long QQQ 2026-06-12 700P qty=1 (strike 700 > 685, same expiry, equal qty) = debit put spread — short put has a sibling long put at a HIGHER strike (700 > 685), same expiry, equal qty — the only allowed put-spread shape; 0 naked shorts across 1 short leg scanned `options-risk/no-naked-short-options.md`
	6	`debit_only`	`Balance`	True	low	portfolio.option_legs[0,1] — QQQ 2026-06-12: long 700p (premium_paid 13.70) + short 685p (premium_received 9.16) → debit spread (long strike 700.0 > short strike 685.0); net debit = 13.70 - 9.16 = 4.54	OPTIONS-RISK
portfolio.option_legs[0,1] — QQQ 2026-06-12: long 700p (premium_paid 13.70) + short 685p (premium_received 9.16) → debit spread (long strike 700.0 > short strike 685.0); net debit = 13.70 - 9.16 = 4.54 — debit put spread (long strike > short strike), net debit 4.54 paid up front; max loss = net_debit × 100 × qty = 4.54 × 100 × 1 = $454, finite and bounded; structure_hint=debit_spread_put confirmed by strike-shape `options-risk/debit-only.md`
SECTOR
	7	`cap_respected`	`Balance Accounting.GicsSector.InformationTechnology 0.30`	True	low	GICS authority financial/parquet/gics-symbols.parquet confirms AAPL → Information Technology, MSFT → Information Technology	SECTOR
GICS authority financial/parquet/gics-symbols.parquet confirms AAPL → Information Technology, MSFT → Information Technology Information Technology holdings: AAPL weight_pct=7.58, MSFT weight_pct=7.45 sector_weight = 7.58% + 7.45% = 15.03% = 0.1503 cap = 0.30; 0.1503 ≤ 0.30 → true No other holding maps to Information Technology (V=Financials, COST=Consumer Staples, AMZN=Consumer Discretionary, SPY/RSP=Index synthetic) `sector/cap-respected.md`
	8	`cap_respected`	`Balance Accounting.GicsSector.ConsumerDiscretionary 0.30`	True	low	Consumer Discretionary holdings in balance_sample/portfolio.json: AMZN only, weight_pct=3.87	SECTOR
Consumer Discretionary holdings in balance_sample/portfolio.json: AMZN only, weight_pct=3.87 Σ weight (Consumer Discretionary) = 3.87% = 0.0387 No other holding carries gics_sector='Consumer Discretionary' (IT: AAPL+MSFT, Financials: V, Staples: COST, Index: SPY+RSP) Decision: sector_weight 0.0387 ≤ cap 0.30 → true `sector/cap-respected.md`
	9	`cap_respected`	`Balance Accounting.GicsSector.Financials 0.30`	True	low	Portfolio examples/balance_sample/portfolio.json, nav_usd=100615.82, as_of=2026-05-15	SECTOR
Portfolio examples/balance_sample/portfolio.json, nav_usd=100615.82, as_of=2026-05-15 Holdings with gics_sector == 'Financials': V (Visa Inc.) weight_pct=7.59 → 0.0759 No other Financials holding; SPY/RSP carry synthetic gics_sector='Index' (excluded) sector_weight = 0.0759 ≤ cap 0.30 → true Margin: 0.30 − 0.0759 = 0.2241 (no knife-edge) `sector/cap-respected.md`
	10	`cap_respected`	`Balance Accounting.GicsSector.HealthCare 0.30`	True	low	balance_sample portfolio has 7 equity holdings; sectors present = [Consumer Discretionary, Consumer Staples, Financials, Index, Information Technology] — NO Health Care holding exists	SECTOR
balance_sample portfolio has 7 equity holdings; sectors present = [Consumer Discretionary, Consumer Staples, Financials, Index, Information Technology] — NO Health Care holding exists Σ weight_pct where gics_sector=='Health Care' = 0.0 (empty contributing set []) sector_weight = 0.000 (fraction), cap = 0.30 → 0.000 <= 0.30 holds Largest single-sector exposure for reference is Information Technology = 15.03% (AAPL 7.58 + MSFT 7.45), still well under cap; Health Care is simply absent `sector/cap-respected.md`
	11	`cap_respected`	`Balance Accounting.GicsSector.ConsumerStaples 0.30`	True	low	Consumer Staples holdings in balance_sample/portfolio.json: COST (Costco Wholesale) weight_pct=7.25	SECTOR
Consumer Staples holdings in balance_sample/portfolio.json: COST (Costco Wholesale) weight_pct=7.25 No other holding carries gics_sector=='Consumer Staples' (AAPL/MSFT=Information Technology, V=Financials, AMZN=Consumer Discretionary, SPY/RSP=Index) sector_weight = 0.0725; cap = 0.30; 0.0725 <= 0.30 → true margin to cap = 0.2275 (22.75 pp of headroom) `sector/cap-respected.md`
	12	`cap_respected`	`Balance Accounting.GicsSector.Industrials 0.30`	True	low	Industrials matching holdings: [] (zero holdings carry gics_sector == 'Industrials')	SECTOR
Industrials matching holdings: [] (zero holdings carry gics_sector == 'Industrials') Σ weight_pct where gics_sector=='Industrials' = 0.0 → sector_weight fraction = 0.000 cap = 0.30; decision 0.000 <= 0.30 → true Sectors actually present in balance_sample: Consumer Discretionary, Consumer Staples, Financials, Index, Information Technology (no Industrials) `sector/cap-respected.md`
	13	`cap_respected`	`Balance Accounting.GicsSector.Energy 0.30`	True	low	Computed from examples/balance_sample/portfolio.json (NAV 100,615.82, as_of 2026-05-15).	SECTOR
Computed from examples/balance_sample/portfolio.json (NAV 100,615.82, as_of 2026-05-15). Energy holdings matched: [] (zero holdings with gics_sector == 'Energy'). Energy sector_weight = 0.0 (sum of matched weight_pct = 0.00% / 100). Portfolio sectors present: Consumer Discretionary, Consumer Staples, Financials, Index, Information Technology — none is Energy. Decision: 0.0 <= 0.30 -> true. `sector/cap-respected.md`
	14	`cap_respected`	`Balance Accounting.GicsSector.Utilities 0.30`	True	low	Portfolio examples/balance_sample/portfolio.json: 7 holdings, none with gics_sector == 'Utilities'	SECTOR
Portfolio examples/balance_sample/portfolio.json: 7 holdings, none with gics_sector == 'Utilities' Matching holdings for sector 'Utilities': [] (empty set) sector_weight = Σ(weight_pct where gics_sector=='Utilities') / 100 = 0.0 Sectors actually present: Consumer Discretionary, Consumer Staples, Financials, Index, Information Technology Decision: 0.0 <= 0.30 cap → true `sector/cap-respected.md`
	15	`cap_respected`	`Balance Accounting.GicsSector.Materials 0.30`	True	low	Materials contributing holdings: [] (none of the 7 holdings have gics_sector=='Materials')	SECTOR
Materials contributing holdings: [] (none of the 7 holdings have gics_sector=='Materials') sector_weight = 0.0 (sum of matching holding weight_pct / 100) cap = 0.30 decision weight<=cap: True sectors present in portfolio: Consumer Discretionary, Consumer Staples, Financials, Index, Information Technology `sector/cap-respected.md`
	16	`cap_respected`	`Balance Accounting.GicsSector.RealEstate 0.30`	True	low	Portfolio examples/balance_sample/portfolio.json has 7 equity holdings across sectors: ['Consumer Discretionary', 'Consumer Staples', 'Financials', 'Index', 'Information Technology'].	SECTOR
Portfolio examples/balance_sample/portfolio.json has 7 equity holdings across sectors: ['Consumer Discretionary', 'Consumer Staples', 'Financials', 'Index', 'Information Technology']. No holding maps to GICS sector 'Real Estate' (real_estate_holdings: [] — empty contributing set). Σ weight where gics_sector == 'Real Estate' = 0.0 (0.00%). cap = 0.30; decision 0.0 <= 0.30 -> True. `sector/cap-respected.md`
	17	`cap_respected`	`Balance Accounting.GicsSector.CommunicationServices 0.30`	True	low	Matching holdings where gics_sector == 'Communication Services': [] (zero holdings)	SECTOR
Matching holdings where gics_sector == 'Communication Services': [] (zero holdings) sector_weight = 0.0 (sum of matching weight_pct / 100 = 0.00) cap = 0.30 Sectors actually present: Consumer Discretionary, Consumer Staples, Financials, Index, Information Technology Decision: 0.0 <= 0.30 -> true `sector/cap-respected.md`
TREND
	1	`sma_cross_up`	`Balance`	True	low	computed @ as_of=2026-05-15 — 5 of 7 holdings show SMA(50) > SMA(200) at 2026-05-15; weighted 65.56% above	TREND
computed @ as_of=2026-05-15 — 5 of 7 holdings show SMA(50) > SMA(200) at 2026-05-15; weighted 65.56% above — weighted majority (≥50%) confirms golden-cross trend regime data_view.py ta final row per symbol — AAPL sma50=266.19 > sma200=259.13; COST sma50=1001.45 > sma200=954.50; AMZN sma50=236.71 > sma200=229.42; SPY sma50=690.04 > sma200=676.07; RSP sma50=198.11 > sma200=193.51 — five holdings in golden-cross regime data_view.py ta final row — MSFT sma50=399.06 < sma200=463.13; V sma50=311.85 < sma200=331.21 — two holdings below their SMA(200) (death-cross), outvoted by weight `trend/sma-cross-up.md`
	2	`slope_positive`	`Balance`	True	medium	Window 2025-05-15 → 2026-05-15; 7 equity holdings, 252 bars each (sufficient, ≥50).	TREND
Window 2025-05-15 → 2026-05-15; 7 equity holdings, 252 bars each (sufficient, ≥50). Weighted-average log-close OLS slope = +0.00011454 (strictly > 0) → true. Renormalized over total weight 43.67 (equity sleeve of balance_sample). Per-symbol log-close slopes: AAPL +0.00129767, MSFT -0.00105845, V -0.00060215, COST +0.00003276, AMZN +0.00037562, SPY +0.00063488, RSP +0.00050273. Aggregate is positive but near-flat; constituents split 5 positive / 2 negative. `trend/slope-positive.md`
	3	`r_squared_geq`	`Balance 0.5`	True	medium	Window 2025-05-15 → 2026-05-15, OLS of log(c) vs ordinal day index, per holding (252 bars each):	TREND
Window 2025-05-15 → 2026-05-15, OLS of log(c) vs ordinal day index, per holding (252 bars each): AAPL: R²=0.6889 (wt 7.58%, slope=0.001298) MSFT: R²=0.5175 (wt 7.45%, slope=-0.001058) V: R²=0.6906 (wt 7.59%, slope=-0.000602) COST: R²=0.0025 (wt 7.25%, slope=0.000033) AMZN: R²=0.1488 (wt 3.87%, slope=0.000376) SPY: R²=0.7333 (wt 7.10%, slope=0.000635) RSP: R²=0.8112 (wt 2.83%, slope=0.000503) Weighted-average R² = 0.5133 over 7 holdings (total weight 43.67%, all with sufficient history; no abstentions) 0.5133 >= 0.5 threshold → true, but margin is only +0.0133 `trend/r-squared-geq.md`
	4	`adx_geq`	`Balance 20.0`	True	medium	balance_sample, as_of=2026-05-15, threshold=20.0; 7 equity holdings, all final-row adx14 non-null (no renormalization needed).	TREND
balance_sample, as_of=2026-05-15, threshold=20.0; 7 equity holdings, all final-row adx14 non-null (no renormalization needed). Per-holding adx14 (weight_pct): AAPL 29.5841 (7.58), MSFT 16.2399 (7.45), V 17.8212 (7.59), COST 10.9441 (7.25), AMZN 38.3830 (3.87), SPY 27.5377 (7.10), RSP 13.5068 (2.83). Weighted-average ADX(14) = Σ(w·adx)/Σw = 21.5738 over Σw=43.67. 21.5738 >= 20.0 → true. Five of seven names sit below 20 (MSFT/V/COST/RSP chop), but AAPL/AMZN/SPY pull the weighted mean over the cutoff — a near-knife-edge pass. `trend/adx-geq.md`
DRAWDOWN · OPTIONS-RISK · SECTOR · TREND — 19 of 20 True.

Metrics

frameworkCount: 5
frameworksPresent: 5
runsTotal: 33
runsAccepted: 33
runsRejected: 0
leanGraphEmitFresh: yes
leanGraphEmitRev: 7a619914a
leanGraphModality: direction-conditional-decaying
leanGraphDenominator: 526
leanGraphCoveragePct: 0.02091254752851711
leanGraphVelocity: 0
leanGraphGoldenShare: 0.0019011406844106464
leanGraphAutomatedShare: 0.019011406844106463
leanGraphMeanDeps: 10.222222222222221
leanGraphGeneratedFactShare: 0.15760869565217392
leanGraphToolchainCurrent: yes
latestRunId: balance_sample
latestRunAt: 2026-06-04T17:41:49Z
latestVerdict: ACCEPTED
latestProofGraphUrl: https://qresev.quantapix.com/proof-graph/run/balance_sample/
tradingEncodedSymbols: 10
tradingTierA: withheld — agreement oracle under re-verification, 2026-07-14
tradingTierB: withheld — agreement oracle under re-verification, 2026-07-14
tradingTierC: withheld — agreement oracle under re-verification, 2026-07-14
tradingTierBlindCertified: 0
tradingSectorsTouched: 4
tradingSectorUniverse: 11
tradingSymbolUniverse: 526
tradingUniversePct: 1.9011
tradingWavesTotal: 9
tradingWavesAudited: 7
tradingWavesReadClean: 3
tradingSymbolsAuditable: 9
tradingSymbolsReadClean: 4
tradingTierAReEarned: 0

Agreement-tier figures withdrawn pending re-verification

Frameworks — module readiness

Verifier-run statistics

Verifier runs

Accepted

Rejected

Latest run

Axiomatize-trading program

Symbols encoded

Tier-A

Sectors touched

Of S&P 500 universe

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

Balance

Trend.is_uptrend

smaCross

slope

rSquared

adx

OptionsRisk.is_clean

OptionsRisk.defined_risk_only

noNaked

debitOnly

Sector.no_violations

∀ s, cap_respected

Drawdown.discipline_breached

maxDD

tuw

recovers

Metrics