/-
Copyright (c) 2026 Raphael Coelho. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Raphael Coelho
-/
import MathFin

/-!
# Axiom audit — the "axioms-clean" claim, build-enforced

The library's headline claim is that every `full` derivation is
`#print axioms`-clean: it depends only on the three standard Mathlib
axioms `[propext, Classical.choice, Quot.sound]` — no `sorryAx`, no extra
axioms.

This file turns that claim from a docstring assertion (in `docs/coverage.md`)
into a **build-enforced invariant**. Each `#guard_msgs in #print axioms`
block below pins the axiom dependencies of a headline / load-bearing
theorem. If any audited theorem ever picks up `sorryAx` (a `sorry` slipped
in) or a new axiom (a dependency changed), the `#guard_msgs` check fails and
**the build breaks**.

The audited set spans every area of the library — it is representative, not
exhaustive; extend it when a new load-bearing theorem lands. A theorem that
appears here is certified axioms-clean by `lake build`, not by assertion.

Note: pure-algebra theorems (closed by `ring`/`field_simp`) may legitimately
depend on a *subset* of the three (or none); those are pinned to their
actual set below. The invariant we enforce is "no `sorryAx`, no axiom
outside the standard three", which the pinned messages capture exactly.
-/

namespace MathFin.AxiomAudit

/-! ## Black-Scholes core -/

/-- info: 'MathFin.bs_call_formula' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.bs_call_formula

/-- info: 'MathFin.bsP_eq_bsV' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.bsP_eq_bsV

/-- info: 'MathFin.hasDerivAt_bsV_S' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.hasDerivAt_bsV_S

/-- info: 'MathFin.bs_pde_holds' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.bs_pde_holds

/-- info: 'MathFin.expected_terminal_eq_forward' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.expected_terminal_eq_forward

/-! ## Feynman–Kac → Black–Scholes-PDE keystone -/

/-- info: 'MathFin.FeynmanKacHeatEquation.feynmanU_heat_equation' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.FeynmanKacHeatEquation.feynmanU_heat_equation

/-- info: 'MathFin.bsV_satisfies_bs_pde_via_feynmanKac' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.bsV_satisfies_bs_pde_via_feynmanKac

/-! ## Garman normal form + consumer-side corollaries -/

/-- info: 'MathFin.bsV_eq_bsVGarman_standard' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.bsV_eq_bsVGarman_standard

/-- info: 'MathFin.black_futures_price_eq_bsVGarman' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.black_futures_price_eq_bsVGarman

/-- info: 'MathFin.bs_dividends_price_eq_bsVGarman' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.bs_dividends_price_eq_bsVGarman

/-! ## Gaussian MGF + lognormal moments -/

/-- info: 'MathFin.integral_exp_affine_gaussianPDFReal_univ' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.integral_exp_affine_gaussianPDFReal_univ

/-- info: 'MathFin.nthMoment_terminal' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.nthMoment_terminal

/-- info: 'MathFin.secondMoment_terminal' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.secondMoment_terminal

/-- info: 'MathFin.variance_terminal' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.variance_terminal

/-- info: 'MathFin.bsLogReturn_mean' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.bsLogReturn_mean

/-! ## Exponential-discount principle + the rate-recovery retrofits -/

/-- info: 'MathFin.rate_eq_neg_log_deriv' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.rate_eq_neg_log_deriv

/-- info: 'MathFin.forwardRate_eq_neg_log_discount' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.forwardRate_eq_neg_log_discount

/-- info: 'MathFin.force_eq_neg_log_deriv_survival' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.force_eq_neg_log_deriv_survival

/-- info: 'MathFin.hazard_eq_neg_log_deriv_survival' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.hazard_eq_neg_log_deriv_survival

/-! ## Static Girsanov: the risk-neutral measure derived -/

/-- info: 'MathFin.gaussian_esscher_pdf' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.gaussian_esscher_pdf

/-- info: 'MathFin.gaussianReal_withDensity_esscher' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.gaussianReal_withDensity_esscher

/-- info: 'MathFin.BSCallHyp.exists_of_physical' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.BSCallHyp.exists_of_physical

/-- info: 'MathFin.bsTerminal_physical_eq_riskNeutral' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.bsTerminal_physical_eq_riskNeutral

/-- info: 'MathFin.discounted_terminal_eq_S0_of_physical' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.discounted_terminal_eq_S0_of_physical

/-- info: 'MathFin.bs_call_formula_of_physical' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.bs_call_formula_of_physical

/-- info: 'MathFin.discounted_physical_terminal_eq_S0' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.discounted_physical_terminal_eq_S0

/-! ## Margrabe exchange option (first multivariate result) -/

/-- info: 'MathFin.margrabe_effective_variance' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.margrabe_effective_variance

/-- info: 'MathFin.exchange_payoff_eq_ratio' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.exchange_payoff_eq_ratio

/-- info: 'MathFin.margrabe_eq_bsVGarman' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.margrabe_eq_bsVGarman

/-- info: 'MathFin.margrabe_parity' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.margrabe_parity

/-- info: 'MathFin.margrabe_price_via_call' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.margrabe_price_via_call

/-! ## Convex pricing functional + FTAP / state-price wiring -/

/-- info: 'MathFin.statePricePricing_convexOn' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.statePricePricing_convexOn

/-- info: 'MathFin.callPrice_finiteState_butterfly_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.callPrice_finiteState_butterfly_nonneg

/-- info: 'MathFin.stateprice_call_butterfly_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.stateprice_call_butterfly_nonneg

/-! ## Binomial trees -/

/-- info: 'MathFin.americanCallPrice_le_binomialPrice' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.americanCallPrice_le_binomialPrice

/-! ## Variance swap (QV limit) -/

/-- info: 'MathFin.tendsto_expected_bsLogPrice_equipartition_sum' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.tendsto_expected_bsLogPrice_equipartition_sum

/-! ## L² quadratic variation of Brownian motion (Summit 1) + its in-probability corollary -/

/-- info: 'MathFin.QuadraticVariationL2.tendsto_qv' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.QuadraticVariationL2.tendsto_qv

/-- info: 'MathFin.QuadraticVariationL2.tendstoInMeasure_qv' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.QuadraticVariationL2.tendstoInMeasure_qv

/-- info: 'MathFin.BrownianQuadraticVariation.qv_equals_t' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.BrownianQuadraticVariation.qv_equals_t

/-! ## Expectation-form Itô / Feynman–Kac (the QV → ½f″ correction, from first principles) -/

/-- info: 'MathFin.FeynmanKacHeatEquation.heatConvolution_eq_add_integral_deriv' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
#print axioms MathFin.FeynmanKacHeatEquation.heatConvolution_eq_add_integral_deriv

/-- info: 'MathFin.FeynmanKacHeatEquation.expectation_ito' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.FeynmanKacHeatEquation.expectation_ito

/-- info: 'MathFin.FeynmanKacHeatEquation.expectation_ito_isPreBrownian' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
#print axioms MathFin.FeynmanKacHeatEquation.expectation_ito_isPreBrownian

/-! ## Adapted Itô isometry (increment-independence cornerstone) -/

/-- info: 'MathFin.ItoIsometryAdapted.integral_adapted_mul_increment' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.ItoIsometryAdapted.integral_adapted_mul_increment

/-- info: 'MathFin.ItoIsometryAdapted.integral_adapted_sq_mul_increment_sq' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIsometryAdapted.integral_adapted_sq_mul_increment_sq

/-- info: 'MathFin.ItoIsometryAdapted.ito_isometry_discrete' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.ItoIsometryAdapted.ito_isometry_discrete

/-- info: 'MathFin.ItoIsometryAdapted.ito_isometry_brownian_self' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.ItoIsometryAdapted.ito_isometry_brownian_self

/-- info: 'MathFin.ItoIsometryAdapted.integral_adapted_mul_increment_sq' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIsometryAdapted.integral_adapted_mul_increment_sq

/-- info: 'MathFin.ItoIsometryAdapted.ito_isometry_discrete_bilinear' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIsometryAdapted.ito_isometry_discrete_bilinear

/-! ## Predictable-rectangle pairing (inner-product core of the continuous Itô integral) -/

/-- info: 'MathFin.ItoIsometryAdapted.adapted_indepFun_forward' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIsometryAdapted.adapted_indepFun_forward

/-- info: 'MathFin.ItoIsometryAdapted.integral_two_increment' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIsometryAdapted.integral_two_increment

/-- info: 'MathFin.ItoIsometryAdapted.rect_increment_pairing' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIsometryAdapted.rect_increment_pairing

/-! ## Continuous Itô integral — foundational bridge (AdaptedAt ↔ natural filtration) -/

/-- info: 'MathFin.ItoIntegralL2.adaptedAt_of_measurable_natural' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralL2.adaptedAt_of_measurable_natural

/-! ## Continuous Itô integral as a CLM on `[0,T]` — the headline -/

/-- info: 'MathFin.ItoIntegralCLM.generateFrom_predictableRect' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.ItoIntegralCLM.generateFrom_predictableRect

/-- info: 'MathFin.ItoIntegralCLM.assembly_isometry_T' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.ItoIntegralCLM.assembly_isometry_T

