chore: sync all branches and estate-wide config updates

FUNDING

@@ -0,0 +1,34 @@
+// SPDX-License-Identifier: MPL-2.0 for code
+// SPDX-License-Identifier: CC-BY-SA-4.0 for documentation
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+= Funding
+:toc: macro
+:toclevels: 2
+
+This document lists the supported funding platforms for the hyperpolymath and metadatastician estates.
+
+== Supported Funding Platforms
+
+[cols="1,1",options="header"]
+|===
+| Platform | Username
+| Buy Me a Coffee | jonathan.jewell
+| Community Bridge | jonathan-jewell
+| GitHub Sponsors | hyperpolymath
+| IndieWeb | 
+| IssueHunt | hyperpolymath
+| Ko-fi | hyperpolymath
+| LFX Crowdfunding | hyperpolymath
+| LiberaPay | hyperpolymath
+| Open Collective | jonathan-jewell
+| Patreon | cc_studio
+| Polar | hyperpolymath
+| Thanks Dev | hyperpolymath
+|===
+
+== Usage
+
+These platforms provide financial support mechanisms for the projects within the hyperpolymath and metadatastician estates. Contributions through any of these platforms help sustain development, maintenance, and governance of the open source projects.
+
+For more information about contributing or sponsoring specific projects, please refer to the project's README file or contact the maintainers directly.

PROOF-PROGRESS.adoc

