Skip to content

refactor(EpistemicScale): rehome pure math, drop aggregator#110

Merged
github-actions[bot] merged 1 commit into
mainfrom
epistemic-final-reorg
Jun 4, 2026
Merged

refactor(EpistemicScale): rehome pure math, drop aggregator#110
github-actions[bot] merged 1 commit into
mainfrom
epistemic-final-reorg

Conversation

@hawkrobe
Copy link
Copy Markdown
Owner

@hawkrobe hawkrobe commented Jun 4, 2026

Audit roadmap step F, the close-out: Caratheodory.lean and SignVectors.lean move to Core/Order/ beside FourierMotzkin.lean (mathlib-only files out of the linguistics tree; SignVec to root namespace); the aggregator's theorems (8a/8b/6/2, axiomA_iff_fa, belowCount) extract to a new EpistemicScale/Completeness.lean leaf; EpistemicTag/five_frameworks_agree move beside their MereoTag/LicensingPipeline siblings in Core/Scales/Defs.lean; the aggregator is deleted — the manifest lists leaves directly, mathlib-style. Deferred with rationale: FinAddMeasureComparativeProbability/Measure and the Defs/Basic split (high import churn across external consumers; the mixin instances from #109 already connect the layers). Local build was interrupted — CI gates this one.

@github-actions github-actions Bot enabled auto-merge (squash) June 4, 2026 00:38
@github-actions github-actions Bot merged commit f0cfebd into main Jun 4, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant