Spaces:

SZLHOLDINGS
/

a11oy

Running

App Files Files Community

a11oy / corpus /formulas /lutar-lean__PROVEN_FORMULAS.md

betterwithage

fix(org-rag): in-image corpus mirror for GitHub-only categories (egress fix)

545c5f9 verified 2 months ago

preview code

Raw

History Blame

19 kB

Proven Formulas — the honest showcase

One rule governs this page: we list only what the Lean kernel checks, with the exact maturity of each result and a link to its proof. The locked proven set is exactly five formulas — a fact itself machine-enforced by Lutar.Wave8.AxiomDisclosure.locked_count_five (depends on no axioms). On top of that locked floor, ~36 experimental theorems are kernel-verified and CI-green on main @ 7885fd9 (waves 5/6/7/8 + agentic P1–P6 + airtight Λ + coder). Everything newer than the locked 5 is experimental / CI-green and is never folded into the locked count. Λ-uniqueness is Conjecture 1 — proven only conditionally, machine-checked false unconditionally.

Locked-kernel toolchain: Lean v4.13.0 · Mathlib pinned d7317655 (v4.13.0) Locked kernel: c7c0ba17 · 749 declarations / 14 unique axioms / 163 tracked sorries · lake build clean Experimental scope (current main): 7885fd9 · Lean v4.18.0 · 1304 declarations / 22 unique axioms · CI-green, kernel-verified (NOT in the locked count) Maturity legend: PROVEN = sorry-free, Lean-core axioms only [propext, Classical.choice, Quot.sound] · AXIOM-GATED = sorry-free given a declared, cited idealization · CI-GREEN(MD) = Mathlib-dependent, kernel-checked by CI · COND. = conditional on a declared axiom · CONJECTURE = not a theorem

1. Locked kernel — proven, sorry-free (exactly 5)

These five are the only formulas counted as proven in the locked Doctrine-v11 kernel c7c0ba17. Source: Lutar/Puriq/Formulas/PuriqFormulaLean.lean.

ID	Theorem	What it proves	Maturity	`#print axioms`
F1	Replay-Hash Determinism (`f1_replay_fold_deterministic`, `f1_replay_fold_eq_trace_last`)	A pure deterministic replay step is a congruence: replaying the same recorded log from the same initial state yields a bit-identical trace — no drift. Underpins the Khipu replay-hash gate.	PROVEN	Lean-core only
F11	Ayni Reciprocity Conservation (`f11_ayni_reciprocity_conservation`, `f11_tit_for_tat_parity`)	Fold-replay of an append-only reciprocity log conserves the balance invariant (Axelrod–Hamilton tit-for-tat parity).	PROVEN	Lean-core only
F12	Kuramoto Phase-Coupling Boundedness — additive fragment (`f12_*`)	The discretised reciprocity coupling stays bounded under additive superposition over an organ set. Honesty caveat: additive scaffolding ONLY — NOT the full nonlinear Kuramoto synchronization.	PROVEN (additive fragment)	Lean-core only
F18	Reed–Solomon `RS(10,6)` Recovery Arithmetic (`f18_*`)	Erasure tolerance: data is recoverable iff at least 6 of 10 shards survive — the resilience arithmetic for the receipt/payload encoding.	PROVEN	Lean-core only
F19	Bekenstein Additive Scaffolding (`f19_*`)	Entropy budget is additive and monotone over a region partition (per-region ≤ total). Honesty caveat: monotone scaffolding ONLY — NOT the full Bekenstein bound `S ≤ 2πkRE/(ℏc)`.	PROVEN (additive fragment)	Lean-core only

F12 and F19 prove only the additive / linear fragment — never described as "Kuramoto synchronization proved" or "Bekenstein bound proved." The Lean docstrings carry the caveat verbatim.

2. Experimental, kernel-verified (CI-green) — labeled experimental, NOT in the locked 5

Every campaign below is kernel-checked by lutar-lean CI but lives in the experimental scope — it does not move the locked count of 5 and does not change Λ's Conjecture-1 status. Cite the PR for the green head SHA and #print axioms cleanliness.