/-- info: 'MathFin.ItoIntegralCLM.simpleAssembly_T_denseRange' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.ItoIntegralCLM.simpleAssembly_T_denseRange

/-- info: 'MathFin.ItoIntegralCLM.itoIntegralCLM_T_norm' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.ItoIntegralCLM.itoIntegralCLM_T_norm

/-! ## Unbounded-horizon `[0,∞)` Itô integral CLM (Summit B / B2) -/

/-- info: 'MathFin.ItoIntegralL2.itoIntegralL2_norm' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.ItoIntegralL2.itoIntegralL2_norm

/-! ## Process-level elementary Itô integral `t ↦ (V●B)_t` — genuine `L²` content -/

/-- info: 'MathFin.ItoIntegralProcess.memLp_itoSimpleProcess' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.ItoIntegralProcess.memLp_itoSimpleProcess

/-- info: 'MathFin.ItoIntegralProcess.itoSimpleProcess_eq_itoSimple' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.ItoIntegralProcess.itoSimpleProcess_eq_itoSimple

/-! ## Keystone `∫₀ᵀ B dB = ½(B_T² − B₀² − T)` through the CLM (its first genuine consumer) -/

/-- info: 'MathFin.ItoIntegralBrownian.itoIntegralCLM_T_brownian' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.ItoIntegralBrownian.itoIntegralCLM_T_brownian

/-! ## Discrete squaring identity (the pathwise Itô keystone) -/

/-- info: 'MathFin.discrete_squaring_identity' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.discrete_squaring_identity

/-! ## Itô's lemma for f(x) = x² — the L² continuous form (the QF-keystone) -/

/-- info: 'MathFin.itoSquared_L2_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.itoSquared_L2_tendsto

/-- info: 'MathFin.itoSquared_L2_tendsto_div2' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.itoSquared_L2_tendsto_div2

/-! ## Itô chain items 3-6: polynomial remainders, 2D Itô, GBM-SDE, BS-PDE -/

/-- info: 'MathFin.discrete_cubing_identity' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.discrete_cubing_identity

/-- info: 'MathFin.discrete_ito_formula_2d' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.discrete_ito_formula_2d

/-- info: 'MathFin.hasDerivAt_gbmValue_space' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.hasDerivAt_gbmValue_space

/-- info: 'MathFin.gbm_solves_sde' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.gbm_solves_sde

/-- info: 'MathFin.bs_pde_eq_itoDrift2D_minus_rV' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.bs_pde_eq_itoDrift2D_minus_rV

/-! ## Margrabe BSCallHyp grounding (leap-3 closure via gaussian vector) -/

/-- info: 'MathFin.normalizedSpread_hasLaw_std' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.normalizedSpread_hasLaw_std

/-- info: 'MathFin.margrabe_bsCallHyp_of_gaussian' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.margrabe_bsCallHyp_of_gaussian

/-- info: 'MathFin.margrabe_price_of_gaussian' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.margrabe_price_of_gaussian

/-! ## Portfolio / risk / performance -/

/-- info: 'MathFin.portfolioVarTwo_ge_min' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.portfolioVarTwo_ge_min

/-- info: 'MathFin.gaussianVaR_translation' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.gaussianVaR_translation

/-- info: 'MathFin.gaussianCVaR_sub_VaR' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.gaussianCVaR_sub_VaR

/-- info: 'MathFin.sharpeRatio_affine_invariant' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in #print axioms MathFin.sharpeRatio_affine_invariant

/-! ## Certified cross-domain bridges -/

/-- info: 'MathFin.portfolioVarN_diag_eq_herfindahl' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.portfolioVarN_diag_eq_herfindahl

/-- info: 'MathFin.survivalFromForce_eq_hazardSurvival' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.survivalFromForce_eq_hazardSurvival

/-- info: 'MathFin.gompertz_cumHazard' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.gompertz_cumHazard

/-! ## CRR → Black–Scholes characteristic-function convergence (the distributional CLT heart) -/

/-- info: 'MathFin.crr_charFun_pow_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.crr_charFun_pow_tendsto

/-- info: 'MathFin.crr_charFun_pow_tendsto_gaussian' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.crr_charFun_pow_tendsto_gaussian

/-- info: 'MathFin.crr_tendsto_gaussian_inDistribution' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.crr_tendsto_gaussian_inDistribution

/-! ## Continuous-time first FTAP (discounted GBM price is a Q-martingale) -/

/-- info: 'MathFin.discountedGBM_isMartingale' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.discountedGBM_isMartingale

/-! ## Binomial pricing as discounted risk-neutral expectation (CRR→BS price bridge) -/

