Audited Residue Calculus ARC 1.0 Formal Specification of the Canonical Audited Generator Noah Robideau License: Creative Commons Attribution 4.0 International (CC BY 4.0) License URL: https://creativecommons.org/licenses/by/4.0/ Suggested attribution: Noah Robideau, Audited Residue Calculus (ARC 1.0): Formal Specification of the Canonical Audited Generator, 2026, https://noahsarc.info/, licensed under CC-BY-4.0. ----------------------------------------------------------------------- ----------------------------------------------------------------------- A standalone mathematical system for residue-preserving reasoning, scoped answers, certified erasure, and obstruction-null completion. ----------------------------------------------------------------------- Version 1.0 ----------------------------------- ----------------------------------- Author Noah Robideau Document status Formal mathematical specification Generator CAG[Γ] = G[Γ] Foundation Univalent / homotopy-coherent dependent type theory Export date 2026-06-28 ----------------------------------------------------------------------- ----------------------------------------------------------------------- Every erased distinction must return as flatness, reconstruction, ledgering, or registered obstruction. ----------------------------------------------------------------------- ----------------------------------------------------------------------- Contents 1. Executive Abstract 3 2. Design Intent and Governing Law 3 3. Foundation and Metatheory 3 4. Syntax and Judgment Forms 4 5. Formal Problems and Residues 5 6. Exact Normal Forms and Residue Localization 5 7. Typed Carriers, Support, and Conservativity 6 8. States, Registries, and Total Remainder 6 9. Legal Transitions and Anti-Collapse 7 10. Failure Registry 8 11. Admissibility Compiler 8 12. Global Answer Objects and Descent 9 13. Scope Logic and Answer Records 10 14. Practical Closed Forms 11 15. Proof Trees and Closure 11 16. Models and the Term Generator 12 17. Initiality 12 18. Non-Collapse, Answer Soundness, and Operational Adequacy 13 19. Completion Certificate and Obstruction Register 13 Appendix A. Core Inference Rules 14 Appendix B. Theorem Index 15 Appendix C. Implementation Notes 16 Final Compression 17 1. Executive Abstract Audited Residue Calculus, abbreviated ARC, is a formal system for reasoning without silent erasure. It treats a problem as a structured presentation, computes the unresolved content of that presentation as a residue, and permits conclusions only when every generated residue has a certified fate. The canonical object of the system is the Canonical Audited Generator, denoted CAG[Γ] or G[Γ]. For a context Γ, G[Γ] is the initial structure generated by the ARC formation rules, constructors, equations, legal-transition rules, scope rules, answer-record rules, and failure-registration rules. ARC is not a universal solver. It does not assert that every residue is flat, every problem is solvable, or every answer is globally valid. Its stronger value is that it provides a universal exact continuation discipline: every presentable distinction can be converted into exact residue form, and every attempted erasure of information must expose its corresponding fiber, reconstruct the lost information, ledger it forward, or register an obstruction. ----------------------------------------------------------------------- Central Statement. For every context Γ, the canonical generator G[Γ] is initial among ARC models over Γ. Every derivable ARC answer is one of four kinds: a global answer, a scoped answer with provenance, a legally promoted scoped answer with fiber accounting, or a registered failure residue. ----------------------------------------------------------------------- ----------------------------------------------------------------------- 2. Design Intent and Governing Law The design intent of ARC is to prevent the most common failure of complex reasoning: a generated distinction disappears before it is solved. The system therefore separates intuition, presentation, residue, support, scope, proof, and completion. The method begins from a direction of search, but it does not treat that direction as proof. It compiles the raw input into a formal presentation, generates all residue forced by that presentation, and makes every later claim conditional on the fate of that residue. ----------------------------------------------------------------------- ARC Master Law: no generated residue may be discarded without flatness, reconstruction, ledgering, or failure registration. ----------------------------------------------------------------------- ----------------------------------------------------------------------- Flatness. A residue is flat when it is equivalent to the terminal object in its typed carrier. Flatness is the formal certificate of canonical solvedness. Reconstruction. A residue is reconstructed when there is auditable data from which an equivalent object is generated, together with the required equivalence certificate. Ledgering. A residue is ledgered when it is carried forward to a successor component through a typed comparison, with the necessary obligation and transfer certificates. Failure registration. A missing certificate, missing construction, ambiguity, obstruction, or unavailable decision procedure is not ignored. It becomes a typed failure residue. 3. Foundation and Metatheory ARC is stated relative to an ambient univalent or homotopy-coherent dependent type theory. Equivalent interpretations may be given in a sufficiently well-behaved infinity-categorical foundation. The formal system assumes universes, homotopy pullbacks, homotopy fibers, dependent sums, dependent products, mapping objects, section objects, and the particular initial algebra or colimit constructions explicitly invoked below. +-----------------------------------------------------------------------+ | Universe hierarchy: | | | | U₀ : U₁ : U₂ : ⋯ | | | | Small spaces: | | | | 𝒮 = 𝒮_(𝒰) | | | | Flatness of a space E: | | | | Flat(E) := Equiv(E, 𝟙) | | | | Obstruction: | | | | Obs(E) := (E → 𝟘) | | | | Constructive ambiguity: | | | | Amb(E) := ∥E∥ × ¬Flat(E) | +=======================================================================+ +-----------------------------------------------------------------------+ Regime classification is treated as a certificate problem. ARC does not assume a global decision procedure that classifies every residue as empty, ambiguous, or flat. When a decision is needed but unavailable, the missing decision certificate is registered as residue. +-----------------------------------------------------------------------+ | Regime certificate: | | | | RegimeCert(E) := Obs(E) + Amb(E) + Flat(E) | | | | Missing regime decision: | | | | RegimeDecisionRes(E) := RegimeCert(E) | +=======================================================================+ +-----------------------------------------------------------------------+ ----------------------------------------------------------------------- Metatheoretic Discipline. Every assertion of closure, reconstruction, soundness, completeness, support conservativity, termination, evidence calibration, resource validity, or scope promotion is represented by a certificate space. A certificate space may itself be obstructed, ambiguous, or flat. ----------------------------------------------------------------------- ----------------------------------------------------------------------- 4. Syntax and Judgment Forms ARC is a judgmental calculus. The following judgment forms define what may be built, used, transformed, certified, or reported. ----------------------------------------------------------------------- Judgment Meaning ----------------------------------- ----------------------------------- Γ ctx Γ is a well-formed context. Γ ⊢ τ type τ is a generated or admitted type. Γ ⊢ E : V_(τ) E is a carrier object at type τ. Γ ⊢ f : E →_(τ) F f is a carrier map at type τ. Γ ⊢ P : Prob_(τ) P is a typed formal problem. Γ ⊢ Res(P) : V_(τ) The residue of P is generated. Γ ⊢ α : State α is an audited state. Γ ⊢ T : Leg₁(α,β) T is a legal transition. Γ ⊢ F : OutDoc_(λ) F is an output doctrine at target type λ. Γ ⊢ A₀ = GloFλ(X;Γ) A₀ is the maximal declared answer object. Γ ⊢scope q : A₀ → A q is a generated scope map. Γ ⊢ a : 𝟙 → A a is a visible answer at scope A. Γ ⊢ R : AnsRec(Γ,X,F,λ) R is a valid answer record. Γ ⊢ Failure(label,C) C is registered as a failure residue. ----------------------------------------------------------------------- A derivation is valid only if each name, map, certificate, and scope used by the derivation is generated from the current context or admitted by an explicit context extension. Otherwise the admissibility residue is produced. 5. Formal Problems and Residues The primitive problem shape is the walking cospan. This single shape separates candidates, interfaces, and selected specifications. +-----------------------------------------------------------------------+ | Walking cospan: | | | | Λ = (0 → 1 ← 2) | | | | Typed formal problems: | | | | Prob_(τ) := Fun(Λ, V_(τ)) | | | | A problem P: | | | | P = (C_(P) → B_(P) ← S_(P)) | | | | Residue of P: | | | | E_(P) := C_(P) ×_(BP) S_(P) | +=======================================================================+ +-----------------------------------------------------------------------+ Candidate space C. The space of possible witnesses, constructions, models, proofs, explanations, states, histories, or realizations. Interface space B. The space of observables, constraints, boundary data, verification outputs, law conditions, tests, or target-interface data. Selected specification S → B. The selected datum, allowed condition, boundary constraint, target requirement, evidence record, or specification being imposed. Residue E_(P). The homotopy pullback C_(P) ×_(BP) S_(P). It is the unresolved content of the problem under the chosen presentation. +-----------------------------------------------------------------------+ | Formation rule: | | | | Γ ⊢ C : V_(τ) | | | | Γ ⊢ B : V_(τ) | | | | Γ ⊢ S : V_(τ) | | | | Γ ⊢ r : C → B | | | | Γ ⊢ s : S → B | | | | ────────────── | | | | Γ ⊢ (C →_(r) B ←_(s) S) : Prob_(τ) | | | | Residue rule: | | | | Γ ⊢ P = (C → B ← S) : Prob_(τ) | | | | ────────────── | | | | Γ ⊢ Res(P) := C ×_(B) S : V_(τ) | +=======================================================================+ +-----------------------------------------------------------------------+ ----------------------------------------------------------------------- Residue Regimes. A residue may be obstructed, ambiguous, or flat. A point of E_(P) certifies existence; flatness of E_(P) certifies canonical solvedness. Inhabitation and determinacy are distinct certificates. ----------------------------------------------------------------------- ----------------------------------------------------------------------- 6. Exact Normal Forms and Residue Localization Exact normal forms preserve unresolved content. They are not solutions unless the preserved residue is already flat. +-----------------------------------------------------------------------+ | For E : V_(τ), define: | | | | J_(τ)(E) := (E → 𝟙_(τ) ← 𝟙_(τ)) | | | | Δ_(τ)(E) := (E →_(id) E ←_(id) E) | | | | Computation rules: | | | | Res(J_(τ)(E)) ≃ E | | | | Res(Δ_(τ)(E)) ≃ E | +=======================================================================+ +-----------------------------------------------------------------------+ +-----------------------------------------------------------------------+ | Exact Continuation. For every typed residue E, both J_(τ)(E) and | | Δ_(τ)(E) are exact continuations. They preserve residue equivalently | | and therefore never delete unresolved content. | | | | Proof. By direct computation of the pullback defining the residue. | | The residue of E → 1 ← 1 is E, and the residue of E → E ← E along | | identities is E. | +=======================================================================+ +-----------------------------------------------------------------------+ +-----------------------------------------------------------------------+ | Residue Localization. For every type τ, typed formal problems | | localized at residue-equivalences are equivalent to typed residues: | | Prob_(τ)[W_(res)⁻¹] ≃ V_(τ). | | | | Proof. The residue functor Res_(τ) : Prob_(τ) → V_(τ) has the | | constant-cospan embedding Δ_(τ) as a fully faithful left adjoint in | | the relevant homotopy-coherent sense. The counit Δ_(τ)(Res(P)) → P is | | a residue-equivalence. Therefore every problem is identified, after | | localization, with its residue-only normal form. | +=======================================================================+ +-----------------------------------------------------------------------+ This theorem is the mathematical reason ARC can treat a problem by preserving its residue. Presentation matters operationally and semantically, but modulo residue-equivalence the problem content is exactly the residue. 7. Typed Carriers, Support, and Conservativity A type τ determines a carrier V_(τ). ARC distinguishes structured carrier-level claims from support-level claims. Support may be easier to compute, but support-level flatness does not automatically imply structured flatness. +-----------------------------------------------------------------------+ | Typed carrier data: | | | | V_(τ) — carrier category / type of objects | | | | 𝟙_(τ) — terminal object | | | | Pull_(τ) — finite homotopy pullbacks | | | | Map_(τ)(E,F) — mapping space | | | | U_(τ) : V_(τ) → 𝒮 — support functor | | | | Structured flatness: | | | | Flat_(τ)(E) := Equiv_(Vτ)(E, 𝟙_(τ)) | | | | Support flatness: | | | | SuppFlat_(τ)(E) := Equiv_(𝒮)(U_(τ)(E), 𝟙) | +=======================================================================+ +-----------------------------------------------------------------------+ +-----------------------------------------------------------------------+ | Support-conservativity for an arrow a : E → F: | | | | SC_(τ)(a) := Map(isEquiv_(𝒮)(U_(τ)(a)), isEquiv_(Vτ)(a)) | +=======================================================================+ +-----------------------------------------------------------------------+ ----------------------------------------------------------------------- Specific-Arrow Conservativity. Support flatness may be promoted to structured flatness only with a support-conservativity certificate for the exact arrow involved. A certificate for a similar arrow or a support-equivalent object cannot be substituted. ----------------------------------------------------------------------- ----------------------------------------------------------------------- This rule prevents a common collapse: treating a support-level summary as if it proved structure-level equivalence. ARC permits this transfer only through an explicit certificate space. 8. States, Registries, and Total Remainder An ARC state records active problem presentations, typed residue components, dependencies, evidence, parameters, and history. The registry is primary; aggregate remainder is derived from it. +-----------------------------------------------------------------------+ | State: | | | | α = (D_(α), P_(α), χ_(α), Reg_(α), Θ_(α), Data_(α), Hist_(α)) | | | | Registry: | | | | Reg_(α) = (J_(α), R_(α), τ_(α), Dep_(α), status_(α), prov_(α)) | | | | For each component j ∈ J_(α): | | | | R_(α)(j) : V_(τα(j)) | +=======================================================================+ +-----------------------------------------------------------------------+ +-----------------------------------------------------------------------+ | Aggregate support remainder: | | | | Rem(α) := lim_(j ∈ Jα) U_(τ(j)) R_(α)(j) | | | | Componentwise flatness: | | | | CompFlat(α) := ∏_(j ∈ Jα) Equiv_(Vτ(j))(R_(α)(j), 𝟙_(τ(j))) | +=======================================================================+ +-----------------------------------------------------------------------+ +-----------------------------------------------------------------------+ | Componentwise Flatness Implies Aggregate Flatness. If CompFlat(α) is | | inhabited, then Rem(α) is flat. | | | | Proof. Each component has terminal support. A homotopy limit of a | | terminal diagram is terminal. The converse is not generally valid | | without additional dependency and support-conservativity | | certificates. | +=======================================================================+ +-----------------------------------------------------------------------+ ARC uses the componentwise registry rather than only the aggregate remainder because dependencies can hide unresolved structure inside a flat-looking aggregate object. 9. Legal Transitions and Anti-Collapse A transition is legal only if it carries forward the old residue obligations. State-time runs forward, while residue-obligation maps backward. +-----------------------------------------------------------------------+ | A legal transition α → β is: | | | | T = (f, ρ, obl, trans, ac) | | | | where: | | | | f : raw transition α → β | | | | ρ : Rem(β) → Rem(α) | | | | obl : Obl(f,ρ) | | | | trans : Trans(ρ) | | | | ac : AntiCollapse(f) | | | | Therefore: | | | | Leg₁(α,β) := ∑_(f) ∑_(ρ) Obl(f,ρ) × Trans(ρ) × AntiCollapse(f) | +=======================================================================+ +-----------------------------------------------------------------------+ +-----------------------------------------------------------------------+ | For each old component j ∈ J_(α): | | | | AntiCollapse_(j)(f) := Flat_(j)(f) + Recon_(j)(f) + Ledger_(j)(f) | | | | Total anti-collapse: | | | | AntiCollapse(f) := ∏_(j ∈ Jα) AntiCollapse_(j)(f) | +=======================================================================+ +-----------------------------------------------------------------------+ Flat branch. The old component is solved by a structured flatness certificate. Reconstruction branch. The old component is reconstructed from auditable successor history, with an equivalence to the reconstructed object. Ledger branch. The old component is compared to a successor component through a typed comparison, obligation certificate, and transfer certificate. +-----------------------------------------------------------------------+ | Anti-Collapse Theorem. AntiCollapse(f) is inhabited exactly when no | | old registry component is silently deleted by f. | | | | Proof. The product over old components requires one lawful fate for | | each component. If any component lacks flatness, reconstruction, and | | ledgering, the product is empty and the transition is not legal. | +=======================================================================+ +-----------------------------------------------------------------------+ ----------------------------------------------------------------------- Compositionality of Legal Transitions. Legal transitions compose. If α → β and β → γ are legal, then the composite α → γ is legal, with backward comparison Rem(γ) → Rem(β) → Rem(α). ----------------------------------------------------------------------- ----------------------------------------------------------------------- 10. Failure Registry Failure is internal to ARC. A missing certificate is a residue, not a side note. The failure registry is stratified to avoid circularity: failures required to operate a failure layer appear one stage higher. +-----------------------------------------------------------------------+ | Stage-zero failure examples: | | | | SmallnessRes, AccessibilityRes, PresentationRes, | | PresentationAmbiguityRes, | | | | SelectionRes, CandidateGenerationRes, InterfaceSelectionRes, | | TypeLocalizationRes, | | | | TypeTranslationCoherenceRes, SupportConsRes, RuleCompleteRes, | | | | CanonRuleCompleteRes, ReconRes, LawRes, ObsRes, SubstrateRes, | | | | ResourceRes, FinalCoalgebraRes, RegimeDecisionRes | | | | Successor stage: | | | | FailReg_(n+1) := FailReg_(n) | | | | + OperateCert(FailReg_(n)) + AuditCert(FailReg_(n)) | | | | + TransportCert(FailReg_(n)) + ComposeCert(FailReg_(n)) | | | | + SmallnessCert(FailReg_(n)) + AccessibilityCert(FailReg_(n)) | | | | Omega stage, when certified: | | | | FailReg_(ω) := colim_(n<ω) FailReg_(n) | +=======================================================================+ +-----------------------------------------------------------------------+ ----------------------------------------------------------------------- Failure Closure. If FailReg_(ω) exists in the ambient foundation, then the stratified registry is closed under every generated finite-stage failure mode. If the colimit or its hypotheses are unavailable, that absence is itself registered one level higher. ----------------------------------------------------------------------- ----------------------------------------------------------------------- 11. Admissibility Compiler A raw name is not a generated object. ARC distinguishes namedness, generatedness, and context admission. This prevents proofs and constructions from smuggling in ungenerated maps, certificates, scopes, or presentations. +-----------------------------------------------------------------------+ | For a sort S and a named object x : S: | | | | Generatedness: | | | | Gen_(Γ)(S,x) := ∑_(t ∈ TermΓ(S)) Eq_(S)(t,x) | | | | Context admission: | | | | CtxAdm_(Γ)(S,x) := certificates that Γ, x:S is well formed | | | | Admissibility residue: | | | | Adm_(Γ)(S,x) := Gen_(Γ)(S,x) + CtxAdm_(Γ)(S,x) | +=======================================================================+ +-----------------------------------------------------------------------+ ----------------------------------------------------------------------- Admissibility branch Operational effect ----------------------------------- ----------------------------------- Generated branch x is represented by a term of G[Γ] and may be used internally. Context branch x becomes a variable in the extended context Γ,x:S; all dependent answers retain that scope. Failure branch Adm_(Γ)(S,x) is exact-normalized or registered as failure residue. ----------------------------------------------------------------------- ----------------------------------------------------------------------- Admissibility Soundness. Every accepted named object is generated from the current context or explicitly admitted by context extension. Every unaccepted name produces an admissibility residue. ----------------------------------------------------------------------- ----------------------------------------------------------------------- This rule applies to inputs, types, carrier objects, maps, presentations, residues, output doctrines, answer objects, scope maps, visible answers, certificates, transitions, rules, and practical closed-form claims. 12. Global Answer Objects and Descent An answer to one presentation is not automatically an answer to the input itself. ARC defines global answers as coherent sections over the presentation atlas, guarded against vacuous truth when no presentation exists. +-----------------------------------------------------------------------+ | Presentation space: | | | | Pres_(Γ)(X) := ∑_(p) PresAdm_(Γ)(X;p) | | | | For p ∈ Pres_(Γ)(X): | | | | p = (τ_(p), C_(p) → B_(p) ← S_(p)) | | | | E_(p) := C_(p) ×_(Bp) S_(p) | | | | Target-normalized residue: | | | | E_(p)^(λ) := L_(λ) e_(τp)(E_(p)) | +=======================================================================+ +-----------------------------------------------------------------------+ +-----------------------------------------------------------------------+ | Guarded global answer object: | | | | Glo_(F)^(λ)(X;Γ) := ∥Pres_(Γ)(X)∥ × ∏_(p ∈ PresΓ(X)) F(E_(p)^(λ)) | | | | Abbreviation: | | | | A₀ := Glo_(F)^(λ)(X;Γ) | +=======================================================================+ +-----------------------------------------------------------------------+ ----------------------------------------------------------------------- Presentation Bridge. A claimed F-answer is presentation-global for X exactly when it is a point of Glo_(F)^(λ)(X;Γ). A single answer at one presentation p is an answer to (X,p), not automatically to X. ----------------------------------------------------------------------- ----------------------------------------------------------------------- Local or interface-relative data are handled by descent. A local answer is globally usable only if the fiber of global answers over that local datum is flat, reconstructed, or ledgered. +-----------------------------------------------------------------------+ | Local-compatible answer object: | | | | Loc_(F)^(λ)(X;U_(•);Γ) := holim A_(F)^(λ)(U_(•);Γ) | | | | Restriction map: | | | | res_(U) : Glo_(F)^(λ)(X;Γ) → Loc_(F)^(λ)(X;U_(•);Γ) | | | | Descent residue for local datum ℓ: | | | | Desc_(F)^(λ)(X;U_(•);Γ;ℓ) := Glo_(F)^(λ)(X;Γ) ×_(LocFλ(X;U•;Γ)) {ℓ} | | | | Legal descent: | | | | LegalDesc := Flat(Desc) + Recon(Desc) + Ledger(Desc) | +=======================================================================+ +-----------------------------------------------------------------------+ ----------------------------------------------------------------------- Descent Soundness. Compatible local answer data may be reported as global exactly when LegalDesc is inhabited. Otherwise the answer remains local-scoped or becomes a registered descent obstruction. ----------------------------------------------------------------------- ----------------------------------------------------------------------- 13. Scope Logic and Answer Records ARC treats every answer as a value at a scope. The maximal declared answer object A₀ is relative to Γ, X, F, and λ. Any reported visible answer through a map from A₀ has an outside-scope residue. +-----------------------------------------------------------------------+ | Scope map: | | | | q : A₀ → A | | | | Visible answer: | | | | a : 𝟙 → A | | | | Outside-scope residue: | | | | Out_(q)(a) := A₀ ×_(A) {a} | | | | Canonical promotion: | | | | CanonProm_(q)(a) := Equiv(Out_(q)(a), 𝟙) | | | | Legal promotion: | | | | LegalProm_(q)(a) := Flat(Out_(q)(a)) + Recon(Out_(q)(a)) + | | Ledger(Out_(q)(a)) | +=======================================================================+ +-----------------------------------------------------------------------+ ----------------------------------------------------------------------- No Unscoped Answer. A visible answer a at scope q may be reported globally only with LegalProm_(q)(a). It may be reported as a naked canonical global answer only with CanonProm_(q)(a). Without either promotion or retained scope provenance, the output is invalid. ----------------------------------------------------------------------- ----------------------------------------------------------------------- ----------------------------------------------------------------------- Answer record form Required data ----------------------------------- ----------------------------------- Global a₀ : 𝟙 → A₀. Scoped q : A₀ → A, a : 𝟙 → A, and provenance retaining q. Promoted q : A₀ → A, a : 𝟙 → A, and LegalProm_(q)(a). Failure A label and registered certificate space C. ----------------------------------------------------------------------- +-----------------------------------------------------------------------+ | Total answer-record space: | | | | AnsRec(Γ,X,F,λ) := AnsGlobal + AnsScoped + AnsPromoted + AnsFailure | +=======================================================================+ +-----------------------------------------------------------------------+ 13.1 Composite Scope Loss If an answer is produced through several scopes, the total outside-scope residue is the fiber of the composite. Stagewise loss decomposes by pullback associativity. +-----------------------------------------------------------------------+ | For A →f B →g C and c : 𝟙 → C: | | | | A ×_(C) {c} ≃ Σ[b ∈ B ×_(C) {c}] (A ×_(B) {b}) | | | | For an answer stack A₀ → A₁ → ⋯ → Aₙ and aₙ : 𝟙 → Aₙ: | | | | OutStack(aₙ) := A₀ ×_(Aₙ) {aₙ} | +=======================================================================+ +-----------------------------------------------------------------------+ ----------------------------------------------------------------------- Composite Loss Theorem. Total answer loss decomposes into the dependent aggregation of all stagewise losses. Stagewise accounting is sufficient for global accounting; a direct certificate for the composite fiber is also sufficient. ----------------------------------------------------------------------- ----------------------------------------------------------------------- 14. Practical Closed Forms A practical form is a representation with certified loss accounting. A finite summary, statistic, model, memory, formula, numerical answer, or simplified expression is not a closed form merely because it is useful or compact. +-----------------------------------------------------------------------+ | Practical compression: | | | | q : E → R | | | | Loss fiber over r : 𝟙 → R: | | | | Loss_(q)(r) := E ×_(R) {r} | | | | Selected-value legality: | | | | LegalValuePCF(q,r) := Flat(Loss_(q)(r)) + Recon(Loss_(q)(r)) + | | Ledger(Loss_(q)(r)) | | | | Representation-level legality: | | | | LegalRepPCF(q) := ∏_(r ∈ R) (Flat(Loss_(q)(r)) + Recon(Loss_(q)(r)) + | | Ledger(Loss_(q)(r))) | +=======================================================================+ +-----------------------------------------------------------------------+ ----------------------------------------------------------------------- Practical Closed Form Criterion. A selected practical value r is globally reportable relative to the declared base object E, or to A0 when q : A0 → R, exactly when LegalValuePCF(q,r) is inhabited. The whole representation R is a legal practical closed form exactly when LegalRepPCF(q) is inhabited. ----------------------------------------------------------------------- ----------------------------------------------------------------------- Exact mode always preserves the full residue. Practical mode is useful only when it accounts for what it omits. 15. Proof Trees and Closure Proof is modeled as a generated object, not as an informal explanation. A proof tree is sound only through a rule system whose rules carry closure-transfer data. +-----------------------------------------------------------------------+ | For a certified rule system R, define the proof-tree polynomial: | | | | (Φ_(R) X)(α) := ∐_(n ≥ 0) ∐_(β1,…,βn) R_(n)(α;β₁,…,β_(n)) × ∏_(i) | | X(β_(i)) | | | | Assuming accessibility: | | | | Sol_(R) := μΦ_(R) | | | | Soundness map: | | | | sound_(α) : Sol_(R)(α) → Cl(I(α)) | +=======================================================================+ +-----------------------------------------------------------------------+ +-----------------------------------------------------------------------+ | Proof-Tree Soundness. Every proof tree maps to a closure certificate. | | If Sol_(R)(α) is inhabited, then α is closed under the closure | | doctrine represented by Cl. | | | | Proof. By initial-algebra recursion. Each proof node contains a | | certified rule, and each certified rule contains the closure map from | | child closures to parent closure. | +=======================================================================+ +-----------------------------------------------------------------------+ +-----------------------------------------------------------------------+ | Rule completeness: | | | | RuleComplete_(R) := ∏_(α) Map(∥Cl(I(α))∥, ∥Sol_(R)(α)∥) | | | | Canonical rule completeness: | | | | CanonRuleComplete_(R) := ∏_(α) Equiv(Sol_(R)(α), Cl(I(α))) | +=======================================================================+ +-----------------------------------------------------------------------+ Soundness is built into the proof tree. Completeness is never assumed. Missing proof completeness is a certificate residue. 16. Models and the Term Generator An ARC model interprets the entire calculus: types, carriers, cospans, residues, exact forms, registries, transitions, proof trees, answer scopes, admissibility, and failure strata. A morphism of ARC models preserves this structure up to coherent equivalence. ----------------------------------------------------------------------- ARC model component Required interpretation ----------------------------------- ----------------------------------- Types and carriers A type object and a carrier V_(τ) for each type, with terminal object, pullbacks, support, and mapping spaces. Formal problems Cospans C → B ← S and residue pullbacks C ×_(B) S. Exact forms J_(τ) and Δ_(τ) with residue-equivalence computation rules. States and registries Audited states, typed residue components, dependencies, and histories. Legal transitions Raw transitions, backward residue maps, obligations, transfers, and anti-collapse. Proofs and closure Rule systems, proof-tree initial algebras, soundness maps, and completeness certificate spaces. Answers and scopes Global answer objects, scope maps, outside-scope residues, promotion certificates, and answer records. Failures Stratified failure registries and failure-registration constructors. ----------------------------------------------------------------------- The term generator G[Γ] is the freely generated ARC model over the context Γ. It starts with the variables of Γ, closes under all constructors, and quotients by the homotopy-coherent equations required by ARC. +-----------------------------------------------------------------------+ | Generated constructors include: | | | | type formation; typed comparison; cospan formation; residue pullback; | | J; Δ; readout fiber; conjunction; alternative; dependent sequencing; | | universal aggregation; compression loss; registry formation; | | anti-collapse; obligation; legal transition; proof-tree construction; | | reconstruction fiber; substrate fiber; calibration fiber; law | | residue; failure successor; exact normalization; presentation atlas; | | global answer section; scope map; outside-scope residue; legal | | promotion; answer record; admissibility residue. | +=======================================================================+ +-----------------------------------------------------------------------+ 17. Initiality Initiality states that G[Γ] is the canonical audited generator over Γ. Any other system satisfying the ARC laws receives a unique structure-preserving interpretation of G[Γ]. +-----------------------------------------------------------------------+ | Let ARCMod_(Γ) be the infinity-category of ARC models with an | | interpretation of Γ. | | | | Initiality theorem: | | | | Map_(ARCModΓ)(G[Γ], A) ≃ 𝟙 | | | | for every ARC model A over Γ. | +=======================================================================+ +-----------------------------------------------------------------------+ +-----------------------------------------------------------------------+ | Initiality Theorem. For every context Γ, G[Γ] is homotopy-initial in | | ARCMod_(Γ). | | | | Proof. Existence is by recursive interpretation of generated terms in | | any target ARC model. Well-definedness follows because every equation | | imposed in G[Γ] is required to hold in every ARC model. Uniqueness | | follows by induction on term formation: any two structure-preserving | | maps agree on Γ and must agree on every generated constructor output | | up to contractible coherence. | +=======================================================================+ +-----------------------------------------------------------------------+ Initiality does not imply a universal flat solver. If a universal flat solver existed, every target ARC model would have to interpret it as a flatness certificate for every residue. Target models may contain empty or noncontractible residues, so such a term cannot exist. ----------------------------------------------------------------------- Universal Exact Continuation. Exact continuation exists for every residue, but flat solution does not. The terms J_(τ)(E) and Δ_(τ)(E) are universal because they preserve residue; they do not assert that the residue is terminal. ----------------------------------------------------------------------- ----------------------------------------------------------------------- 18. Non-Collapse, Answer Soundness, and Operational Adequacy The major soundness theorems are structural consequences of the formation rules. Every rule either preserves residue exactly, accounts for loss fibers, transfers closure with a certificate, retains scope, or registers failure. +-----------------------------------------------------------------------+ | Non-Collapse Soundness. Every derivable ARC answer either preserves | | every generated distinction, assigns each erased distinction a lawful | | fate, or registers the missing fate as failure residue. | | | | Proof. Proceed by induction on derivations. Cospan formation | | generates residue. Exact normal forms preserve residue. Compression | | computes loss fibers. Scope promotion computes outside-scope fibers. | | Descent computes descent fibers. Legal transition requires flatness, | | reconstruction, or ledgering of every old component. Admissibility | | prevents ungenerated names. Failure registration converts missing | | certificates into typed residues. | +=======================================================================+ +-----------------------------------------------------------------------+ +-----------------------------------------------------------------------+ | Answer Soundness. If Γ ⊢ R : AnsRec(Γ,X,F,λ), then R is exactly one | | of: a global answer, a scoped answer with provenance, a legally | | promoted answer with outside-scope fiber accounting, or a registered | | failure residue. | | | | Proof. The answer-record type is defined as the coproduct of those | | four constructors. No fifth constructor exists. | +=======================================================================+ +-----------------------------------------------------------------------+ ----------------------------------------------------------------------- Operational Adequacy. Every validated operational output is derivable as an ARC answer record. Solve mode requires structured flatness, Exact mode returns residue-preserving normal form, Practical mode requires loss-fiber accounting, and Explore mode returns legal futures. ----------------------------------------------------------------------- ----------------------------------------------------------------------- 19. Completion Certificate and Obstruction Register ARC 1.0 is complete as a formal mathematical specification relative to its ambient foundation and the explicit certificate obligations below. When an implementation lacks one of these obligations, ARC does not collapse; it registers the missing certificate as residue. ----------------------------------------------------------------------- ARCComplete := (Foundation, Judgments, FormationRules, ComputationRules, AdmissibilityCompiler, ModelSemantics, TermModel, Initiality, NonCollapseSoundness, ScopeSoundness, OperationalAdequacy, FailureClosure) ----------------------------------------------------------------------- ----------------------------------------------------------------------- ----------------------------------------------------------------------- Meta-obligation Status inside ARC ----------------------------------- ----------------------------------- UniverseCert Required to bound carriers, syntax, and certificate spaces. SmallnessCert Required for small indexing categories, registries, and presentation spaces. AccessibilityCert Required for generated localizations, initial algebras, and some colimits. LocalizationCert Required when a generated type is a reflective localization. TypeTranslationCoherenceCert Required for cross-type comparison and ledger composition. HITQuotientCert Required for a proof-assistant implementation of homotopy-coherent quotient syntax. InitialAlgebraCert Required for proof-tree objects Sol_(R) = μ Φ_(R). FinalCoalgebraCert Required for infinite legal process objects. SequentialColimitCert Required for FailReg_(ω). ----------------------------------------------------------------------- ----------------------------------------------------------------------- Completion is obstruction-nullity: every generated survivor is legally neutralized, lawfully supported, preserved, or registered as exact obstruction. ----------------------------------------------------------------------- ----------------------------------------------------------------------- Appendix A. Core Inference Rules A.1 Problem and Residue Rules +-----------------------------------------------------------------------+ | Problem formation: | | | | Γ ⊢ C : V_(τ) | | | | Γ ⊢ B : V_(τ) | | | | Γ ⊢ S : V_(τ) | | | | Γ ⊢ r : C → B | | | | Γ ⊢ s : S → B | | | | ────────────── | | | | Γ ⊢ (C →_(r) B ←_(s) S) : Prob_(τ) | | | | Residue formation: | | | | Γ ⊢ P = (C → B ← S) : Prob_(τ) | | | | ────────────── | | | | Γ ⊢ Res(P) := C ×_(B) S : V_(τ) | +=======================================================================+ +-----------------------------------------------------------------------+ A.2 Exact Form Rules +-----------------------------------------------------------------------+ | Exact forms: | | | | Γ ⊢ E : V_(τ) | | | | ────────────── | | | | Γ ⊢ J_(τ)(E) : Prob_(τ) | | | | Γ ⊢ Δ_(τ)(E) : Prob_(τ) | | | | Computation: | | | | Res(J_(τ)(E)) ≃ E | | | | Res(Δ_(τ)(E)) ≃ E | +=======================================================================+ +-----------------------------------------------------------------------+ A.3 Legal Transition Rule +-----------------------------------------------------------------------+ | Legal transition: | | | | Γ ⊢ f : Raw(α,β) | | | | Γ ⊢ ρ : Rem(β) → Rem(α) | | | | Γ ⊢ o : Obl(f,ρ) | | | | Γ ⊢ t : Trans(ρ) | | | | Γ ⊢ a : AntiCollapse(f) | | | | ────────────── | | | | Γ ⊢ (f,ρ,o,t,a) : Leg₁(α,β) | +=======================================================================+ +-----------------------------------------------------------------------+ A.4 Scope and Answer Rules +-----------------------------------------------------------------------+ | Scoped answer: | | | | Γ ⊢scope q : A₀ → A | | | | Γ ⊢ a : 𝟙 → A | | | | Γ ⊢ retain(q,a) | | | | ────────────── | | | | Γ ⊢ Scoped(q,a,retain) : AnsRec(Γ,X,F,λ) | | | | Promoted answer: | | | | Γ ⊢scope q : A₀ → A | | | | Γ ⊢ a : 𝟙 → A | | | | Γ ⊢ c : LegalProm_(q)(a) | | | | ────────────── | | | | Γ ⊢ Promoted(q,a,c) : AnsRec(Γ,X,F,λ) | | | | Failure answer: | | | | Γ ⊢ C : CertSpace | | | | Γ ⊢ Registered(label,C) | | | | ────────────── | | | | Γ ⊢ Failure(label,C) : AnsRec(Γ,X,F,λ) | +=======================================================================+ +-----------------------------------------------------------------------+ A.5 Admissibility Rule +-----------------------------------------------------------------------+ | Admissibility: | | | | Adm_(Γ)(S,x) := Gen_(Γ)(S,x) + CtxAdm_(Γ)(S,x) | | | | Generated branch: | | | | g : Gen_(Γ)(S,x) | | | | ────────────── | | | | Γ ⊢ x : S | | | | Context branch: | | | | a : CtxAdm_(Γ)(S,x) | | | | ────────────── | | | | Γ,x:S ⊢ x : S | | | | Failure branch: | | | | Adm_(Γ)(S,x) required but no branch supplied | | | | ────────────── | | | | Γ ⊢ Failure(AdmissibilityRes, Adm_(Γ)(S,x)) | +=======================================================================+ +-----------------------------------------------------------------------+ Appendix B. Theorem Index ----------------------------------------------------------------------- Theorem Claim ----------------------------------- ----------------------------------- Residue Localization Formal problems modulo residue-equivalence are typed residues. Exact Continuation J_(τ)(E) and Δ_(τ)(E) preserve residue for every typed residue E. Specific-Arrow Conservativity Support flatness promotes to structured flatness only through the exact support-conservativity certificate. Componentwise Flatness Componentwise registry flatness implies aggregate remainder flatness. Anti-Collapse A legal transition deletes no old residue silently. Failure Closure Stratified failure registries close generated finite-stage failures. Admissibility Soundness No name is usable without generatedness, context admission, or failure registration. Presentation Bridge Global answers are coherent sections over the presentation atlas. Descent Soundness Local answers globalize only through a flat, reconstructed, or ledgered descent fiber. No Unscoped Answer A visible scoped answer promotes only through outside-scope fiber accounting. Composite Loss Total scope loss decomposes by pullback associativity. Practical Closed Form A representation is closed exactly when all selected loss fibers have lawful fates. Proof-Tree Soundness Proof trees map to closure certificates. Initiality G[Γ] is homotopy-initial in ARCMod_(Γ). Non-Collapse Soundness Every derivable answer preserves, accounts for, or registers all erased distinctions. Answer Soundness Every answer record is global, scoped, promoted, or failure-registered. Operational Adequacy Every validated operational output is derivable as an answer record. ----------------------------------------------------------------------- Appendix C. Implementation Notes This manuscript is a formal specification. A machine-checked implementation requires selecting a proof assistant or formal foundation capable of representing the relevant homotopy-coherent structures, or else replacing those structures with a stricter 1-categorical or set-level fragment. A practical mechanization can proceed module by module. A minimal first implementation may restrict carriers to ordinary types or sets, replace homotopy pullbacks with ordinary pullbacks, and treat certificate spaces as ordinary propositions or types. The full ARC system is recovered by adding higher identity structure, homotopy coherence, dependent sums and products, reflective localizations, and higher-categorical model semantics. 1. Implement the core cospan and residue calculus: Prob_(τ), Res(P), J, Δ, and residue-equivalence. 2. Implement certificate spaces for flatness, reconstruction, ledgering, and failure registration. 3. Implement registries and legal transitions with anti-collapse products over old components. 4. Implement scope maps, outside-scope residues, answer records, and legal promotion. 5. Implement admissibility: generatedness, context admission, and failure registration for names. 6. Implement proof trees as initial algebras only after the required accessibility hypotheses are fixed. 7. State and prove initiality for the chosen syntax/model category. The implementation should preserve the governing invariant: every constructor that forgets structure must produce an explicit fiber or a certificate explaining the fate of that fiber. This invariant is the central regression test for any implementation of ARC. Final Compression +-----------------------------------------------------------------------+ | A problem is a cospan: | | | | C → B ← S | | | | Its content is a pullback residue: | | | | E = C ×_(B) S | | | | A solution is flatness of that residue. | | | | An exact answer preserves that residue. | | | | A practical answer accounts for every loss fiber. | | | | A scoped answer retains its scope. | | | | A global answer descends across presentations and local data. | | | | A legal transition preserves old residue by flatness, reconstruction, | | or ledgering. | | | | A missing certificate is residue. | | | | A generated object must be admissible. | | | | The canonical generator is initial among all systems obeying these | | laws. | +=======================================================================+ +-----------------------------------------------------------------------+ ----------------------------------------------------------------------- ARC 1.0: the initial non-collapsing audited residue calculus. ----------------------------------------------------------------------- -----------------------------------------------------------------------