From e0d16152800858d15c0f3081f4cb7b07ae8c4389 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 20 May 2026 14:46:39 +0100 Subject: [PATCH] =?UTF-8?q?theory:=20Axis=208=20graded=20access=20modality?= =?UTF-8?q?=20=E2=80=94=20thin=20slice=20(Access,=20=E2=89=A4a,=20?= =?UTF-8?q?=E2=89=A4a-trans,=20=E2=89=A4a-prop)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lands the thin-slice obligations 1-6 of the Axis 8 graded access modality (decision: refinement 2 of taxonomy.md §8 / the Axis 8 design study). Mirrors EchoGraded / EchoLinear's order-layer recipe verbatim: 1. Access -- 5-grade enum (free / decidable / enum / feasible / infeasible) 2. _≤a_ -- Hasse-enumerated access order (15 constructors, one per reachable pair) 3. ≤a-trans -- transitivity by case-split 4. ≤a-prop -- propositionality by case-split + refl; the load-bearing lemma per the design's §6 falsifier — DID close on refl 5. CEcho + EchoAccess -- per-grade carrier + Σ-shape package 6. access-of, degrade-access -- projection + _≤a_-indexed degrade Deferred to the follow-up PR (per the body of EchoAccess.agda and the Axis 8 design doc §5 items 5-8): * degrade-access-comp / -compose / -via-join — per-decoration composition; the factoring-free closer chain of composition.md §6. * _⊔a_ join + ≤a-⊔a-{left,right,univ} — categorical join. * Honest carrier for enum / feasible / infeasible (bridge to EchoFiberCount.FiberSize-fin) — the falsifier mode B of the design's §6. Current carriers are minimal Lift ⊤ placeholders so the order layer ships green. Wired into All.agda; headlines pinned in Smoke.agda. No postulates, no escape pragmas, --safe --without-K throughout. Refs docs/echo-types/roadmap.md "Theory work" Axis 8 entry (line 31) and roadmap item 6 (line 239). Does NOT close anything. Agda build (Agda 2.8.0, stdlib v2.3): $ LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda Checking All (.../proofs/agda/All.agda). Checking EchoAccess (.../proofs/agda/EchoAccess.agda). Checking Smoke (.../proofs/agda/Smoke.agda). EXIT=0 $ LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/Smoke.agda EXIT=0 Co-Authored-By: Claude Opus 4.7 (1M context) --- proofs/agda/All.agda | 1 + proofs/agda/EchoAccess.agda | 262 ++++++++++++++++++++++++++++++++++++ proofs/agda/Smoke.agda | 22 +++ 3 files changed, 285 insertions(+) create mode 100644 proofs/agda/EchoAccess.agda diff --git a/proofs/agda/All.agda b/proofs/agda/All.agda index 0ff91a6..c8da97a 100644 --- a/proofs/agda/All.agda +++ b/proofs/agda/All.agda @@ -19,6 +19,7 @@ open import EchoCNOBridge open import EchoApprox open import EchoIndexed open import EchoDecidable +open import EchoAccess open import EchoFiberCount open import EchoEpistemicResidue open import EchoRelational diff --git a/proofs/agda/EchoAccess.agda b/proofs/agda/EchoAccess.agda new file mode 100644 index 0000000..531fe7a --- /dev/null +++ b/proofs/agda/EchoAccess.agda @@ -0,0 +1,262 @@ +{-# OPTIONS --safe --without-K #-} + +-- Axis-8 second formal artifact: graded access modality. +-- +-- `EchoDecidable.agda` shipped the decidability-respecting refinement +-- of axis 8 (taxonomy.md §8): `EchoDec f y := Dec (Echo f y)`. That +-- module is the bottom of a lattice; this one builds the lattice. +-- +-- The graded access modality refines `Echo f y` with a grade +-- `c : Access` naming the *feasibility class* at which the echo's +-- witness is reachable: +-- +-- free — witness in hand, no search +-- decidable — a constructive decider exists (EchoDecidable.EchoDec) +-- enum — exhaustive Fin-search (EchoFiberCount terrain) +-- feasible — polynomial-time class (grade-only marker) +-- infeasible — super-polynomial / cryptographic; witness exists +-- only metatheoretically (grade-only marker) +-- +-- The chain `free ≤ decidable ≤ enum ≤ feasible ≤ infeasible` is +-- reflexive at every grade and one-step at the named edges; the order +-- relation `_≤a_` is enumerated by its 15 reachable pairs in +-- Hasse-diagram style, exactly mirroring `EchoGraded._≤g_` and +-- `EchoLinear._≤m_`. +-- +-- This file lands the **thin slice** of the recipe per the design in +-- `taxonomy.md` §8 / the Axis 8 study under `/tmp/echo-types-exploration`: +-- +-- 1. `Access` — enum of five feasibility classes +-- 2. `_≤a_` — Hasse-enumerated access order +-- 3. `≤a-trans` — transitivity by case-split +-- 4. `≤a-prop` — propositionality by case-split + refl +-- (load-bearing; the falsifier from the +-- design's §6) +-- 5. `EchoAccess` — Σ-shape carrier indexed by `Access` +-- 6. `access-of`, +-- `degrade-access` — projection + ≤a-indexed degrade primitive +-- +-- Deferred to follow-up (the design doc §5 obligations 5–8): +-- +-- * `degrade-access-comp`, `degrade-access-compose`, +-- `degrade-access-via-join` — per-decoration composition; the +-- "factoring-free" closer chain of `composition.md` §6. +-- * `_⊔a_` join + `≤a-⊔a-{left,right,univ}` — categorical join +-- structure. +-- * Honest carrier for `enum` (bridge to `EchoFiberCount.FiberSize-fin`) +-- so `feasible` / `infeasible` are not Potemkin labels — the +-- falsifier mode B of the design's §6. The current carriers are +-- deliberately the minimal placeholders that let the order layer +-- ship green. + +module EchoAccess where + +open import Level using (Level; _⊔_) +open import Data.Unit.Base using (⊤; tt) +open import Data.Product.Base using (Σ; _,_) +open import Relation.Nullary.Decidable.Core using (yes) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +open import Echo using (Echo) +open import EchoDecidable using (EchoDec) + +---------------------------------------------------------------------- +-- 1. The access enum +---------------------------------------------------------------------- + +-- Five feasibility classes along a single chain. Lower = more +-- accessible. The taxonomy §8 reading: `free` is information- +-- theoretic *and* operationally trivial; `infeasible` is the +-- cryptographic-hash regime (a witness exists metatheoretically but +-- is computationally out of reach). + +data Access : Set where + free : Access + decidable : Access + enum : Access + feasible : Access + infeasible : Access + +---------------------------------------------------------------------- +-- 2. The access order +---------------------------------------------------------------------- + +-- Hasse-enumerated: every reachable (c1, c2) pair has exactly one +-- inhabitant. 5 grades give 15 constructors (5+4+3+2+1). Each +-- constructor names its source and target — the same shape as +-- `EchoGraded._≤g_` (6 constructors for 3 grades) and +-- `EchoLinear._≤m_` (3 constructors for 2 modes). This shape is what +-- makes `≤a-prop` reduce to case-split + `refl` under `--without-K`. + +data _≤a_ : Access → Access → Set where + free≤free : free ≤a free + free≤decidable : free ≤a decidable + free≤enum : free ≤a enum + free≤feasible : free ≤a feasible + free≤infeasible : free ≤a infeasible + decidable≤decidable : decidable ≤a decidable + decidable≤enum : decidable ≤a enum + decidable≤feasible : decidable ≤a feasible + decidable≤infeasible : decidable ≤a infeasible + enum≤enum : enum ≤a enum + enum≤feasible : enum ≤a feasible + enum≤infeasible : enum ≤a infeasible + feasible≤feasible : feasible ≤a feasible + feasible≤infeasible : feasible ≤a infeasible + infeasible≤infeasible : infeasible ≤a infeasible + +---------------------------------------------------------------------- +-- 3. Transitivity +---------------------------------------------------------------------- + +-- Same recipe as `EchoGraded.≤g-trans`: on a reflexive first step, +-- propagate `p23`; otherwise enumerate the reachable composites. The +-- enumerated relation has exactly one inhabitant per (c1, c3) pair so +-- there is no choice of factoring — each clause is forced. + +≤a-trans : ∀ {c1 c2 c3} → c1 ≤a c2 → c2 ≤a c3 → c1 ≤a c3 +≤a-trans free≤free p23 = p23 +≤a-trans free≤decidable decidable≤decidable = free≤decidable +≤a-trans free≤decidable decidable≤enum = free≤enum +≤a-trans free≤decidable decidable≤feasible = free≤feasible +≤a-trans free≤decidable decidable≤infeasible = free≤infeasible +≤a-trans free≤enum enum≤enum = free≤enum +≤a-trans free≤enum enum≤feasible = free≤feasible +≤a-trans free≤enum enum≤infeasible = free≤infeasible +≤a-trans free≤feasible feasible≤feasible = free≤feasible +≤a-trans free≤feasible feasible≤infeasible = free≤infeasible +≤a-trans free≤infeasible infeasible≤infeasible = free≤infeasible +≤a-trans decidable≤decidable p23 = p23 +≤a-trans decidable≤enum enum≤enum = decidable≤enum +≤a-trans decidable≤enum enum≤feasible = decidable≤feasible +≤a-trans decidable≤enum enum≤infeasible = decidable≤infeasible +≤a-trans decidable≤feasible feasible≤feasible = decidable≤feasible +≤a-trans decidable≤feasible feasible≤infeasible = decidable≤infeasible +≤a-trans decidable≤infeasible infeasible≤infeasible = decidable≤infeasible +≤a-trans enum≤enum p23 = p23 +≤a-trans enum≤feasible feasible≤feasible = enum≤feasible +≤a-trans enum≤feasible feasible≤infeasible = enum≤infeasible +≤a-trans enum≤infeasible infeasible≤infeasible = enum≤infeasible +≤a-trans feasible≤feasible p23 = p23 +≤a-trans feasible≤infeasible infeasible≤infeasible = feasible≤infeasible +≤a-trans infeasible≤infeasible infeasible≤infeasible = infeasible≤infeasible + +---------------------------------------------------------------------- +-- 4. Propositionality of the access order +---------------------------------------------------------------------- + +-- Each constructor of `_≤a_` is pinned by both source and target, so +-- the order is propositional: any two proofs of `c1 ≤a c2` are equal. +-- This is the *load-bearing* lemma of the access recipe — see +-- `composition.md` §6 and `EchoGraded.≤g-prop` (lines 79–89 of +-- `EchoGraded.agda`). The whole "factoring-free composition" closer +-- chain rests on it. +-- +-- Pattern-matches close under `--without-K` because each (c1, c2) +-- pair has exactly one inhabitant of `_≤a_`; Agda's case-split picks +-- the unique constructor on both sides and both reduce to `refl`. +-- The design doc's §6 falsifier reads: "If `≤a-prop` does not close +-- on case-split + `refl` in ≤30 minutes, the design is wrong; collapse +-- grades that case-split distinguished but propositional equality +-- does not." This module shows the chain does close. + +≤a-prop : ∀ {c1 c2} (p p' : c1 ≤a c2) → p ≡ p' +≤a-prop free≤free free≤free = refl +≤a-prop free≤decidable free≤decidable = refl +≤a-prop free≤enum free≤enum = refl +≤a-prop free≤feasible free≤feasible = refl +≤a-prop free≤infeasible free≤infeasible = refl +≤a-prop decidable≤decidable decidable≤decidable = refl +≤a-prop decidable≤enum decidable≤enum = refl +≤a-prop decidable≤feasible decidable≤feasible = refl +≤a-prop decidable≤infeasible decidable≤infeasible = refl +≤a-prop enum≤enum enum≤enum = refl +≤a-prop enum≤feasible enum≤feasible = refl +≤a-prop enum≤infeasible enum≤infeasible = refl +≤a-prop feasible≤feasible feasible≤feasible = refl +≤a-prop feasible≤infeasible feasible≤infeasible = refl +≤a-prop infeasible≤infeasible infeasible≤infeasible = refl + +---------------------------------------------------------------------- +-- 5. The graded carrier +---------------------------------------------------------------------- + +-- Per-grade carriers along the design's §4 sketch. `free` and +-- `decidable` are honest (full witness; constructive decider). The +-- `enum`, `feasible`, and `infeasible` carriers are deliberately the +-- minimal placeholder `⊤` for this slice — promoting them to honest +-- bridges (`enum` → `FiberSize-fin`, `feasible` / `infeasible` → +-- complexity-tagged variants) is the design's deferred §6 mode-B +-- mitigation and lands in the follow-up PR. +-- +-- The level lift on `⊤` is needed because `Echo f y` lives in +-- `Set (a ⊔ b)` and Agda demands a single ambient level across the +-- match. `Level.Lift` from the standard library keeps the carrier +-- universe-uniform without disturbing `≤a-prop` (which is +-- grade-indexed, not carrier-indexed). + +open import Level using (Lift; lift) + +CEcho : + ∀ {a b} {A : Set a} {B : Set b} + → Access → (A → B) → B → Set (a ⊔ b) +CEcho free f y = Echo f y +CEcho decidable f y = EchoDec f y +CEcho {a} {b} enum _ _ = Lift (a ⊔ b) ⊤ +CEcho {a} {b} feasible _ _ = Lift (a ⊔ b) ⊤ +CEcho {a} {b} infeasible _ _ = Lift (a ⊔ b) ⊤ + +-- The Σ-shape mirror of `EchoGraded.GEcho`'s implicit graded bundle: +-- pair a grade with content at that grade. Useful when callers want +-- a single hom-set to thread through the access lattice rather than +-- a grade-indexed family. + +EchoAccess : + ∀ {a b} {A : Set a} {B : Set b} + → (A → B) → B → Set (a ⊔ b) +EchoAccess f y = Σ Access (λ c → CEcho c f y) + +---------------------------------------------------------------------- +-- 6. `access-of` and `degrade-access` +---------------------------------------------------------------------- + +-- Projection: read off the access grade of a packed `EchoAccess`. + +access-of : + ∀ {a b} {A : Set a} {B : Set b} + {f : A → B} {y : B} → EchoAccess f y → Access +access-of (c , _) = c + +-- The `_≤a_`-indexed degrade primitive. Going to a *less accessible* +-- grade *forgets* content: `free → decidable` wraps the witness in +-- `yes`, every step into the placeholder block discards down to +-- `tt`, and reflexive cases are the identity. +-- +-- The cases enumerate the same 15 constructors as `_≤a_`. The chain +-- `free → decidable → enum/.../infeasible` is the only place real +-- content moves; from `enum` onward the carrier is already `⊤`-lifted +-- so every transition is `lift tt`. +-- +-- Per-decoration composition (`degrade-access-comp` + `compose` + +-- `via-join`) is deferred to the follow-up PR per the body of this +-- module. The order layer (`≤a-trans`, `≤a-prop`) is the +-- mathematical prerequisite for that follow-up, and lands here. + +degrade-access : + ∀ {a b} {A : Set a} {B : Set b} {f : A → B} {y : B} + {c1 c2 : Access} → c1 ≤a c2 → CEcho c1 f y → CEcho c2 f y +degrade-access free≤free e = e +degrade-access free≤decidable e = yes e +degrade-access free≤enum _ = lift tt +degrade-access free≤feasible _ = lift tt +degrade-access free≤infeasible _ = lift tt +degrade-access decidable≤decidable d = d +degrade-access decidable≤enum _ = lift tt +degrade-access decidable≤feasible _ = lift tt +degrade-access decidable≤infeasible _ = lift tt +degrade-access enum≤enum e = e +degrade-access enum≤feasible _ = lift tt +degrade-access enum≤infeasible _ = lift tt +degrade-access feasible≤feasible e = e +degrade-access feasible≤infeasible _ = lift tt +degrade-access infeasible≤infeasible e = e diff --git a/proofs/agda/Smoke.agda b/proofs/agda/Smoke.agda index 19e3f60..9c716a4 100644 --- a/proofs/agda/Smoke.agda +++ b/proofs/agda/Smoke.agda @@ -82,6 +82,28 @@ open import EchoDecidable using ; echo-dec-compose-fin ) +-- Axis 8 second formal artifact (taxonomy.md §8): graded access +-- modality, thin slice. Mirrors `EchoGraded` and `EchoLinear`'s order +-- layer (enum, Hasse-enumerated order, transitivity, propositionality) +-- plus the Σ-shape carrier + `_≤a_`-indexed degrade primitive. +-- Per-decoration composition (`degrade-access-comp` / `compose` / +-- `via-join`) and join structure (`_⊔a_`) land in the follow-up PR. +open import EchoAccess using + ( Access + ; free + ; decidable + ; enum + ; feasible + ; infeasible + ; _≤a_ + ; ≤a-trans + ; ≤a-prop + ; CEcho + ; EchoAccess + ; access-of + ; degrade-access + ) + open import EchoFiberCount using ( FiberSize-fin ; FiberSize-fin-no-hit