/-- info: 'MathFin.binomialPrice_eq_integral_convPow' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.binomialPrice_eq_integral_convPow

/-! ## CRR → Black–Scholes call-price convergence (the named theorem) -/

/-- info: 'MathFin.binomialPrice_call_tendsto_bs' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.binomialPrice_call_tendsto_bs

/-! ## CRR → Black–Scholes call price in literal closed form `S₀Φ(d₁) − Ke^{−rT}Φ(d₂)` -/

/-- info: 'MathFin.binomialPrice_call_tendsto_bs_closed' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.binomialPrice_call_tendsto_bs_closed

/-! ## Summit A: bounded-derivative continuous-time Itô formula in L² (CLM-identified) -/

/-- info: 'MathFin.tendsto_weighted_qv' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.tendsto_weighted_qv

/-- info: 'MathFin.tendsto_ito_remainder' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.tendsto_ito_remainder

/-- info: 'MathFin.ItoIntegralRiemannBridge.itoIntegralCLM_T_of_bdd_cont' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.ItoIntegralRiemannBridge.itoIntegralCLM_T_of_bdd_cont

/-- info: 'MathFin.ito_formula_L2_bddDeriv' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_L2_bddDeriv

/-! ## Summit A′: time-dependent Itô formula in L² (CLM-identified) -/

/-- info: 'MathFin.tendsto_weighted_qv_process' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.tendsto_weighted_qv_process

/-- info: 'MathFin.tendsto_ito_remainder_td' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.tendsto_ito_remainder_td

/-- info: 'MathFin.ItoIntegralRiemannBridgeTD.itoIntegralCLM_T_of_bdd_cont_td' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.ItoIntegralRiemannBridgeTD.itoIntegralCLM_T_of_bdd_cont_td

/-- info: 'MathFin.ito_formula_td_L2_bddDeriv' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_td_L2_bddDeriv

/-! ## Localized (exponential-growth) time-dependent Itô formula — the rung-3 unlock to GBM -/

/-- info: 'MathFin.pathIntegral_expGrowth_memLp' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.pathIntegral_expGrowth_memLp

/-- info: 'MathFin.ito_formula_td_localized' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_td_localized

/-! ## Itô → pricing bridge: geometric Brownian motion decomposed by the Itô integral

`ItoFormulaGBM.lean`: the **first pricing-ward consumer of the analytic Itô tower** (which
until now had none — GBM/BS pricing ran via separate algebraic towers and the Wald
exponential). The localized formula, applied to the *time-localized* GBM exponent
`(t,x) ↦ S₀ exp((m−σ²/2)·φₙ(t) + σx)` (identity on `[0,T]`, globally bounded so the
exp-growth hypotheses hold uniformly in time), yields `ito_formula_gbm`:
`Ŝ(T) − Ŝ(0) =ᵐ itoIntegralCLM_T gfx + ∫₀ᵀ m·Ŝ ds`. Setting `m = 0`
(`discountedGBM_eq_itoIntegral`) makes the drift vanish — the Itô-integral content of the
discounted-GBM martingale, grounding it on the continuous Itô integral rather than the Wald
exponential. -/

/-- info: 'MathFin.ito_formula_gbm' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_gbm

/-- info: 'MathFin.discountedGBM_eq_itoIntegral' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.discountedGBM_eq_itoIntegral

/-! ## Itô formula against a constant-coefficient Itô process

`ItoFormulaItoProcess.lean`: generalizes the GBM decomposition from the exponential value
function to an arbitrary `C³` exponential-growth `f`. For `X_t = X₀ + b·t + σ B_t`,
`ito_formula_itoProcess` gives `f(X_T) − f(X₀) =ᵐ itoIntegralCLM_T gfx + ∫₀ᵀ (f'(X)·b + ½f''(X)·σ²) ds`
— i.e. `∫ f'(X) dX + ½∫ f''(X)σ² ds`, the diffusion the genuine Itô integral. Same
time-localization of the `b·t` exponent as the GBM case; constant coefficients keep the
diffusion integrand a function of `B`. -/

/-- info: 'MathFin.ito_formula_itoProcess' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_itoProcess

/-! ## The time-dependent Itô formula as a process (semimartingale decomposition)

`ItoFormulaProcess.lean`: lifts the terminal Itô formula (a single fixed-horizon `Lp` statement)
to a process identity holding for **every** `t ≤ T`: `f(t,B_t) − f(0,B_0) =ᵐ itoProcessL2Inf t F +
∫₀ᵗ (f_t + ½f_xx) ds`, the stochastic term the genuine Itô-integral *process* — a continuous `L²`
martingale with an everywhere-continuous local-martingale modification. The witness is canonical
(`ito_formula_td_L2_bddDeriv_explicit` exposes `gfx =ᵐ [f_x(·,B)]`); the construction is the
zero-extension `exists_fullHorizon_extension` fed to the existing `[0,∞)` horizon-consistency. No
Markov property, no PDE — entirely inside the Itô tower. -/