Campaign	PR	CI-green head	Count	Axiom posture
Agentic loop P1–P6 — the governed RAG→MCP→kernel→receipt loop proven as a system	#188	`2ede47a2`	28 theorems	14 axiom-free; P5 axiom-gated on `hashFn_collision_resistant` (NIST FIPS 180-4)
Wave-5 — AM–GM, Cauchy–Schwarz, conformal coverage, receipt-collision pigeonhole, optional-stopping	#186	`b71114cf`	11	0 new axioms (6 Mathlib-dep CI-green + 5 bare-lean)
Wave-6 — graph substrate: Λ-graph iso-invariance, GNN≤1-WL ceiling, spectral contraction, DAG termination	#189	`dc7ae26d`	11	0 new axioms
Wave-7 — conformal rank-count/p-value, Doob two-sided audit envelope, PAC-Bayes routing envelope, degree-sum iso-invariance	#190	`d6a232ba`	10	0 new axioms
Mathlib-bump C3/C4/C5 — concentration / KL re-exports	#187	—	3	re-exports, CI-green
Coder formulas — code-substrate formula ports	#193	—	—	CI-green
Λ-uniqueness (Set α + Set δ) — airtight Λ — conditional uniqueness within strengthened axiom classes	#192	`5f0bb5ee`	22 results	`lambda_unique_setAlpha` uses Lean-core axioms only; 10 impostor-deaths axiom-free
Wave-8 — disclosure-soundness, hash-chain tamper-evidence, split-conformal coverage, CPA minimality, Simplex switching safety, Byzantine `n=3f+1`, min-gate uniqueness, density-matrix PSD, governance spectral, Λ strict monotonicity	lutar-lean@main	`7885fd9`	10 theorems	core axioms `[propext, Classical.choice, Quot.sound]` (M2 just `[propext]`); `0 sorryAx`

