Proven formulas (experimental)

If a trust-weight matrix is strictly diagonally dominant, every eigenvalue is bounded away from 0, so the matrix is non-degenerate (no zero-eigenvalue collapse).

What it adds to governance gate — matrix-health pre-flight (RUN before aggregating): Real pre-aggregation safety gate: certifies the trust-weight matrix is invertible before a trust update, preventing a degenerate (collapsing) aggregation.

Source: Gershgorin circle theorem (1931); Mathlib Matrix.Spectrum ↗ · Lutar/Wave9/Gershgorin.lean ↗

#print axioms ⟶ 'no_zero_eigenvalue' / 'nonsingular_of_strict_diag_dominant' / 'isUnit_det_of_strict_diag_dominant' depends on axioms: [propext, Classical.choice, Quot.sound]

Merkle root binding, inclusion-proof soundness, and append-only are proven by structural induction — an inclusion proof cannot lie about membership and the log cannot be silently rewritten.

What it adds to receipts / audit — backs the inclusion-proof + tamper-evidence story: Formal backing for the signed-receipt hash-chain: inclusion proofs are sound and the log is append-only, so receipts are tamper-evident.

Source: RFC 6962 (Certificate Transparency); arXiv:2303.04500 ↗ · Lutar/Wave9/Merkle.lean ↗

#print axioms ⟶ 'merkle_root_binding' / 'merkle_inclusion_sound' / 'merkle_append_only' depends on axioms: [propext]

A nonnegative (super)martingale wealth process crosses 1/α with probability ≤ α at ANY time — so operators can stop/alarm at any moment with valid coverage, no fixed sample size required.

⚠ Fixed-time Ville is PROVEN; the full sup-over-all-time form is an explicitly-labeled in-file ROADMAP.

What it adds to audit / trust-gate — live 'anytime alarm' (RUN the wealth path): Continuous monitoring with a time-uniform risk bound: alarm the instant evidence crosses threshold — more efficient and safer than fixed-n testing.

Source: Ville (1939); arXiv:2009.03167 ↗ · Lutar/Wave9/Ville.lean ↗

#print axioms ⟶ 'Supermartingale.expectation_le_one' / 'ville_markov_bound' / 'ville_fixed_time' depends on axioms: [propext, Classical.choice, Quot.sound]

Controlled (governed) declassification preserves non-interference: an attacker cannot influence which secret bits get released through the policy channel.

What it adds to P3 / non-interference governance card: Governance soundness: secrets are disclosed only via governed channels, never leaked by attacker influence — backs the controlled-release story.

Source: Nonmalleable Information Flow, CCS 2017; arXiv:1708.08596 ↗ · Lutar/Wave9/RobustDeclass.lean ↗

#print axioms ⟶ 'noninterference_of_robust' / 'released_facts_attacker_invariant' depends on axioms: [] ; 'robust_declass_sound' depends on axioms: [propext, Classical.choice, Quot.sound]

A time-uniform generalization (confidence) envelope for model routing, assembled from the proven Ville fixed-time corollary.

⚠ PARTIAL-core: the Ville-assembled confidence envelope is proven; the full Donsker–Varadhan variational identity + sup-over-time packaging are explicitly-labeled ROADMAP.

What it adds to routing-envelope card (governance gateway): An anytime generalization bound so model-routing trust gates stay sound under continual operation (ROADMAP parts labeled honestly).

Source: Chugg–Wang–Ramdas, unified recipe for (time-uniform) PAC-Bayes; arXiv:2302.03421 ↗ · Lutar/Wave9/TimeUniformPACBayes.lean ↗

#print axioms ⟶ 'pac_bayes_confidence' / 'pac_bayes_risk_envelope' depends on axioms: [propext, Classical.choice, Quot.sound]

If every read quorum intersects every write quorum (read_q + write_q > n) then no two quorums decide differently — agreement safety with flexible quorum sizing.

What it adds to mesh / consensus card (RUN the intersection check): Flexible quorum sizing: pick fast small read quorums + larger write quorums while keeping agreement safety — efficient consensus tuning.

Source: Lamport, Part-Time Parliament (Paxos) 1998; Howard et al., Flexible Paxos, OPODIS 2016 ↗ · Lutar/Wave10/QuorumIntersection.lean ↗

#print axioms ⟶ 'quorum_intersection_agreement' / 'quorum_unique_decision' does not depend on any axioms ; 'majority_quorums_intersect' depends on axioms: [propext, Quot.sound]

Under a PRF-injective hypothesis, distinct keywords map to distinct search tokens — so an encrypted-search result set is sound w.r.t. the queried keyword.