/-- info: 'MathFin.ito_formula_td_L2_bddDeriv_explicit' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_td_L2_bddDeriv_explicit

/-- info: 'MathFin.ito_formula_td_process' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ito_formula_td_process

/-! ## Carr–Madan static replication / spanning formula -/

/-- info: 'MathFin.carrMadan_spanning' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.carrMadan_spanning

/-- info: 'MathFin.carrMadan_log_spanning' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.carrMadan_log_spanning

/-! ## Binomial martingale representation (market completeness) -/

/-- info: 'MathFin.binomial_martingale_representation' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.binomial_martingale_representation

/-! ## Path-1 upgrades (2026-06-04): reduced cores earned to full derivations -/

/-- info: 'MathFin.submartingale_optional_sampling' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.submartingale_optional_sampling

/-- info: 'MathFin.portfolioVarN_covariance_eq_variance' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.portfolioVarN_covariance_eq_variance

/-- info: 'MathFin.gaussianCVaR_isLeast_ruObjective' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.gaussianCVaR_isLeast_ruObjective

/-- info: 'MathFin.survival_probability_eq_Phi_distanceToDefault' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.survival_probability_eq_Phi_distanceToDefault

/-- info: 'MathFin.newtonStep_quadratic_error' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.newtonStep_quadratic_error

/-- info: 'MathFin.newtonSeq_tendsto_root' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.newtonSeq_tendsto_root

/-- info: 'MathFin.snellAux_le_of_supermartingale_of_ge' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.snellAux_le_of_supermartingale_of_ge

/-- info: 'MathFin.snellAux_eq_discounted_americanPrice' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.snellAux_eq_discounted_americanPrice

/-- info: 'MathFin.discounted_americanPrice_supermartingale' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.discounted_americanPrice_supermartingale

/-- info: 'MathFin.discounted_intrinsic_le_americanPrice' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.discounted_intrinsic_le_americanPrice

-- Poisson-process theory + Itô-process QV (2026-06-05 full-push round)

/-- info: 'MathFin.PoissonSuperposition.poissonMeasure_conv_poissonMeasure' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.PoissonSuperposition.poissonMeasure_conv_poissonMeasure

/-- info: 'MathFin.PoissonSuperposition.indepFun_map_add_poissonMeasure' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.PoissonSuperposition.indepFun_map_add_poissonMeasure

/-- info: 'MathFin.PoissonThinning.markedPoissonMeasure_eq_prod' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.PoissonThinning.markedPoissonMeasure_eq_prod

/-- info: 'MathFin.PoissonThinning.thinned_streams' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.PoissonThinning.thinned_streams

/-- info: 'MathFin.PoissonCounting.map_count_eq_poissonMeasure' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.PoissonCounting.map_count_eq_poissonMeasure

/-- info: 'MathFin.PoissonInterarrival.map_firstArrival_eq_expMeasure' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.PoissonInterarrival.map_firstArrival_eq_expMeasure

/-- info: 'MathFin.PoissonInterarrival.survival_factorizes' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.PoissonInterarrival.survival_factorizes

/-- info: 'MathFin.ItoProcessQV.tendsto_qv_ito_process' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.ItoProcessQV.tendsto_qv_ito_process

-- Finance layer over the Poisson/QV track (2026-06-06): variance-swap drift
-- immunity, first-to-default additivity, Poisson pgf, Merton jump-diffusion

/-- info: 'MathFin.tendsto_realizedVariance_gbm_L2' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.tendsto_realizedVariance_gbm_L2

/-- info: 'MathFin.firstToDefault_spread_eq_sum_hazards' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.firstToDefault_spread_eq_sum_hazards

/-- info: 'MathFin.PoissonPgf.integral_pow_poissonMeasure' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in
  #print axioms MathFin.PoissonPgf.integral_pow_poissonMeasure

/-- info: 'MathFin.mertonCallTerm_eq_integral' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.mertonCallTerm_eq_integral

/-- info: 'MathFin.integral_mertonSpot' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.integral_mertonSpot

/-- info: 'MathFin.merton_put_call_parity' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.merton_put_call_parity

-- Merton dominance + classic display; Markov path law (2026-06-06): jump
-- risk is never free (spot convexity + compensation identity), the
-- Λ′ = Λ(1+k) textbook display (rate-shift identity), and Saporito 1.1.2
-- derived from the pin's Ionescu–Tulcea trajectory kernels

