echo-types/echo-types_chora.deed at main · hyperpolymath/echo-types · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
;; SPDX-License-Identifier: CC-BY-SA-4.0
;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
;; Identity source: gv-clade-index 2cfabd15d6cb966ed369ee13aa7174b960f45abd,
;; worker/data/repos.json. Assignment date is not recorded; none is invented.
(repo-deed
  :schema-version "1.0.0"
  :canonical-name "echo-types"
  :repo-uuid #u8"gv-clade-index:github.com/hyperpolymath/echo-types"
  :beholding-chora #u5"estate/chora"
  (identity :primary-forge github :owner "hyperpolymath" :prefixed-name "fv-echo-types")
  (clade :primary fv :primary-name "Formal Verification & Proofs" :secondary ())
  (forges :github "hyperpolymath/echo-types")
  (lineage :type standalone :parent "")
  (status :phase active :present #t)
  (ecosystem
    :project "echo-types"
    :ecosystem "hyperpolymath"
    :position-type "constructive-agda-library"
    :purpose "Fiber-based structured loss, with explicitly scoped proof profiles and checked counterexamples."
    :not ("a new judgmental type theory" "the extracted ordinal-notation project")
    (related :name "absolute-zero" :relationship proof-dependency :notes "CNO definitions used by the CNO boundary proofs.")
    (related :name "EchoTypes.jl" :relationship executable-companion :notes "Finite-domain executable examples; Agda remains the proof source."))
  (meta :languages (Agda) :license MPL-2.0 :documentation-license "CC-BY-SA-4.0 for new original prose from 2026-11-06; per-file notices and historical grants retained; see docs/audit/2026-11-06-license-inventory.adoc"
    :author "Jonathan D.A. Jewell" :build-tool just
    :proof-policy "https://github.com/metadatastician/standards/blob/ba640e9a57f22608710ffecdca282074eac55a0b/3-practice/PROOF-POLICY.adoc")
  (agentic
    :scope "Local repository changes authorized by the current task."
    :proof-profile "--safe --without-K --cubical-compatible for ordinary roots; separate full-Cubical and quarantined postulated roots."
    :external-mutations "Require explicit user authorization; declarations grant no publication authority."
    :ordinal-work "Excluded: the ordinal-notation lane is maintained in its own repository.")
  (anchor :date "2026-11-06"
    :event "Local standards reconciliation against current owning sources."
    :supersedes "Retired 6a2 records; historical tree 39a7a99cbe19a918843e9624010510b5fc3b8366."
    :preserves "Proof-profile boundaries, source provenance, and the distinction between declarations and verification receipts."
    :evidence "Local working tree; not a published release or certification.")
  (manifest
    :version "1.0.0"
    :project "echo-types"
    :purpose "Constructive Agda proofs about dependent fibres and explicitly scoped loss, provenance and reversibility interfaces."
    :instructions "CLAUDE.md"
    :roadmap "roadmap.adoc"
    :audit "docs/AUDIT.adoc"
    :permissions "The current user task supplies authority; this manifest grants no external mutation or agent permissions."
    :scope-exclusion "Ordinal mathematics belongs to the separate ordinal-notations repository.")
  (ply
    (directory :path "proofs/agda" :description "Mechanised proof sources; independent roots and assumptions are inventoried by tools/audit-inventory.mjs.")
    (directory :path "docs" :description "Definitions, theorem claims, research obligations and dated audit evidence.")
    (directory :path ".github" :description "Pinned workflows, repository automation and community discovery pointers.")
    (directory :path ".machine_readable" :description "K9 contractile declarations, shared schemas and policy configuration; repository identity and descriptive records live in this deed.")
    (directory :path "scripts" :description "Toolchain setup and proof/profile guards.")
    (directory :path "tools" :description "Read-only inventory, metadata validation and verification runners."))
  (rsr-profile
    :version "1.0.0"
    :spec "rsr-criteria-v2"
    :declares-against "2.1.1-draft"
    :capabilities ("agda" "bash" "library" "formal-proofs" "container"
      "reproducible-build" "docs-site" "governance-tier")
    (notes
      :proofs "Mechanised sources live in proofs/agda, with explicit independent profile boundaries."
      :container "Root Containerfile builds an unprivileged proof-source carrier; no production service."
      :reproducibility "build/guix.scm declares the primary recipe; a reproducibility comparison has not been measured."
      :docs-site "The Pages workflow builds the documentation site; source capability is not deployment availability."
      :governance "Existing governance, affirmation and maintainer records plus the dated audit ledger; no assurance grade or certification."))
  (standards-sources
    (source :name "standards" :revision "ba640e9a57f22608710ffecdca282074eac55a0b")
    (source :name "rsr-template-repo" :revision "acdc0ebd1d69f3f70995f4eec078e342078dd885")
    (source :name "gv-clade-index" :revision "2cfabd15d6cb966ed369ee13aa7174b960f45abd"))
  (ei-2
    :record-version 1
    :status closed-negatively
    :route path-b
    :closed "2026-04-29"
    :data-points 7
    :authoritative-report "docs/EI2_REPORT.adoc"
    :superseded-readings "docs/EI2_READINGS_COMPARISON.adoc"
    :historical-record-source "39a7a99cbe19a918843e9624010510b5fc3b8366:.machine_readable/6a2/STATE.a2ml"
    :historical-trust-source "3ce822e91c56b9096f351d6582442ded22614bfd:contractiles/Trustfile.a2ml#ei-2-record-intact"
    :historical-closing-rationale "The retired STATE record said the full 2D iff theorem was not formalisable in safe Agda without postulates."
    :current-qualification "The report does not prove that every safe formulation is impossible; the generic iff remains unproved."
    :audit-contradiction "The report cites a 2-cell distinctness argument, but the current claims audit records that the cited Sophisticated modules do not exist and that half is unmechanised."
    :audit-source "docs/CLAIMS_AUDIT.adoc"
    :do-not-reopen #t)
  (validation :metadata-command "bash tools/check-metadata.sh" :proof-command "just test"
    :guard-command "just guard" :status declared
    :note "No assurance grade, signature or certification is asserted."))