2.1 Agentic-loop P1–P6 (PR #188 @ `2ede47a2`) — the system-level proof

Property	Guarantee	Maturity
P1 receipt-completeness	every hop leaves exactly one chained receipt; no silent drop/reorder	PROVEN
P2 gate-soundness	Emit ALLOW ⇔ both policy gate and kernel gate ALLOW; DENY absorbing	PROVEN
P3 non-interference (Goguen–Meseguer)	poisoned/untrusted retrieval provably cannot flip a DENY→ALLOW	PROVEN (axiom-free core)
P4 replay-determinism	re-running a recorded run reproduces a byte-identical receipt chain	PROVEN (axiom-free)
P5 tamper-evidence	any single-receipt mutation makes re-verify reject	AXIOM-GATED (`hashFn_collision_resistant`, disclosed)
P6 monotone auditability	an accepted prefix never has to be retracted as the log grows	PROVEN

2.2 Wave-8 (10 theorems, `main` @ `7885fd9`) — with benefit + `#print axioms`

All Wave-8 theorems are kernel-verified and CI-green; they are experimental and do not move the locked count of 5. Core axioms are [propext, Classical.choice, Quot.sound] unless noted; 0 sorryAx across the set.

ID	Theorem	Benefit	`#print axioms`
Ph1	`disclosure_sound`	Axiom-honesty gate — the disclosure of a declaration's axioms is sound (you cannot under-report what a theorem depends on).	`[propext, Classical.choice, Quot.sound]`
M2	`hashchain_tamper_evident`	Cannonico tamper-evidence — any mutation of a hash-chained receipt is detectable.	`[propext]` only
CP1	split-conformal marginal coverage	Trust intervals with a distribution-free marginal-coverage guarantee — split-conformal, NOT* Hoeffding*.	`[propext, Classical.choice, Quot.sound]`
G1	CPA minimality (collision)	Minimal collision/abuse surface for the canonical-receipt scheme.	`[propext, Classical.choice, Quot.sound]`
S2	Simplex switching safety	Safe fallback switching between a complex and a verified-baseline controller.	`[propext, Classical.choice, Quot.sound]`
B1	Byzantine `n = 3f+1`	Quorum safety bound underpinning the 3-of-4 witness consensus.	`[propext, Classical.choice, Quot.sound]`
L2	min-gate deny-by-default uniqueness	The deny-by-default min-gate is the unique aggregator with that safety property.	`[propext, Classical.choice, Quot.sound]`
Q1	density-matrix PSD	Governance state stays a valid (positive-semidefinite) density matrix.	`[propext, Classical.choice, Quot.sound]`
Q2	governance spectral (real)	Governance operator has real spectrum — well-posed scoring.	`[propext, Classical.choice, Quot.sound]`
L3	Λ strict monotonicity	Λ is strictly monotone per axis — more evidence never lowers the score spuriously.	`[propext, Classical.choice, Quot.sound]`

Wave-8 is experimental. It does not change the locked count of 5 and does not change Λ's Conjecture-1 status. The locked-count-five fact itself is a Wave-8 theorem (Lutar.Wave8.AxiomDisclosure.locked_count_five) that depends on no axioms — the locked set cannot silently grow.

3. Λ — the honest line on uniqueness (Conjecture 1)

Λ is the geometric-mean trust aggregator over four axes (provenance, containment, coherence, convergence). Its uniqueness is Conjecture 1 — and this page states exactly what was proven and what was not. Source: Lutar/Wave6/SetAlphaUniqueness.lean + SetDeltaUniqueness.lean, PR #192 @ 5f0bb5ee.

What we proved (CI-green)

Uniqueness within Set α = {A1 symmetry, A2 idempotency, A3 all-strict monotonicity, A4 continuity, A5′ multiplicativity} — lambda_unique_setAlpha, conditional on one declared, cited bridge axiom setAlpha_cauchy.
Uniqueness within Set δ = {δ1 reflexivity, δ2 symmetry, δ3 bisymmetry, δ4 per-argument strict monotonicity, δ5′ multiplicativity} — geomMean_unique_KS, continuity derived for free via Kiss–Shulman (2026), conditional on two declared, cited bridge axioms KS_theorem_1_1 + setDelta_stage2.
Λ-membership and all ten impostor-deaths are AXIOM-FREE (Lean-core only, no sorryAx): AM, HM, PM², max, min each fail A5′ (Set α) or δ4-PSI/δ5′ (Set δ) at a concrete witness — so the discriminator is genuine.

`#print axioms` — verbatim from the SUCCESS build log @ `5f0bb5ee`

'Lutar.Wave6.SetAlpha.lambda_unique_setAlpha' depends on axioms:
  [propext, Classical.choice, Quot.sound, Lutar.Wave6.SetAlpha.setAlpha_cauchy]
'Lutar.Wave6.SetDelta.geomMean_unique_KS' depends on axioms:
  [propext, Classical.choice, Quot.sound,
   Lutar.Wave6.SetDelta.KS_theorem_1_1, Lutar.Wave6.SetDelta.setDelta_stage2]
'Lutar.Wave6.SetAlpha.maxAgg_not_A5prime'      depends on axioms: [propext, Classical.choice, Quot.sound]  -- impostor death, axiom-free
'Lutar.Wave6.SetDelta.arithmeticMean_not_delta5' depends on axioms: [propext, Classical.choice, Quot.sound]  -- impostor death, axiom-free

Theorem U — governance-safe uniqueness (REAL · CONDITIONAL, axiom-free)

Rule of citation (Doctrine v11): any Λ-uniqueness claim cites Theorem U or its corollaries U₁ / U₂ — uniqueness holds modulo the audit-invariant equivalence ≈Λ under the Identifiability Assumptions (IA); strict = only under the documented Anchored / Normalized predicate. Source: Lutar/Uniqueness/TheoremU.lean (+ LambdaEquiv.lean, Identifiability.lean, AxiomCheck.lean); dependency ledger DEPENDENCY_MAP.md.

Result	Statement	Maturity
Theorem U (`TheoremU_LambdaUnique`)	any two IA-solutions are `≈Λ` (indeed `=`), by REDUCTION to Round13 — no new axiom, no `sorry`	REAL · CONDITIONAL (axiom-free)
Corollary U₁ (`CorollaryU1_LambdaUnique_Separable`)	separable, slice-multiplicative aggregator ⇒ Λ (`Round13.lambda_unique_of_separable`)	REAL · CONDITIONAL
Corollary U₂ (`CorollaryU2_LambdaUnique_Factors`)	power-law factorization `Φ x = ∏ (x i)^(αᵢ)` ⇒ Λ (`Round13.lambda_unique_of_factors`)	REAL · CONDITIONAL
strict `=` (`TheoremU_LambdaUnique_eq`, `lambda_equiv_to_eq_of_anchored`)	`≈Λ` collapses to `=` only under `Anchored` / `Normalized`	REAL · CONDITIONAL
Conjecture 1 (`Conjecture1_LambdaUnique`)	unconditional uniqueness under bare A1–A5	OPEN — non-claim: statement-only, machine-checked FALSE as stated; bounty `lambda-bounty`

Theorem U is EXPERIMENTAL · additive — it does not move the locked count of 5 and does not change Λ's Conjecture-1 status. The ≈Λ relation is genuinely non-trivial: the proven A1–A5 counterexample maxAgg is ≉Λ to Λ 2 (lambdaEquiv_nondegenerate), so "uniqueness modulo ≈Λ" excludes the impostor.

What we do not claim

NOT unconditional uniqueness under the original weaker axioms A1–A5. That statement is machine-checked false — the in-tree counterexample Round13.maxAgg_ne_Lambda exhibits an aggregator satisfying A1–A5 that is not Λ.
Λ-uniqueness therefore stays Conjecture 1, never a theorem. Strengthening the axiom class (A5 → A5′ multiplicativity, or deriving continuity via Kiss–Shulman) or reframing modulo ≈Λ under IA (Theorem U) is how the conditional results become provable; it does not close the original weaker conjecture.

Open bounty: lambda-bounty · BOUNTY.md.

4. Counts (honest)

Metric	Value
Locked proven formulas	5 — `{F1, F11, F12, F18, F19}` @ `c7c0ba17`; the count is itself a no-axiom Lean theorem (`locked_count_five`)
Locked kernel	`749` declarations / `14` unique axioms / `163` tracked sorries · Lean `v4.13.0` · `lake build` clean
Experimental scope (current `main`)	`7885fd9` · Lean `v4.18.0` · `1304` declarations / `22` unique axioms · CI-green
Experimental kernel-verified (CI-green) — ~36 theorems	wave-5 (11), wave-6 (11), wave-7 (10), wave-8 (10), agentic-loop (28), airtight Λ Set α+δ (22 results) — never in the locked count
Λ-uniqueness	Conjecture 1 — conditional within strengthened classes (CI-green); unconditional uniqueness machine-checked false
Supply chain	SLSA L1 honest today (cosign signing + `slsa.dev/provenance/v0.2` wired). SLSA L2 is roadmap — build-provenance attestation not yet earned on deployed images. L3 is out of scope. FedRAMP, Iron Bank, and CMMC are not pursued and not claimed.

5. Citations

Λ axiomatic characterization: Aczél & Saaty (1983), Procedures for synthesizing ratio judgements, J. Math. Psych. 27(1):93–102, doi:10.1016/0022-2496(83)90028-7; Csató (2018), arXiv:1706.07256; Kiss & Shulman (2026), Theorem 1.1, arXiv:2606.05221.
Loop: Goguen & Meseguer (1982), doi:10.1109/SP.1982.10014; Merkle (1987); NIST FIPS 180-4.
DOI lineage: Zenodo concept DOI 10.5281/zenodo.19944926.

Proof reports: team/PROVE_WAVE5..7_REPORT.md, team/PROVE_AGENTIC_LOOP_REPORT.md, team/LAMBDA_UNIQUENESS_PROOF_REPORT.md. All commits Signed-off-by Stephen P. Lutar Jr. stephenlutar2@gmail.com.

6. Putnam 2025 — honest current verdict (additive)

The honest, doctrine-v11 per-problem verdict for the canonical Putnam 2025 set (86th William Lowell Putnam Mathematical Competition, Dec 6 2025: A1–A6, B1–B6), computed from the Lean kernel on lutar-lean main @ b7c3e38. This section is additive — the locked-5 {F1, F11, F12, F18, F19} @ c7c0ba17 and the Λ = Conjecture 1 line above are unchanged.

We are not doing "drones solve Putnam." We are doing: Intelligence → Structure → Conjecture → Certificate. killinchu supplies intelligence (tracking, fusion, ROE decisions, signed receipts). We extract mathematical structure (graphs, constraints, optimization instances). We pose Putnam-grade + SZL-native problems. We ship certificates (Lean-verified REAL theorems, reproducible benchmarks, provenance).

Headline: 0 REAL / 11 DEMO / 1 OPEN. The headline number is the count of REAL (Lean-kernel-checked) theorems.

Label	Meaning
REAL	Lean-kernel checked, no sorry, no extra axioms beyond declared
DEMO	compiles but uses sorry/unproven lemmas
OPEN	statement only

Problem	Lean proof file	Status	Note
A1	`Lutar/Putnam/P_A1.lean`	DEMO	formalized statement; proof uses sorry/unproven lemmas
A2	`Lutar/Putnam/P_A2.lean`	DEMO	formalized statement; proof uses sorry/unproven lemmas
A3	`Lutar/Putnam/P_A3.lean`	OPEN	statement only (True-shell); official answer withheld pending a real proof
A4	`Lutar/Putnam/P_A4.lean`	DEMO	formalized statement; proof uses sorry/unproven lemmas
A5	`Lutar/Putnam/P_A5.lean`	DEMO	formalized statement; proof uses sorry/unproven lemmas
A6	`Lutar/Putnam/P_A6.lean`	DEMO	formalized statement; proof uses sorry/unproven lemmas
B1	`Lutar/Putnam/P_B1.lean`	DEMO	formalized statement; proof uses sorry/unproven lemmas
B2	`Lutar/Putnam/P_B2.lean`	DEMO	formalized statement; proof uses sorry/unproven lemmas
B3	`Lutar/Putnam/P_B3.lean`	DEMO	formalized statement; proof uses sorry/unproven lemmas
B4	`Lutar/Putnam/P_B4.lean`	DEMO	formalized statement; proof uses sorry/unproven lemmas
B5	`Lutar/Putnam/P_B5.lean`	DEMO	formalized statement; proof uses sorry/unproven lemmas
B6	`Lutar/Putnam/P_B6.lean`	DEMO	formalized statement; proof uses sorry/unproven lemmas
SZL-12A / SZL-12B	— not yet on `main`	PENDING	SZL-native originals — pending upstream kernel work

A3 is OPEN (statement-only True-shell); the official 2025 A3 answer is intentionally withheld here until a REAL proof exists. No problem is currently REAL: each DEMO file formalizes the statement but discharges the proof with sorry or unproven lemmas. This page will show REAL counts the moment the kernel run lands verified proofs.