/-- info: 'MathFin.bsV_spot_convexOn' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.bsV_spot_convexOn

/-- info: 'MathFin.bsV_le_mertonCallPrice' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.bsV_le_mertonCallPrice

/-- info: 'MathFin.mertonCallPrice_eq_classic_tsum' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.mertonCallPrice_eq_classic_tsum

/-- info: 'MathFin.markovPathMeasure_cylinder' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.markovPathMeasure_cylinder

-- Blueprint-spine closure (2026-06-06): every spine node is axiom-pinned.
-- Gap found by tests/test_values.py::test_blueprint_spine_is_audited on its
-- first run — seven tagged headliners (including bs_identity, the magic
-- identity itself) had no guard.

/-- info: 'MathFin.WienerIntegralL2.wiener_assembly_isometry' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.WienerIntegralL2.wiener_assembly_isometry

/-- info: 'MathFin.ItoIntegralCLM.itoIntegralCLM_T' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralCLM.itoIntegralCLM_T

/-- info: 'MathFin.discrete_ito_formula' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.discrete_ito_formula

/-- info: 'MathFin.hasLaw_esscher_tilt' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.hasLaw_esscher_tilt

/-- info: 'MathFin.BSCallHyp.of_isPreBrownian' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.BSCallHyp.of_isPreBrownian

/-- info: 'MathFin.bs_identity' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.bs_identity

/-- info: 'MathFin.bs_pde_from_no_arbitrage' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.bs_pde_from_no_arbitrage

-- Values round 6 (2026-06-09): Andre's reflection-principle counting
-- bijection (Binomial/PathReflection.lean), wired to the corpus as
-- `mf-reflection-principle-counting`.

/-- info: 'MathFin.reflectionPrincipleEquiv_below' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.reflectionPrincipleEquiv_below

-- Summit B / B1a (2026-06-10): the elementary Itô integral, viewed as a process
-- `t ↦ (V●B)_t`, is an adapted L² martingale
-- (Foundations/ItoIntegralProcessMartingale.lean). Infrastructure for the
-- gated Girsanov/Lévy/martingale-representation/SDE cluster; no corpus entry
-- yet (the `full` entry lands with B1b, the general integrand).

/-- info: 'MathFin.ItoIntegralProcess.itoSimpleProcess_adaptedAt' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.itoSimpleProcess_adaptedAt

/-- info: 'MathFin.ItoIntegralProcess.condExp_adapted_mul_increment' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.condExp_adapted_mul_increment

/-- info: 'MathFin.ItoIntegralProcess.itoSimpleProcess_isMartingale' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.itoSimpleProcess_isMartingale

/-- info: 'MathFin.ItoIntegralProcess.itoSimpleProcess_isometry_time' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.itoSimpleProcess_isometry_time

/-- info: 'MathFin.ItoIntegralProcess.itoSimpleProcessLp_l2_continuous' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.itoSimpleProcessLp_l2_continuous

-- Summit B / B3 (2026-06-13): the elementary Itô integral as a continuous LOCAL
-- MARTINGALE — pathwise continuity (given continuous Brownian paths) + Degenne's
-- `Martingale.IsLocalMartingale` (`Foundations/ItoIntegralProcessLocalMartingale.lean`).
-- The localization entry point; consumes the upstream local-martingale class.

/-- info: 'MathFin.ItoIntegralProcess.itoSimpleProcess_pathContinuous' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.itoSimpleProcess_pathContinuous

/-- info: 'MathFin.ItoIntegralProcess.itoSimpleProcess_isLocalMartingale' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcess.itoSimpleProcess_isLocalMartingale

-- Summit B / B1b (2026-06-12): the GENERAL-integrand Itô integral
-- `(φ●B)_t = ∫₀ᵗ φ dB` for `φ ∈ L2Predictable[0,T]`, built by extending B1a's
-- t-process along the dense `simpleAssembly_T` (`Foundations/ItoIntegralProcessGeneral.lean`).
-- The key identity `(φ●B)_t = E[∫₀ᵀ φ dB | 𝓕_t]` gives the L² martingale property,
-- a.e.-adaptedness, the contraction and terminal Itô isometry, and L²-continuity.
-- The explicit time-indexed isometry E[(φ●B)_t²] = ∫₀ᵗ E[φ²] ds is deferred.

/-- info: 'MathFin.ItoIntegralProcessGeneral.itoProcessCLM_eq_condExpL2' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessGeneral.itoProcessCLM_eq_condExpL2

/-- info: 'MathFin.ItoIntegralProcessGeneral.itoIntegralProcessGen_isMartingale' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessGeneral.itoIntegralProcessGen_isMartingale