What it adds to a11oy Code SBOM / search integrity card (RUN the injectivity check): Search integrity for the encrypted SBOM index: no token collisions ⇒ results are sound for the queried keyword.

Source: Kamara & Papamanthou, Parallel and Dynamic Searchable Symmetric Encryption, CCS 2012/FC 2013 ↗ · Lutar/Wave10/DSSEToken.lean ↗

#print axioms ⟶ 'dsse_token_injective' / 'dsse_token_distinct' / 'dsse_search_sound' does not depend on any axioms

Non-interference is preserved under identity, sequential composition, fold/iteration, chaining, and pairing — secure components compose into secure systems.

What it adds to P3 / non-interference governance card: Compositional governance soundness: chaining governed steps preserves non-interference, so the pipeline as a whole stays leak-free.

Source: Goguen & Meseguer, IEEE S&P 1982; Mantel MAKS, IEEE S&P 2002 ↗ · Lutar/Wave10/NonInterferenceComposition.lean ↗

#print axioms ⟶ 'ni_id' / 'ni_comp' does not depend on any axioms ; 'ni_foldl' / 'ni_chain' / 'ni_pair' depends on axioms: [propext]

Replaying the same audit log yields the same final state (deterministic), and the first divergence pinpoints any altered entry — so audits are re-verifiable and tamper is localized.

What it adds to audit / replay card (RUN deterministic replay + tamper-localize): Backs the 're-verifiable' claim: an auditor re-runs the log and gets the identical state; any single altered entry is pinpointed exactly.

Source: Schneider, State Machine Approach, ACM CS 1990; Lamport, Time/Clocks, CACM 1978 ↗ · Lutar/Wave10/ReplayDeterminism.lean ↗

#print axioms ⟶ 'replay_deterministic' / 'replay_congr' / 'tamper_localized' does not depend on any axioms ; 'replay_append' depends on axioms: [propext, Quot.sound]

A runtime monitor that returns not just pass/fail but a signed margin ρ — how far the signal is from violating the rule. A satisfied trace guarantees ρ≥0, and ρ>0 guarantees satisfaction.

⚠ Two-sided bound (Sat⇒ρ≥0, ρ>0⇒Sat, ρ<0⇒¬Sat) is PROVEN; the naive iff Sat↔ρ>0 is FALSE at the ρ=0 boundary and is NOT claimed.

What it adds to sensor-fusion / monitor card (RUN the robustness margin): Quantitative runtime monitoring: a signed margin tells operators how close a track/sensor signal is to breaching its bound — actionable headroom, not just a boolean.

Source: Donzé & Maler, Robust Satisfaction of Temporal Logic over Real-Valued Signals, FORMATS 2010 ↗ · Lutar/Wave10/STLRobustness.lean ↗

#print axioms ⟶ 'STL.rho_sound' / 'STL.rho_pos_sound' / 'STL.rho_neg_violation' depends on axioms: [propext, Quot.sound]

Fuse two sensors observing the same target even when you do NOT know how their errors are correlated. The fused covariance is always a valid, never-overconfident uncertainty ellipse.

⚠ PROVEN core = PSD convex closure of the information form (ci_information_psd). Full inverted-covariance Loewner monotonicity is a labelled ROADMAP, not claimed.

What it adds to sensor-fusion card (RUN the conservative fusion): Safe multi-sensor fusion with less bookkeeping: combine estimates with unknown cross-correlation and still get a provably valid, conservative track uncertainty.

Source: Julier & Uhlmann, A Non-divergent Estimation Algorithm (Covariance Intersection), ACC 1997 ↗ · Lutar/Wave9/CovarianceIntersection.lean ↗

#print axioms ⟶ 'posSemidef_convex_comb' / 'ci_information_psd' depends on axioms: [propext, Classical.choice, Quot.sound]

With k edge-disjoint routes between two nodes, the path survives ANY k−1 broken links — and the min-cut tells you exactly how many failures the mesh can take. Fail-safe routing, not a hope.

⚠ MR-1 reachability halves + Menger's two directly-formalizable halves are PROVEN; the full min-max Menger equality is a labelled ROADMAP.

What it adds to mesh / tactical-routing card (RUN the survival proof): Provable mesh resilience: compute the redundancy k, then prove the route still connects after removing the worst k−1 links — fail-safe routing with a number behind it.

Source: Menger (1927); CLRS 3e Ch.26 (max-flow/min-cut); Mathlib SimpleGraph.Path ↗ · Lutar/Wave10/ReachabilityRedundancy.lean ↗

#print axioms ⟶ 'reach_mono' / 'cut_disconnects' / 'path_refutes_cut' depends on axioms: (none) ; 'disjoint_paths_le_cut' depends on axioms: [propext, Classical.choice, Quot.sound]