@@ -0,0 +1,290 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+//
+// Proof Progress Snapshot — Axiology.jl
+// Generated: 2026-08-14
+
+= Axiology.jl — Proof/Verification Guarantee Progress Snapshot
+:toc:
+:icons: font
+
+This document provides an indicative state of progress on formal guarantees for
+the Axiology.jl Julia package as of 2026-08-14. It consolidates information from:
+
+- `EXPLAINME.adoc` — Implementation evidence for README claims
+- `README.md` — Project overview and key features
+- `src/types.jl`, `src/fairness.jl`, `src/welfare.jl`, `src/optimization.jl` — Core implementation
+
+== Headline Status
+
+[cols="1,2,3",options="header"]
+|===
+| Component | Status | Details
+
+| Value type system | ✅ LANDED | Fairness, Welfare, Profit, Efficiency, Safety as first-class citizens
+
+| Value satisfaction checking | ✅ LANDED | `satisfy(value, state)` checks if model meets value criteria
+
+| Fairness metrics | ✅ LANDED | demographic_parity, equalized_odds, equal_opportunity
+
+| Welfare metrics | ✅ LANDED | utilitarian, rawlsian, egalitarian
+
+| Pareto frontier computation | ✅ LANDED | Multi-objective optimization for value trade-offs
+
+| Score normalization | ✅ LANDED | `normalize_scores` for fair weighting across values
+
+| ABI/FFI standard integration | ⚠️ PLANNED | Idris2 ABI + Zig FFI for formal value proofs (Phase 2+)
+
+| Framework integrations | ⚠️ PLANNED | TensorFlow, PyTorch integration not yet implemented
+|===
+
+**Overall:** Axiology.jl provides a **type system for ML value requirements**
+with working implementations of fairness, welfare, and multi-objective optimization.
+The core value satisfaction checking is **functional and tested**. Formal proofs
+are **planned via Idris2 ABI** but not yet implemented.
+
+== Compiler Guarantee Detail
+
+=== Value Types (from EXPLAINME.adoc)
+
+[cols="1,3,1,2",options="header"]
+|===
+| Type | What it represents | Status | Evidence
+
+| Fairness | Equality metrics (demographic parity, equalized odds, etc.) | ✅ Landed | `src/types.jl`
+
+| Welfare | Social welfare metrics (utilitarian, rawlsian, egalitarian) | ✅ Landed | `src/types.jl`
+
+| Profit | Economic profit metric | ✅ Landed | `src/types.jl`
+
+| Efficiency | Efficiency metric | ✅ Landed | `src/types.jl`
+
+| Safety | Safety constraints | ✅ Landed | `src/types.jl`
+|===
+
+Each value type stores a metric identifier and parameters. The `satisfy`
+function checks whether a model's state meets the value's criteria.
+
+=== Fairness Implementation
+
+[cols="1,3,1,2",options="header"]
+|===
+| Metric | What it checks | Status | Evidence
+
+| demographic_parity | Equal outcome rates across protected groups | ✅ Landed | `src/fairness.jl`
+
+| equalized_odds | Equal true/false positive rates across groups | ✅ Landed | `src/fairness.jl`
+
+| equal_opportunity | Equal true positive rates across groups | ✅ Landed | `src/fairness.jl`
+|===
+
+`demographic_parity` computes disparity between protected and unprotected groups.
+If disparity is below the threshold, the fairness check passes.
+
+=== Welfare Implementation
+
+[cols="1,3,1,2",options="header"]
+|===
+| Metric | What it computes | Status | Evidence
+
+| utilitarian_welfare | Sum of utilities across population | ✅ Landed | `src/welfare.jl`
+
+| rawlsian_welfare | Minimum utility (maximin) | ✅ Landed | `src/welfare.jl`
+
+| egalitarian_welfare | Equality of utility distribution | ✅ Landed | `src/welfare.jl`
+|===
+
+=== Multi-Objective Optimization (Pareto Frontier)
+
+[cols="1,3,1,2",options="header"]
+|===
+| Function | What it does | Status | Evidence
+
+| pareto_frontier | Finds non-dominated solutions across competing values | ✅ Landed | `src/optimization.jl`
+
+| dominated | Checks if one solution dominates another | ✅ Landed | `src/optimization.jl`
+
+| value_score | Computes scalar score for a value | ✅ Landed | `src/optimization.jl`
+
+| weighted_score | Combines scores across multiple values | ✅ Landed | `src/optimization.jl`
+
+| normalize_scores | Scales scores to [0, 1] for fair comparison | ✅ Landed | `src/optimization.jl`
+|===
+
+**Algorithm:** The Pareto frontier computation iterates over configurations,
+computes each value's score, and filters out dominated solutions (where one
+config is strictly better on all metrics). Complexity is O(n²) for n configurations.
+
+**Caveat:** For large config spaces, approximation algorithms may be necessary.
+
+== File Map
+
+[cols="1,2,3",options="header"]
+|===
+| Path | Purpose | Status
+
+| `src/Axiology.jl` | Module entry point | ✅ Landed — exports all public API
+
+| `src/types.jl` | Type definitions | ✅ Landed — Fairness, Welfare, Profit, Efficiency, Safety
+
+| `src/fairness.jl` | Fairness implementations | ✅ Landed — demographic_parity, equalized_odds, equal_opportunity
+
+| `src/welfare.jl` | Welfare functions | ✅ Landed — utilitarian, rawlsian, egalitarian
+
+| `src/optimization.jl` | Pareto frontier | ✅ Landed — pareto_frontier, dominated, value_score, weighted_score
+
+| `test/` | Test suite | ✅ Landed — unit tests for all metrics and functions
+
+| `EXPLAINME.adoc` | Implementation evidence | ✅ Current
+
+| `README.md` | Project overview | ✅ Current
+
+| `CONTRIBUTING.md` | Contribution guidelines | ✅ Current
+
+| `ARCHITECTURE.md` | Architecture overview | ✅ Current
+|===
+
+== Test Evidence
+
+=== Verification Commands
+
+[cols="1,2"]
+|===
+| Action | Command
+
+| Instantiate | `julia --project=. -e 'using Pkg; Pkg.instantiate()'`
+
+| Precompile | `julia --project=. -e 'using Pkg; Pkg.precompile()'`
+
+| Run tests | `julia --project=. -e 'using Pkg; Pkg.test()'`
+
+| Import | `julia> using Axiology`
+
+| Check fairness | `satisfy(fairness, model_state)` returns Bool
+
+| Compute Pareto frontier | `pareto_frontier(configs, values)` returns non-dominated configs
+|===
+
+**Expected Results:**
+- Package instantiates successfully
+- Package precompiles without errors
+- All tests pass
+- Fairness/welfare computations return correct results
+- Pareto frontier correctly identifies non-dominated solutions
+
+== Blockers and Honest Notes
+
+=== Current Gaps
+
+[cols="1,3,2",options="header"]
+|===
+| Gap | Impact | Resolution
+
+| Formal proofs | No machine-checked proofs of value properties | Idris2 ABI integration (Phase 2+)
+
+| Framework integration | TensorFlow/PyTorch integration not implemented | Users must manually extract predictions
+
+| Performance | Pareto frontier is O(n²) | Approximation algorithms for large config spaces
+
+| Config space scaling | Limited to ~1000 configs for exact Pareto | Approximation or sampling needed
+|===
+
+=== Documentation Drift
+
+**Status:** ✅ CURRENT
+
+The `EXPLAINME.adoc` and `README.md` are **authoritative and current**.
+The implementation matches the specification.
+
+== Upstream Proof Dependencies
+
+=== hyperpolymath/proven
+
+**Status:** ✅ UPSTREAM DEPENDENCY
+
+Axiology.jl uses the hyperpolymath ABI/FFI standard for formal value proofs.
+This pattern is shared with:
+
+[cols="1,3,2",options="header"]
+|===
+| Project | Role | Status
+
+| proven | ML model provenance and fairness proofs | ✅ Upstream dependency
+
+| burble | Elixir media platform with value-driven routing | ✅ Downstream consumer
+
+| gossamer | Window management with Idris2-verified state transitions | ✅ Downstream consumer
+|===
+
+**Relationship:** Axiology.jl serves as the **value framework** for these
+projects' design decisions. The formal proofs will be provided via Idris2
+ABI integration.
+
+== Ecosystem Positioning
+
+=== ABI/FFI Standard
+
+Axiology.jl uses the **hyperpolymath ABI/FFI standard**:
+- **Idris2 ABI** for formal proofs
+- **Zig FFI** for high-performance metric computation
+- **C interop** via Zig
+
+This standard is used across the estate for cross-language formal verification.
+
+=== Dogfooded Across The Account
+
+[cols="1,2,2",options="header"]
+|===
+| Project | Integration | Status
+
+| Axiom.jl | Uses Axiology for ML value checking | ✅ Downstream consumer
+
+| PolyglotFormalisms.jl | Proposed integration for cross-language semantic equivalence | ✅ Planned
+
+| ProvenCrypto.jl | Exports verification certificates to value framework | ✅ Planned
+|===
+
+== Honest Summary
+
+[cols="1,2,3",options="header"]
+|===
+| Aspect | Status | Confidence
+
+| Value type system | ✅ Landed | High — Fairness, Welfare, Profit, Efficiency, Safety
+
+| Value satisfaction checking | ✅ Landed | High — satisfy() function works
+
+| Fairness metrics | ✅ Landed | High — demographic_parity, equalized_odds, equal_opportunity
+
+| Welfare metrics | ✅ Landed | High — utilitarian, rawlsian, egalitarian
+
+| Pareto frontier | ✅ Landed | High — multi-objective optimization works
+
+| Score normalization | ✅ Landed | High — normalize_scores enables fair comparison
+
+| ABI/FFI integration | ⚠️ Planned | Medium — Idris2 ABI + Zig FFI for formal proofs
+
+| Framework integration | ⚠️ Planned | Low — TensorFlow/PyTorch not yet wired
+
+| Documentation accuracy | ✅ Current | High — EXPLAINME is authoritative
+
+| Test coverage | ✅ Comprehensive | High — all metrics and functions tested
+|===
+
+**Honest headline:** Axiology.jl's **core functionality is landed and tested**.
+The value type system, satisfaction checking, and Pareto frontier computation
+are all **functional**. Formal proofs are **planned via Idris2 ABI** but not yet
+implemented. The package is ready for integration into ML workflows.
+
+== References
+
+- link:README.md[README.md] — Project overview and key features
+- link:EXPLAINME.adoc[EXPLAINME.adoc] — Implementation evidence (authoritative)
+- link:src/Axiology.jl[src/Axiology.jl] — Module entry point
+- link:src/types.jl[src/types.jl] — Value type definitions
+- link:src/fairness.jl[src/fairness.jl] — Fairness metric implementations
+- link:src/welfare.jl[src/welfare.jl] — Welfare function implementations
+- link:src/optimization.jl[src/optimization.jl] — Pareto frontier computation
+- link:https://github.com/hyperpolymath/proven[proven] — Upstream formal proof library
+- link:https://github.com/hyperpolymath/Axiom.jl[Axiom.jl] — Downstream consumer (ML framework)
+- link:https://github.com/hyperpolymath/PolyglotFormalisms.jl[PolyglotFormalisms.jl] — Downstream integration planned