/-- info: 'MathFin.ItoIntegralProcessGeneral.itoProcessCLM_aeStronglyMeasurable' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessGeneral.itoProcessCLM_aeStronglyMeasurable

/-- info: 'MathFin.ItoIntegralProcessGeneral.itoProcessCLM_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessGeneral.itoProcessCLM_norm_le

/-- info: 'MathFin.ItoIntegralProcessGeneral.itoProcessCLM_norm_terminal' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessGeneral.itoProcessCLM_norm_terminal

/-- info: 'MathFin.ItoIntegralProcessGeneral.itoIntegralProcessGen_l2_continuous' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessGeneral.itoIntegralProcessGen_l2_continuous

-- The deferred per-`t` Itô isometry `E[(φ●B)_t²] = ∫_{(0,t]×Ω} φ²`
-- (`Foundations/ItoIntegralProcessIsometry.lean`), proved by density-transferring the
-- band-restricted simple-process isometry against the band-truncation CLM.
/-- info: 'MathFin.ItoIntegralProcessGeneral.itoProcessCLM_norm_sq' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessGeneral.itoProcessCLM_norm_sq

-- Covariation of Itô integrals (2026-06-23): the BILINEAR Itô isometry. The Itô
-- integral, bundled as a `LinearIsometry` (`itoIsometry_T`), preserves the
-- L²-inner product (`LinearIsometry.inner_map_map`, polarization of the norm
-- isometry), giving `𝔼[(∫φ dB)(∫ψ dB)] = ⟪φ, ψ⟫` and, on the diagonal, the Itô
-- isometry itself (`Foundations/ItoIntegralCovariation.lean`). The bilinear
-- completion of B1 and the covariance backbone for covariance-swap pricing.

/-- info: 'MathFin.ItoIntegralCovariation.itoIsometry_T' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralCovariation.itoIsometry_T

/-- info: 'MathFin.ItoIntegralCovariation.inner_itoIntegralCLM_T' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralCovariation.inner_itoIntegralCLM_T

/-- info: 'MathFin.ItoIntegralCovariation.covariation_itoIntegralCLM_T' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralCovariation.covariation_itoIntegralCLM_T

/-- info: 'MathFin.ItoIntegralCovariation.variance_itoIntegralCLM_T' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralCovariation.variance_itoIntegralCLM_T

-- Continuous modification of the general-integrand Itô process (2026-06-26): the
-- first PATHWISE-regularity result for the general integrand and the tower→pricing
-- gate. Simple approximants `Vₙ ● B` (B3-continuous) are a.s.-uniformly Cauchy on
-- `[0,T]` (Doob's continuous-time maximal inequality + Borel–Cantelli on a fast
-- subsequence), so their uniform limit `itoContinuousMod` is pathwise continuous,
-- equals the L² process `itoProcessCLM T t φ` a.e. at every `t ≤ T` (a modification,
-- via `tendstoInMeasure_ae_unique`), and is bundled by `exists_continuous_modification_itoProcess`
-- (`Foundations/ItoIntegralProcessContinuousModification.lean`). Non-redundant: Degenne's
-- general càdlàg modification is `sorry`-backed, and this L²+Doob route yields a
-- genuinely continuous (not merely càdlàg) version.

/-- info: 'MathFin.ItoIntegralProcessContinuousModification.itoContinuousMod_modification' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessContinuousModification.itoContinuousMod_modification

/-- info: 'MathFin.ItoIntegralProcessContinuousModification.itoContinuousMod_continuousOn' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessContinuousModification.itoContinuousMod_continuousOn

/-- info: 'MathFin.ItoIntegralProcessContinuousModification.exists_continuous_modification_itoProcess' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessContinuousModification.exists_continuous_modification_itoProcess

-- The IsLocalMartingale follow-on (`Foundations/ItoIntegralProcessLocalMartingaleGeneral.lean`):
-- the everywhere-continuous representative of the modification, adapted to the
-- NULL-AUGMENTED Brownian filtration `𝓕ᴮ ⊔ 𝓝`, is a genuine `IsLocalMartingale`.
-- The measure-theoretic heart is `condExp_sup_nulls` — conditioning on the null
-- augmentation agrees a.e. with conditioning on `𝓕ᴮ` (proved via the σ-algebra crux
-- `exists_ae_eq_of_sup_nulls`), which transfers the L² martingale property to the
-- a.e.-defined modification while repairing it into an everywhere-continuous adapted
-- process — the `∀ ω, IsCadlag` hypothesis of Degenne's `Martingale.IsLocalMartingale`.
/-- info: 'MathFin.ItoIntegralProcessLocalMartingaleGeneral.exists_continuous_localMartingale_modification' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoIntegralProcessLocalMartingaleGeneral.exists_continuous_localMartingale_modification

-- The [0,∞) crown (`Foundations/ItoIntegralProcessLocalMartingaleInfinite.lean`): the per-horizon
-- continuous local martingales are glued — horizon consistency (`itoProcessL2Inf_eq_itoProcessCLM`,
-- itself resting on the `[0,T]` `SimpleProcess` clamp) makes each a modification of the SAME
-- unbounded-horizon process, and `indistinguishable_of_modification_on` agrees them on overlaps —
-- into a single everywhere-continuous local martingale on the WHOLE half-line, whose martingale
-- property is the GLOBAL `itoProcessL2Inf_isMartingale` through `condExp_sup_nulls` (no horizon clamp).
/-- info: 'MathFin.ItoLocalMartingaleInfinite.exists_continuous_localMartingale_modification_infinite' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ItoLocalMartingaleInfinite.exists_continuous_localMartingale_modification_infinite

/-! ## Finite-Ω Fundamental Theorem of Asset Pricing (Harrison–Pliska, 2026-06-25) -/

-- The separating-dual kernel (`Foundations/ConvexSeparation.lean`): a finite-dim
-- subspace disjoint from the standard simplex admits a strictly-positive
-- annihilating dual (finite-dimensional geometric Hahn–Banach). The geometric
-- core shared by the single- and multi-period FTAP backward directions.
/-- info: 'MathFin.exists_pos_dual_of_disjoint_stdSimplex' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.exists_pos_dual_of_disjoint_stdSimplex

-- Multi-state single-period FTAP, now a biconditional (`FTAPMultiState.lean`):
-- the backward direction (no arbitrage ⟹ EMM) via the separating-dual kernel.
/-- info: 'MathFin.hasEMM_multi_iff_not_hasArbitrage' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.hasEMM_multi_iff_not_hasArbitrage

-- Finite-Ω multi-period FTAP (`FTAPDiscrete.lean`): NoArbitrage ⟺ ∃ EMM, the
-- finite case of Dalang–Morton–Willinger. Backward via global separation of the
-- attainable-gains subspace from the simplex; forward via transform telescoping.
/-- info: 'MathFin.ftap_discrete' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.ftap_discrete

-- General-Ω one-period FTAP (`FTAPOnePeriod.lean`): NoArbitrage ⟺ ∃ EMM for a
-- scalar L⁰ return on an arbitrary probability space (Föllmer–Schied 1.55 /
-- one-period DMW). Backward via the bounded-density reduction to L¹, the scalar
-- no-arbitrage dichotomy, and the two-region balancing `withDensity` — no
-- Hahn–Banach, no Kreps–Yan.
/-- info: 'MathFin.OnePeriod.ftap_one_period' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.OnePeriod.ftap_one_period

-- General-Ω one-period FTAP, d assets (`FTAPOnePeriodVector.lean`): NoArbitrage ⟺ ∃ EMM
-- for a non-redundant ℝᵈ-valued L⁰ return on an arbitrary probability space. Backward via
-- the explicit Esscher / minimal-divergence density z = σ⟪θ₀,Y⟫ minimising the softplus
-- potential — no Hahn–Banach, no L⁰-cone closedness, no measurable selection.
/-- info: 'MathFin.OnePeriodVector.ftap_one_period_vector' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.OnePeriodVector.ftap_one_period_vector

/-! ## Itô → pricing bridge: the deterministic-integrand Wiener integral is Gaussian

`WienerIntegralGaussian.lean`: a deterministic-integrand Itô integral
`∫ f dB` is `gaussianReal 0 ‖f‖²` (charFun route: simple-process Gaussianity +
density + Lévy / `Measure.ext_of_charFun`). Its first pricing consumer is the
Vasicek terminal law (`VasicekSDEGaussian.lean`): the SDE solution
`r_T = mean + σ ∫₀ᵀ e^{−κ(T−s)} dB_s` has the posited law `N(mean, σ²(1−e^{−2κT})/(2κ))`,
**derived** rather than assumed — the first Itô-tower consumer in FixedIncome. -/

/-- info: 'MathFin.WienerIntegralL2.wienerIntegralLp_map_eq_gaussianReal' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.WienerIntegralL2.wienerIntegralLp_map_eq_gaussianReal

/-- info: 'MathFin.vasicekShortRate_hasLaw_gaussian' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs (whitespace := lax) in #print axioms MathFin.vasicekShortRate_hasLaw_gaussian

end MathFin.AxiomAudit
