Paper deep dive
Beyond Natural Language: An Agent-Native Language for Autonomous Science
Yifeng He, Jiachen Liu
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%
Last extracted: 9/23/2026, 4:31:08 AM
Summary
The paper introduces Lara, a machine-checkable language and protocol designed for autonomous scientific agents to manage research claims. Unlike natural language, Lara formalizes claims, evidence, assumptions, and objections into executable artifacts. A deterministic checker evaluates these programs, assigning statuses (justified, defeated, contested, gap) based on Dung's argumentation framework. The system supports cross-context argument transport via 'bridges' and is mechanized in Lean 4, providing a robust epistemic kernel for AI-driven scientific inquiry.
Entities (12)
Relation Signals (11)
Lara → createdby → Yifeng He
confidence 95% · Authors listed: Yifeng He and Jiachen Liu
Lara → createdby → Jiachen Liu
confidence 95% · Authors listed: Yifeng He and Jiachen Liu
Lara → providesstatus → justified
confidence 95% · assigning each claim a reproducible status: 'justified'...
Lara → providesstatus → defeated
confidence 95% · assigning each claim a reproducible status: ... 'defeated'...
Lara → providesstatus → contested
confidence 95% · assigning each claim a reproducible status: ... 'contested'...
Lara → providesstatus → gap
confidence 95% · assigning each claim a reproducible status: ... or 'gap'
Lara → mechanizedin → Lean 4
confidence 92% · mechanize the semantic guarantees in Lean 4 (roughly 117,000 lines)
Lara → affiliatedwith → ARA Lab
confidence 90% · Authors affiliation: ARA Lab
Lara → enables → autonomous science
confidence 90% · Lara provides an epistemic kernel for autonomous science
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:As autonomous AI agents take on every stage of scientific inquiry, research output is expanding far beyond human review capacity. Yet scientific communication still relies on natural-language prose: an informal medium prone to ambiguity, hidden assumptions, and untracked limitations that machines cannot reliably audit. We introduce Lara, a machine-checkable language and protocol for checking and revising support for research claims. By turning research arguments into executable artifacts, Lara provides an epistemic kernel for autonomous science: it enables automated validation pipelines for research agents, lets declared bridges connect arguments across papers into an auditable network, and allows both humans and machines to recheck the standing of an encoded claim in milliseconds. In a Lara program, authors explicitly declare their claims, supporting evidence and assumptions, and known objections or limitations. A lightweight, deterministic checker adjudicates these interactions, assigning each claim a reproducible status: "justified", "defeated", "contested", or "gap", which marks a claim whose support is incomplete and locates the unanswered question. Case studies cover empirical review, a philosophical debate without measurements, and the loss of support when an assumed axiom is withdrawn. We establish the metatheory of claim checking and cross-context argument transport, and mechanize the semantic guarantees in Lean 4 (roughly 117,000 lines), leaving three arguments on paper. The audited public metatheory is "sorry"-free and uses only Lean's three standard axioms; some executable examples additionally trust native evaluation.
Tags
Links
- Source: https://arxiv.org/abs/2609.25421v1
- Canonical: https://arxiv.org/abs/2609.25421v1
Trouble viewing inline? Open PDF directly →
Full Text
237,360 characters extracted from source content.
Expand or collapse full text
Beyond Natural Language: An Agent-Native Language for Autonomous Science Yifeng He and Jiachen Liu ARA Lab As autonomous AI agents take on every stage of scientific inquiry, research output is expanding far beyond human review capacity. Yet scientific communication still relies on natural-language prose: an informal medium prone to ambiguity, hidden assumptions, and untracked limitations that machines cannot reliably audit. We introduce Lara, a machine-checkable language and protocol for checking and revising support for research claims. By turning research arguments into executable artifacts, Lara provides an epistemic kernel for autonomous science: it enables automated validation pipelines for research agents, lets declared bridges connect arguments across papers into an auditable network, and allows both humans and machines to recheck the standing of an encoded claim in milliseconds. In a Lara program, authors explicitly declare their claims, supporting evidence and assumptions, and known objections or limitations. A lightweight, deterministic checker adjudicates these interactions, assigning each claim a reproducible status: justified, defeated, contested, or gap, which marks a claim whose support is incomplete and locates the unanswered question. Case studies cover empirical review, a philosophical debate without measurements, and the loss of support when an assumed axiom is withdrawn. We establish the metatheory of claim checking and cross-context argument transport, and mechanize the semantic guarantees in Lean 4 (roughly 117 000117\,000 lines), leaving three arguments on paper. The audited public metatheory is sorry-free and uses only Lean’s three standard axioms; some executable examples additionally trust native evaluation. Code: github.com/ARA-Labs/Lara 1 Introduction Scientific progress depends on accumulating verifiable knowledge through rigorous peer critique. For more than three centuries, the research paper has served as the universal medium for this critique. The genre assumes a human on each side: an author compresses an investigation into a linear narrative that states claims and cites selected evidence, while a reader reconstructs the inferential links that the narrative leaves implicit. Medawar (1996) famously argued that this genre misrepresents inquiry itself: the published narrative preserves the successful path and discards the dead ends and iterative revisions that produced it (Howitt and Wilson, 2014; Tregoning, 2026). The genre nonetheless endured because human judgment bridged the gap: reviewers read the prose, weighed the tables, and decided holistically whether the argument held together. Such a verdict is un-auditable: it cannot locate a missing premise, and it cannot distinguish a claim that was contested from a claim that was never supported. The rise of autonomous AI agents shatters this human-centric equilibrium. Language-model agents now carry projects from hypothesis generation to experiment execution and manuscript drafting (Lu et al., 2024; Aygün et al., 2026; Tang et al., 2026). Inside OpenAI’s research organization, agents already perform 3.1 workdays of research for every workday of human labor (OpenAI, 2026). Beyond the lab, annual submissions to flagship AI venues now exceed 20 00020\,000 papers each, forcing peer review to automate in response: venues now deploy machine reviews across major tracks (Biswas et al., 2026) or mandate end-to-end AI authorship and review (Bianchi et al., 2026). In this regime, natural language fails as a communication protocol: it is an informal medium prone to ambiguity, unstated assumptions, and untracked failures that machines cannot reliably audit. When machines write claims and machines judge them through prose, no step in the loop can be checked. The same shift supplies the remedy. Software engineering absorbed the same surge in productivity when code generation became cheap: verification migrated from manual code inspection into automated type checkers, test suites, and continuous integration pipelines. Autonomous scientific agents now capture the complete computational substrate of discovery: structured datasets, execution logs, code repositories, and failed attempts (Liu et al., 2026). The full record of an investigation is now digital and machine-readable. We no longer need to force machines to compress structured discoveries into informal prose only for other machines to guess their meaning; instead, we can formalize research validation itself as an executable computing discipline. Realizing executable verification for science requires resolving one obstacle. In formal mathematics, proof certificates are factive and monotonic (Necula, 1997; Miller, 2015): once a proof checker accepts a theorem, the conclusion holds under its axioms, and no subsequent discovery can retract it while its assumptions remain fixed. Research arguments can also be defeasible. A later experiment can invalidate a scientific conclusion even when its original premises and inference steps remain well-formed. For instance, an inequality between two measured benchmark scores (0.74>0.710.74>0.71) remains an arithmetic fact; yet if a subsequent audit exposes unaddressed confounders or a shifted test distribution (Recht et al., 2019), that arithmetic ceases to justify the claim that one method outperforms another. A formal system for research claims must therefore obey a governing design principle: it must separate checking the validity of a support term from accepting the claim it supports. We introduce Lara, a machine-checkable language and protocol for checking and revising support for research claims that operationalizes this principle. Its premises may be measurements, attributed statements, or explicit assumptions. A philosophical objection can defeat an inference, and a deductive argument can lose its reusable support when a target context withholds an assumption. The same distinction between checked support and accepted claims applies in each case. By transforming research arguments into executable, checkable programs, Lara enables four capabilities: 1. Continuous integration for autonomous science: AI research agents can run automated regression tests on their own hypotheses, based on their declared claims and support, obtaining deterministic verdicts from a checker rather than relying on noisy prompt-based evaluations. Lara thus serves as an epistemic kernel for research agents, ensuring they build subsequent research on verified findings. 2. Auditable links across the literature: Instead of treating papers as isolated documents, declared bridges across contexts connect findings into an auditable network; when a later world declares a distribution shift or counterexample as a typed attack on a transported argument, a modal query from the earlier world reports that the claim is no longer justified in every accessible context. A literature-scale knowledge graph over checked claims is a possible downstream application. 3. Objections and limitations as first-class assets: Authors and agents declare challenges to premises, conclusions, or inference steps as typed attacks. A failed experiment or a philosophical objection can therefore defeat the support it targets, while a claim with no complete support stays distinct from one whose support is defeated. 4. Separating checked deductions from revisable claims: Strict backends certify steps relative to declared premises and theories. The surrounding argument records how those steps support a claim and whether that support survives challenges or a change of assumptions. A certified numerical comparison, for example, can remain valid after an objection defeats the claimed empirical improvement. At a high level, a Lara program acts as a research claim certificate. Authors declare their claims (pairing natural-language prose with formal targets), evidence leaves tagged with provenance, inference steps, and typed attacks. Inferences split into two tiers: strict deductive steps delegate proof obligations to registered backends (such as rational arithmetic or natural deduction), while defeasible steps instantiate policy-governed schemes that must explicitly answer mandatory critical questions (such as randomization, sample power, or the scope of an assumed premise) or face immediate checker rejection. Attacks target specific structural positions: rebutting conclusions, undermining evidence leaves, or undercutting inference rules when exception conditions trigger. A support term that checks does not yet settle its claim: another argument can defeat it, and a third can reinstate it by defeating the attacker. A lightweight, deterministic checker therefore compiles accepted programs into a Dung argumentation framework (Dung, 1995), whose grounded evaluation assigns each claim a status: justified when complete support survives all challenges, defeated when all support is overturned, contested when arguments reach an undecided deadlock, or gap when no complete support argument exists. Across distinct papers or environments, a conservative possible-world semantics models each accepted program as a world, employing declared structural bridges to transport support terms while relying on an executable attack-bisimulation checker to decide when claim statuses survive the translation. A status is relative to the signature, policy, backend registry, and admitted evidence. The checker decides whether the declared support stands; it does not establish that a formal atom faithfully represents a prose claim or that an admitted measurement is accurate. Transport is guarded in the same way: structural bridges preserve checked support, but a target world may contain additional attackers, and a mechanized example transports support while the claim changes from justified to defeated. The case studies make this scope concrete (Appendix D). Alongside empirical review and cross-paper comparisons, a philosophy-of-mathematics debate uses only assumed and attested premises to exhibit unresolved disagreement and reinstatement. An axiom-withdrawal example combines certified hypothesis reuse with a Lean witness showing why support cannot cross into a context that withholds its premise. These demonstrations instantiate the existing calculus without adding domain-specific kernel rules. We make the following contributions: • A typed claim-support calculus: We formulate the core language and protocol with explicit critical-question obligations, typed positional attacks, and isolated strict backends (Section 3). • Metatheory and status preservation: We prove status preservation between direct source semantics and compiled argumentation frameworks, establish dependency accountability and backend replacement, and develop an update calculus governing status transitions (Section 6). • Cross-context possible-world semantics: We formalize modal observations over checked contexts, establish exact support transport, and provide a sound and complete executable decider for status-preserving attack bisimulations (Section 5 and Section 6.8). • Mechanization and empirical evaluation: We mechanize the semantic results in Lean 4 across 144 files and roughly 117 000117\,000 lines. The audited public metatheory uses only Lean’s standard three axioms; some executable examples additionally trust native evaluation, and three arguments remain on paper (Section 6). We validate a Haskell checker through differential testing on 673 verdict-bearing and 66 malformed inputs, including systematic mutation suites (Section 7). 2 Background and overview A paper reports that a new method works better than an existing one. Before building on that result, another scientist needs to understand how the comparison was made, whether any objections remain unanswered, and whether the result applies in the setting they care about. Lara makes these relationships explicit so that a checker can follow them, drawing on three ideas: research records that agents read and write, formal argumentation over reasons and objections, and comparison across possible worlds. A running example then shows how a Lara program expresses them, and a trust architecture sets out what the checker guarantees. 2.1 Background 2.1.1 Agent-native research: records that agents read and write A scientist continuing someone else’s investigation needs access to the work behind its conclusions: the data, the analysis, the experimental conditions, and the reasons for abandoning earlier approaches. An AI research agent, a system that uses tools to carry out research tasks, needs this information too. We call a record agent-native when it organizes the information for an agent to find and use directly. A claim has a name, its evidence points to specific results, and the record links those results to the procedures that produced them. The record serves the role of a laboratory notebook whose entries connect directly to the relevant data and code. Agents now write these records as well as read them. Lu et al. (2024) report a system that generates a research idea, writes the code, runs the experiment, and drafts the manuscript, then repeats the cycle on its own output. Earlier tools helped a human with a single step; this system runs the whole loop. Each pass builds on what an earlier pass recorded, which places the record between two machines. Liu et al. (2026) propose the Agent-Native Research Artifact (ARA) format for such records. An ARA brings together claims and methods, code and configurations, evidence, and a history of the investigation, including failed experiments and abandoned approaches. For example, it can preserve both a reported improvement and a later experiment where the improvement disappeared. A scientist or an agent building on that result can then inspect the conditions of both experiments instead of seeing only the successful one. The record stores both experiments but leaves their relationship unstated. The later experiment might expose a flaw in the original comparison, or it might concern a different population. Whoever continues the work has no declared answer to check. Lara lets an author state the proposed relationship and makes its consequences checkable. ARA supplies one source of these records; authors and agents can also write Lara programs directly. The checker reads a program the same way whichever of them wrote it. 2.1.2 Formal argumentation: reasons and objections A measured improvement, a claim about that improvement, and a reason to believe the claim are different things. The measurement is evidence. The statement that the new method works better is a claim. An argument connects the evidence to the claim, for example by explaining why the two methods were compared under conditions that make the result meaningful. Scientific review tests these connections. A reviewer might object that the two methods were tested under different conditions, so their reported scores do not establish the claimed improvement. The author might respond with records showing that the reviewer consulted an outdated protocol. If that response defeats the objection, the original argument can stand again. This is defeasible reasoning: a reason for accepting a claim can lose its force when a challenge appears, and regain it when that challenge is answered. Formal argumentation represents this exchange as a diagram of arguments and the objections between them (Dung, 1995). Each node represents an argument; an arrow points from an objection to the argument it challenges. Such a challenge is called an attack. An abstract argumentation framework records this pattern while setting aside the arguments’ internal details. Its semantics specifies the rules for deciding which arguments to accept. Lara uses grounded semantics: begin with arguments that face no declared attack, mark the arguments they attack as defeated, and accept further arguments once all their attackers have been defeated. Continue until no decision changes. Two arguments that only attack each other remain undecided; the rules do not choose a winner without further grounds. Lara adds a check before this evaluation: each argument must contain the support its stated inference rule requires, and each attack must be allowed by the declared rules. The checker then reports one of four statuses. A claim is justified when at least one complete support argument survives, defeated when complete support exists but every such argument is defeated, and contested when no support argument is accepted and some remain undecided. A claim with no complete support argument at all is gap. The premises need not be measurements: an argument may instead use an explicit assumption or an attributed position. The policy specifies which inferences and objections these premises license; the philosophy example in Section D.4 exercises this case. These statuses describe the declared case for a claim. They do not establish that its measurements are accurate or that the claim is true. 2.1.3 Possible worlds: comparing research settings A claim may have convincing support in one research record and face an unanswered objection in another. A scientist comparing them needs to keep track of which evidence and assumptions each conclusion rests on. Possible-world semantics provides a way to do this: evaluate a statement separately in each specified situation, called a world, and then ask how its standing differs across worlds (Kripke, 1963). Logicians study the languages that describe such situations as modal logic (Blackburn et al., 2001). In Lara, a world is a program that passes the checker. It may express a research record or an argument under a chosen set of assumptions. It contains evidence, arguments, and challenges, together with the rules used to assess them. A world can combine material from several papers; it need not correspond to one paper. To compare worlds, a researcher declares a bridge that specifies which comparison to make and how a claim in one record corresponds to a claim in the other. These connections form the model’s accessibility relation: the set of comparisons its queries use. Choosing an appropriate comparison remains the researcher’s responsibility. A researcher can now put two questions to the checker. Is the claim justified in some compared record? Is it justified in every compared record? Modal logic calls these the diamond and box queries. If one compared record justifies the claim and another defeats it, the answer to the first question is yes and to the second is no. The comparison leaves the original record’s own verdict intact. The second question tests robustness, and a claim cannot pass it without at least one declared comparison. We depict both operations in Figure 1: following reasons and objections within a record, and comparing claim statuses across records. The formal definitions follow in Section 4 and Section 5. Reasons within one record Response to the objection accepted Objection to the comparison defeated Argument for the improvement accepted challengeschallenges Comparisons between records Source research record Record 1 claim: defeated Record 2 claim: justified declaredcomparisonsjustified in some compared record: yesjustified in every compared record: no Figure 1: Following a debate and comparing research records are different operations. Left: each box is an argument. With no further challenges, the response defeats the objection, so the original argument is accepted again. Right: each box is a whole research record. The same claim is justified in one compared record and defeated in the other, so it is justified somewhere but not everywhere among these comparisons. Comparing records does not rewrite the original record’s verdict. 2.2 A running example We now encode the distinction between missing and defeated support. An experiment report asserts that method M improves accuracy on distribution D, on the strength of one measured effect over a baseline M0M_0; the same artifact’s exploration trace records a dead end in which the effect vanished under a distribution shift. We give the artifact’s support for that claim as a Lara program in Figure 2, in two runs: run 1 leaves the mandatory external-validity question undischarged, and run 2, shown in full, answers it. This policy requires off-distribution evidence even for the stated claim on D; that requirement is a policy choice. Both programs and their expected reports ship in the artifact. ⬇ 1 artifact paper_17 at sha256:a... 2 policy empirical-v3 3 use backends [nd@1, ord@1] 4 let base_score = 0.71 5 let ours_score = 0.74 6 claim c1 7 nl = "Method M improves accuracy on distribution D" 8 formal = improves(M, accuracy, D) 9 binding = author = alice, audit-status = reviewed 10 claim c2 11 nl = "The baseline accuracy base_score is strictly below ours_score" 12 formal = num_lt(base_score, ours_score) 13 binding = author = alice, audit-status = reviewed 14 leaf e1 : reports(exp_3, effect(M, accuracy, D, positive)) 15 kind = observed 16 provenance = ai-executed 17 refs = [evidence/table_2.csv#row=mean] 18 leaf base : reports(exp_3, score_cell(M0, accuracy, D, base_score)) 19 leaf ours : reports(exp_3, score_cell(M, accuracy, D, ours_score)) 20 leaf e4 : distribution_shift(M, accuracy, D) 21 arg s1 : supports(c2) by lt_recheck from [base, ours] 22 assurance = cert(ord@1, sha256:empv3-t0, (ordcmp (prem base) (prem ours))) 23 leaf e6 : generalizes(M, accuracy, D) 24 arg a1 : supports(c1) by controlled_experiment from [e1] 25 discharge randomization with e2 26 discharge adequate_power with e3 27 discharge external_validity with e6 28 arg d1 : challenges(external_validity(a1)) by leaf(e4) 29 undercut d1 a1.rule 30 status c1 31 status c2 Figure 2: Run 2 of the running example, from the artifact. Run 1 omits lines 23–29. We elide e2 and e3, and base, ours, e4, and e6 keep only their declaration line; their metadata has the form shown for e1. Elaboration infers rule substitutions and resolves named certificate premises to numeric slots. The program declares exactly what the checker judges. Lines 1–3 fix the replay identity: the artifact digest, the versioned claim-support policy, and the backend registry. Each claim then pairs a natural-language sentence with a formal target atom, and the checker does not establish that the signed binding between them is faithful (Section 3.1). The leaves admit evidence with its kind, provenance tag, and source reference, the recorded dead end e4 among them. Admitting e4 does not make it an attack; it counts only once a typed attack cites it (Section 3.5). Of the two arguments, s1 re-checks the ordered comparison of the score cells under a certificate the checker replays, while a1 instantiates the policy’s controlled-experiment scheme (Figure 7). A support argument must conclude the claim’s formal target syntactically, after normalization, and must account for every critical question: e2 and e3 discharge randomization and power, and the off-distribution result e6, absent from run 1, discharges external validity. The last declarations turn the dead end into the typed attack d1, which undercuts a1 at that rule occurrence because it concludes the scheme’s declared exception. ⬇ $ lara check run1/example.lara # without lines 23-29 (verdict (replay-id ...) accept (labels (0 in)) (edges) (statuses (status (atom improves (con M) (con accuracy) (con D)) gap) (status (atom num_lt (num 0.71) (num 0.74)) justified))) $ lara check run2/example.lara # the program as shown (verdict (replay-id ...) accept (labels (0 in) (1 out) (2 in)) (edges (2 1)) (statuses (status (atom improves (con M) (con accuracy) (con D)) defeated) (status (atom num_lt (num 0.71) (num 0.74)) justified))) Figure 3: Checker reports from the artifact’s pinned running example. Replay identities are elided, paths abbreviated, and verdicts wrapped for the page. Acceptance exits 0; rejection returns a nonzero exit code and a located diagnostic. Both programs are accepted (Figure 3). Run 1 omits a1: declaring it with an unanswered mandatory question would cause rejection. Thus supp()supp( c1) is empty and c1 is gap. Run 2 declares the additional evidence and complete support argument, together with the undercut that makes c1 defeated. The undercut challenges the inference’s applicability; it does not prove the empirical claim false. Adding e6 alone would not cause this transition: run 2 also declares a1, d1, and the attack. The attack on a1 leaves s1 and c2 justified in both runs. Strict rule occurrences cannot be rebutted or undercut, although an attack on a premise can still defeat a containing argument. The two claims stand apart here because the program declares no inference carrying the arithmetic into the empirical claim. We give a program whose certified arithmetic does feed a defeasible claim, and outlives its defeat, in Listing J.1. Comparing nearby settings Reusing support from another paper requires identifying the relevant differences (Table 1). New evidence may change a world’s status; a changed premise may instead invalidate the transport contract. The possible-world semantics makes these comparisons explicit through declared bridges (Section 5). Table 1: Motivating comparisons between nearby research settings. These are illustrative scenarios, not evaluated case studies. A small difference does not by itself establish comparability. Shared setting Difference What must be checked Task and classifier New test population Whether the evidence still supports the claim Inference-scheme family New premise or obligation Whether the support-transport contract holds Claim and existing support Additional attacker Whether justification survives the attacker Argument structure Renamed vocabulary Whether support and attacks are preserved 2.3 Trust architecture Following proof-carrying code (Necula, 1997), an untrusted producer supplies the program and its backend certificates. The trusted pipeline (Figure 4) checks them against the signature, versioned policy, and backend registry. Each verdict records these versions, the core version, and the artifact digest for replay, together with its evidence and backend dependencies (Theorem 6.2). Choosing the policy and assessing the evidence remain separate judgments. artifacttraceproducerauthor ∣ script ∣ LLMLara program+ certificatestrusted inputsΣ , Π (versioned), RRparser,policy validatorsupport & attackcheckerbackend registryregistered checkerscompiler, groundedevaluator, status enginereport: status, locateddiagnostics, replay identitytrusted baseuntrusted↺ digest-pinned bundlereplays byte for byte Figure 4: The trust architecture. Only the producer’s output is checked: the signature Σ , versioned policy Π , and registry R reach the trusted base directly (shaded node), never through the producer. The emitted status is one of four core values or evidence-blocked. Scope Acceptance establishes that the declared support and attacks pass the checker; a claim’s status then describes its support in the compiled framework. Both are relative to the admitted evidence, policy, and backend registry. A modal answer ranges over the declared comparisons alone, and says nothing about a setting that no bridge reaches. The checker does not establish the truth of the encoded claims, the accuracy of admitted evidence, the suitability of the policy or backend theory, or the faithfulness of the prose-to-formal binding (Section 3.1, Theorem 6.9). 3 The claim-support language A Lara program is a claim-support certificate: it declares evidence leaves, policy-rule instances, the obligations those instances leave open, and typed attacks. The checker interprets it against four fixed inputs: a logical signature Σ , a versioned claim-support policy Π , a strict-backend registry R, and an artifact snapshot at a recorded digest, whose versions and digest form the replay identity. We give the abstract syntax in Figure 5. The JSON front end decodes directly to it; the presentation surface reaches it through a validated elaborator that expands comparison blocks, labelled rule premises, and cell … interpolation before the core-calculus boundary. Propositions and leavesg⩴k|k(g1,…,gn)ground term over Σp⩴(g1,…,gn)atomic propositionℓ⩴l:pevidence leafκ⩴observed|attested∣assumed∣certifiedleaf kindSupport terms(mode of r is fixed by Π)w⩴levidence leaf∣r⟨θ;w1,…,wn;q↦wq;o;α⟩rule instanceθ⩴X1↦g1,…,Xm↦gmground substitutionα⩴∣(β,h,κβ)assuranceStrict-certificate backend(registered in R,opaque to the source)β:→βproposition encodingβ:ℎβ×[β]×β×β→,certificate checkerClaims and typed attacksc⩴(,p,)claimπ⩴ε∣π.i∣π.qposition in a termk⩴rebutwu∣undercutwu@π∣underminewu@πattack array[]@r@\;c@\;l@ l@ @intercolPropositions and leaves @intercol\\[2.0pt] g& &k\ \ k(g_1,…,g_n)&ground term over $ $\\ p& &pred(g_1,…,g_n)&atomic proposition\\ & & leaf\ l:p&evidence leaf\\ κ& & observed\ \ attested\ \ assumed\ \ certified&leaf kind\\[6.0pt] @intercolSupport terms\;\;(mode of r is fixed by ) @intercol\\[2.0pt] w& & leaf\ l&evidence leaf\\ & &r θ;\,w_1,…,w_n;\,\q w_q\;\,\o\;\,α &rule instance\\ θ& &\X_1 g_1,…,X_m g_m\&ground substitution\\ α& & none\ \ trusted\ \ cert(β,h, _β)&assurance\\[6.0pt] @intercolStrict-certificate backend\;\;(registered in R,\ opaque to the source) @intercol\\[2.0pt] encode_β&:&prop _β&proposition encoding\\ check_β&:&Theory_β×[Form_β]×Form_β×Cert_β→\accept,reject\&certificate checker\\[6.0pt] @intercolClaims and typed attacks @intercol\\[2.0pt] c& & claim\ (nl,\,p,\,binding)&claim\\ π& & \ \ π.i\ \ π.q&position in a term\\ k& & rebut\ w\ u\ \ undercut\ w\ u@π\ \ undermine\ w\ u@π&attack\\ array Figure 5: Abstract syntax of Lara. A single category of support term w carries the assurance annotation α: defeasible instances use none, strict ones are trusted by policy or discharged by an opaque certificate for a backend registered in R at theory digest h. Backend formulas, proof terms, and theories (β encode_β, β check_β, …) are not source constructs and never enter a support term, which keeps a backend’s factivity off the support level. Metavariables: l leaves, r rule identifiers, X rule parameters, q critical questions, o declared holes. 3.1 Propositions, leaves, and claims Support-level propositions are ground first-order atoms over a fixed vocabulary in Σ . Programs may instantiate this vocabulary but may not extend it. The policy declares Σ as a many-sorted signature over two built-in base sorts, and the checker sorts the policy’s patterns and each rule instance’s substitution range; a substitution lemma carries well-sortedness to every atom an accepted program reaches. Conflict at the support level comes from a declared contrary relation rather than from negation to falsum, and an implication is reified as a named rule rather than asserted as a proposition. An evidence leaf declares a proposition together with its kind (observed, attested, assumed, or certified), provenance, and source references. A claim combines a natural-language string, a formal target atom, and an untrusted, human-signed binding between them. A support term supports the claim exactly when its conclusion equals the formal target under the normalized-identity relation ≡. Support is positional identity rather than entailment, so no solver enters the trusted base. An auditor must assess whether the formal atom expresses the prose; normalized identity checks only the formal targets, not their meaning. The presentation surface narrows one source of error: cell e inserts the named leaf’s value into the prose, so the quoted number equals the value stored in the leaf. 3.2 Proposition normalization The identity relation ≡ is the trusted-base equality on propositions, so its definition stays minimal. It operates on the core abstract syntax that both front ends reach (the JSON wire directly, the presentation surface after elaborator expansion), so whitespace, field order, encoding differences, and surface sugar are gone before ≡ applies. A normal form nf(⋅)nf(·) canonicalizes literals and recurses structurally, but it reorders no arguments: the core calculus treats no symbol as associative or commutative. Then p≡qp≡ q iff nf(p)=nf(q)nf(p)=nf(q), which is decidable, total, an equivalence relation, and linear in term size. 3.3 Claim-support policies and obligations A claim-support policy defines named inference schemes. A strict scheme is deductive; a defeasible scheme provides presumptive support and lists critical questions, in the argument-scheme tradition (Walton et al., 2008), that an instance must discharge or leave explicitly open. The policy also declares the contrary relation (the only source of propositional conflict) and exception conditions that license undercuts. Policies are versioned trusted inputs: an artifact program instantiates schemes but never defines or modifies them at runtime. Whether a rule is strict or defeasible is a property of its policy entry, not separate program syntax. Each rule instance carries an explicit ground substitution. The checker therefore performs no unification; it applies the substitution and checks syntactic identity. An instance must account for every declared critical question, either with a discharging subterm or with an explicit hole. Only optional questions may remain open in an accepted program. If an instance leaves a mandatory question open, the checker rejects the program and names both the argument and the question. The ablation in Section 7.3 removes this gate. An instance with an unanswered mandatory question cannot support a claim in an accepted program. The claim is gap only if it has no other complete support argument. Leaf admission precedes evaluation and returns admit, quarantine, or reject from a policy table over (leaf kind, provenance) keys (Section 4 fixes the judgment). A quarantine decision retains the declaration for audit but removes arguments that use it. Quarantine creates no attack, but it can remove one; the conservative public reporting of Section 4 prevents any resulting promotion. The support judgment Σ;Π;Γ;R⊢w:(p)⊳O ; ; ;R w: supports(p) O records unmet mandatory obligations O for a term w supporting proposition p (Figure 6). An argument is complete exactly when O=∅O= ; optional questions can remain open without contributing to O. The defeasible scheme in Figure 7 supplies the shape the running example uses. For a1, the Rule form in Figure 6 derives Σ;Π;Γ;R⊢:((M,,D))⊳∅ ; ; ;R a1: supports(improves(M,accuracy,D)) . The premise leaf e1 has no obligations, and the three discharged questions contribute empty sets. If external validity were instead an explicit hole, the rule would derive _\external\_validity\. Such a term fails the program-level gate. Σ;Π;Γ;R⊢w:(p)⊳O ; ; ;R w: supports(p) O w supports p with open obligations O Γ(l)=pΣ;Π;Γ;R⊢l:(p)⊳∅left=Leafr⟨X1,…,Xm⟩∈Π(P1,…,Pn⇒C)=rdom(θ)=X1,…,Xm|w→|=nΣ;Π;Γ;R⊢wi:(pi)⊳Oipi≡Piθ(1≤i≤n)qj:Aj=cq(r)qj=D⊎HΣ;Π;Γ;R⊢wq:(pq)⊳Oqpq≡Aqθ(q∈D)assurance ok (Section 3.4)O=⋃iOi∪⋃qOq∪(H∩mand(r))Σ;Π;Γ;R⊢r⟨θ;w→;q↦wq;H⟩:(Cθ)⊳Oleft=RuleΣ;Π;Γ;R⊢w:(concl(w))⊳Oconcl(w)≡c.wcleft=Supports array[]c (l)=p ; ; ;R leaf\ l: supports(p) left=Leaf\\[20.0pt] r X_1,…,X_m ∈ 8.19447pt(P_1,…,P_n C)=r 8.19447ptdom(θ)=\X_1,…,X_m\ 16.38895pt| w|=n 8.19447pt ; ; ;R w_i: supports(p_i) O_i 8.19447ptp_i≡ P_iθ 8.19447pt(1≤ i≤ n) 8.19447pt\q_j:A_j\=cq(r) 16.38895pt\q_j\=D H 8.19447pt ; ; ;R w_q: supports(p_q) O_q 8.19447ptp_q≡ A_qθ 8.19447pt(q∈ D) 8.19447ptassurance ok ( sec:strict) 8.19447ptO= _iO_i∪ _qO_q∪ (H (r) ) ; ; ;R r θ; w;\q w_q\;H : supports(Cθ) O left=Rule\\[24.0pt] ; ; ;R w: supports(concl(w)) O 8.19447ptconcl(w)≡ c.formalw supportsc left=Supports array Figure 6: The support judgment. Substitutions and question maps have unique keys, H is a set, and every displayed instantiation must be defined. A strict-mode instance discharges its assurance side condition (trusted by policy or accepted by a registered backend certificate, Section 3.4) and carries an empty question map and hole set; a defeasible instance carries no strict assurance. Only mandatory holes enter O, so an optional hole adds no obligation. Scheme _(M,Y,D) controlled\_experiment(M,Y,D) (mode: defeasible) Premise e:(,(M,Y,D,δ)) leaf\ e:reports(exp,effect(M,Y,D,δ)) Conclusion (M,Y,D)improves(M,Y,D) q1q_1 randomization: were units assigned at random? (mandatory) q2q_2 adequate_power: was the sample adequately powered? (mandatory) q3q_3 external_validity: does the effect hold off distribution D? (mandatory) _:_ℎ(M,Y,D) exception\ controlled\_experiment:distribution\_shift(M,Y,D) Figure 7: A defeasible inference scheme with its critical questions. An instance must discharge every mandatory question with a subterm; one that leaves such a question open as a hole is rejected as incomplete. The exception clause turns the “shown otherwise” failure mode of q3q_3 into an undercut target, so a defeater concluding the exception atom attacks instances of this scheme at rule position (Figure 9). 3.4 Strict-certificate backends A strict rule instance has no critical questions or holes. The policy either marks it explicitly trusted or requires an opaque certificate for a fixed, versioned backend in R. Backend formulas, proof terms, axioms, and model theory remain outside the source calculus. A registry entry supplies only an encoding β encode_β from source propositions to backend formulas and a checker β check_β. Δ⊢e:ϕ e:φ under assumptions Δ , term e checks at backend formula ϕφ ϕ⩴a|⊥|ϕ→ϕe⩴i∣ϕe∣ee|ϕeΔ(i)=ϕΔ⊢i:ϕleft=HypΔ,ϕ1⊢e:ϕ2Δ⊢ϕ1e:ϕ1→ϕ2left=AbsΔ⊢e1:ϕ1→ϕ2Δ⊢e2:ϕ1Δ⊢e1e2:ϕ2left=AppΔ⊢e:⊥Δ⊢ϕe:ϕleft=Abort array[]cφ a\ \ \ \ φ→φ e hyp\ i\ \ lam\ φ\ e\ \ app\ e\ e\ \ abort\ φ\ e\\[16.0pt] (i)=φ hyp\ i:φ left=Hyp , _1 e: _2 lam\ _1\ e: _1→ _2 left=Abs\\[18.0pt] e_1: _1→ _2 8.19447pt e_2: _1 app\ e_1\ e_2: _2 left=App e: abort\ φ\ e:φ left=Abort array Figure 8: The reference strict backend: intuitionistic natural deduction for implication and falsum. The assumption context Δ holds the encoded premise conclusions, which a certificate indexes by de Bruijn position. Induction on the derivation gives soundness and exact dependency accounting. Because source propositions are atomic, the backend certifies only the propositional consequences its encoding and declared theory make visible: no domain law is silently relabelled a tautology. For a strict scheme P1,…,Pn⇒CP_1,…,P_n C at substitution θ, the instance checks only when β check_β accepts β(Cθ) encode_β(Cθ) against the encoded premise conclusions β(Piθ) encode_β(P_iθ) and the declared, digest-addressed theory. The checker handles the premise terms normally and propagates their obligations; only their normalized conclusions cross the interface. That interface runs one way, so no backend formula or proof term can be eliminated into a source truth judgment and the support judgment stays non-factive even when a backend is factive. Nothing else about a backend reaches the calculus, so replacing a backend preserves statuses when the replacement accepts the same strict instances (Theorem 6.11). A registry entry owes the calculus four laws, which the metatheory cites by name. Different strict instances may use different registered backends. Each certificate establishes a consequence in its own backend’s logic (Theorem 6.12). Definition 3.1 (Registry entry). A registry entry for a backend β pairs an encoding β encode_β from source propositions to backend formulas with a certificate checker β check_β satisfying four laws: B1 Deterministic replay. β check_β is a total function of the theory, premises, goal, and certificate: replay is deterministic and terminating. B2 Normalization reflection. p≡qp≡ q iff β(p)=β(q) encode_β(p)= encode_β(q). B3 Certificate soundness. If β(T,Δ,ϕ,κ)= check_β(T, ,φ,κ)=accept, then T;Δ⊧βϕT; _βφ for the backend consequence relation ⊧β _β. B4 Dependency accounting. Every reported slot of an accepted certificate names an in-range premise or theory entry. Replay gives the same verdict on contexts that agree at all reported slots, and the conclusion is a ⊧β _β-consequence of the reported entries alone. These laws permit over-reporting; exact consultation requires a backend-specific result. An unwitnessed strict instance is accepted only when its policy entry says so explicitly; reports distinguish such a trusted-policy step from a certified one. The reference backend is intuitionistic natural deduction for implication and falsum (Figure 8). Its certificates use de Bruijn indices, so the checker follows structural recursion without proof search, and it encodes each proposition as an atom over an injective serialization of nf(p)nf(p), which makes backend formula equality coincide with source ≡. The Logic of Proofs is an optional adapter behind the same interface, its t:Ft:F judgments and realization internal to it. The corpus study records which strict steps carry checked certificates (Appendix C). Σ;Π;Γ;R⊢k:(w,u@π) ; ; ;R k: attacks(w,u@π) Σ;Π;Γ;R⊢w:(pw)⊳Owmode(root(u))=ContraryΠ(pw,concl(u))Σ;Π;Γ;R⊢rebutwu:(w,u@ε)left=RebutΣ;Π;Γ;R⊢w:(pw)⊳Owu@π=r⟨θ;…⟩mode(r)=r:E∈Πpw≡EθΣ;Π;Γ;R⊢undercutwu@π:(w,u@π)left=UndercutΣ;Π;Γ;R⊢w:(pw)⊳Owu@π=lΓ(l)=pContraryΠ(pw,p)Σ;Π;Γ;R⊢underminewu@π:(w,u@π)left=Undermine array[]c ; ; ;R w: supports(p_w) O_w 8.19447ptmode(root(u))= defeasible 8.19447ptContrary_ (p_w,concl(u)) ; ; ;R rebut\ w\ u: attacks(w,u@ ) left=Rebut\\[12.0pt] ; ; ;R w: supports(p_w) O_w 8.19447ptu@π=r θ;… 8.19447ptmode(r)= defeasible 8.19447pt exception\ r:E∈ 8.19447ptp_w≡ Eθ ; ; ;R undercut\ w\ u@π: attacks(w,u@π) left=Undercut\\[12.0pt] ; ; ;R w: supports(p_w) O_w 8.19447ptu@π= leaf\ l 8.19447pt (l)=p 8.19447ptContrary_ (p_w,p) ; ; ;R undermine\ w\ u@π: attacks(w,u@π) left=Undermine array Figure 9: Typed positional attacks. ContraryΠ(p,q)Contrary_ (p,q) holds when some declared AB contrary\ A\ B and ground substitution ρ satisfy p≡Aρp≡ Aρ and q≡Bρq≡ Bρ. Rule lookup, occurrence lookup, and instantiation must succeed. The local judgment permits open OwO_w; whole-program acceptance requires both endpoints to be declared complete arguments (Figure 11). 3.5 Typed positional attacks An attack names a position in a support term, and the three kinds match the three kinds of position. A rebut targets the conclusion of a defeasible instance and requires a declared contrary pair. An undercut targets a defeasible rule occurrence and requires the attacker to conclude the rule’s declared exception. An undermine targets a leaf and requires the attacker to conclude a contrary of the leaf’s proposition. Strict rules expose neither exceptions nor rebuttable conclusions, so they can be neither undercut nor rebutted. We state the attack judgment Σ;Π;Γ;R⊢k:(w,u@π) ; ; ;R k: attacks(w,u@π) in Figure 9; the position π doubles as the source location a diagnostic reports. A recorded dead end therefore defeats nothing until one of the three forms cites it: a dead-end tag, confidence score, or provenance downgrade cannot attack on its own. Whole-program checking ends with a completeness scan: each ordered contrary pair of complete arguments with a leaf or defeasible root as target must be covered by a declared attack, including closure onto containing arguments (Figure 11). The consistency half of Theorem 6.6 rests on this attack-completeness postcondition, and an ablation in Section 7.3 removes the scan. 4 Compilation and claim-support semantics A well-formed Lara program compiles to a finite Dung argumentation framework, and the framework’s grounded labelling, aggregated per claim, is the four-state core status. Source admission The trusted source boundary derives the checking context from the policy’s admission table ΠA _A, which maps (leaf kind, provenance) keys to decisions and defaults to admit (Figure 10). Duplicate policy keys, duplicate leaf identifiers, or a metadata view that departs from the declared leaf table make the source invalid before any leaf decision. A reject decision stops the source at the first rejected leaf in declaration order (R8) and produces no checked unit, while a quarantine decision removes the leaf from the checking context, as do inconsistent duplicate-report groups. Admission runs after structural elaboration has reconstructed every support tree and before the checker, so one combined pruning pass sees the full support graph: it removes every argument that uses a removed leaf and every attack whose raw endpoint no longer resolves, and emits the canonical audit. Identity follows declared argument identifiers rather than support-term equality, so equal terms can still name distinct arguments, and group consistency always reads the original leaf table, so quarantining one member cannot hide a conflict. ΠA⊢⟨M,U⟩↝ _A M,U source admission over ordered leaf metadata M and the declared unit U (k,p)∈ΠAdecideΠA(k,p)=ΠA(k,p)left=Decide(k,p)∉ΠAdecideΠA(k,p)=left=Default array[]c (k,p)∈ _Adecide_ _A(k,p)= _A(k,p) left=Decide (k,p)∉ _Adecide_ _A(k,p)= admit left=Default array Γpolicy=l declared∣decideΠA(kind(l),prov(l))=Qpol=l declared∣decideΠA(kind(l),prov(l))=Qgrp=l∣l is a member of an inconsistent duplicate-report groupQ=Qpol∪QgrpΓchecked=l declared∣l∉Q array[]r@\;=\;l _policy&\\,l declared _ _A(kind(l),prov(l))= admit\,\\\ Q_pol&\\,l declared _ _A(kind(l),prov(l))= quarantine\,\\\ Q_grp&\\,l l is a member of an inconsistent duplicate-report group\,\\\ Q&Q_pol∪ Q_grp\\ _checked&\\,l declared l∉ Q\,\ array The prune removes the leaves in Q, every argument whose support tree uses a removed leaf, and every attack with a removed raw endpoint. audit is its canonical projection: removed leaf rows with their causes (policy first, then one cause per inconsistent containing group, in group declaration order), removed argument ids, and removed raw attacks, all in declaration order. valid(ΠA,M,U)l is the first declared leaf with decideΠA(kind(l),prov(l))=ΠA⊢⟨M,U⟩↝R8(l)left=Rejectvalid(ΠA,M,U)decideΠA(kind(l),prov(l))≠ for every declared leaf lΠA⊢⟨M,U⟩↝⟨Γpolicy,Γchecked,Q,⟩left=Admit array[]c valid( _A,M,U) 8.19447ptl is the first declared leaf with decide_ _A(kind(l),prov(l))= reject _A M,U 8(l) left=Reject\\[20.0pt] valid( _A,M,U) 8.19447ptdecide_ _A(kind(l),prov(l))≠ reject for every declared leaf l _A M,U _policy, _checked,Q,audit left=Admit array Figure 10: Policy admission at the source boundary, over the admission table ΠA _A. Because Admit requires that no declared leaf rejects, Γchecked _checked equals Γpolicy∖Qgrp _policy Q_grp: the policy-admitted leaves minus the members of inconsistent duplicate-report groups. Whole-program acceptance Admission supplies the context for the local support and attack judgments. The checker then accepts exactly the units satisfying Figure 11: every argument is complete, every attack is licensed, and the required conflicts are covered. An accepted program can still contain defeated arguments; the judgment permits status computation and does not predetermine its outcome. Static(Σ,Π,P)NoDup(ruleIds(Π))NoDup(P.)∀w∈P.,∃p.Σ;Π;Γ;R⊢w:(p)⊳∅∀k∈P.,∃w,u,π.Σ;Π;Γ;R⊢k:(w,u@π)∧w,u∈P.AttackComplete(P.,P.)Σ;Π;Γ;R⊢Pleft=Accept Static( , ,P) (ruleIds( )) (P.args) ∀ w∈ P.args,\ ∃ p.\ ; ; ;R w: supports(p) ∀ k∈ P.atts,\ ∃ w,u,π.\ ; ; ;R k: attacks(w,u@π)\ \ w,u∈ P.args (P.args,P.atts) ; ; ;R P\ ok left=Accept Figure 11: Whole-program acceptance after decoding and admission. StaticStatic requires a well-formed signature, well-sorted policy, ground inputs and arguments, in-scope policy variables, and strict-chain well-formedness (Definition 4.4). In the attack premise, w and u@πu@π are the endpoints and occurrence named by k. AttackCompleteAttackComplete requires a declared attack from each source to an occurrence contained in each contrary target whose root is a leaf or a defeasible instance. Pairs are ordered and include self-pairs. Decoding requires unique argument identifiers and declared endpoints; NoDup(P.)NoDup(P.args) also excludes equal support terms. Compilation The arguments of the framework are the complete checked support terms; the attacks are exactly the compiled typed attacks, closed under subarguments in the ASPIC+ manner. An attack on an occurrence compiles to an edge onto every argument that contains that occurrence, so defeating a subterm defeats every complete term built on it. Certificate payloads stay attached to nodes for replay but are not term positions or attack targets. Relabelling them injectively preserves argument names, rule instances, conclusions, obligations, and positions; collapsing distinct payloads to one certified marker can identify subterms and add closure edges (Theorem 6.11). The grounded labelling (Definition 4.2) then maps each argument to in, out, or undec; the definition states the grounded semantics of Dung (1995) in the form the mechanization uses. Definition 4.1 (Compiled framework). For a checked program P, let A(P)A(P) be its set of complete checked terms: the declared terms w with Σ;Π;Γ;R⊢w:(concl(w))⊳∅ ; ; ;R w: supports(concl(w)) . The compiled framework is (P)=(A(P),↝)AF(P)=(A(P), ), where v↝wv w iff P declares a checked attack Σ;Π;Γ;R⊢k:(v,u@π) ; ; ;R k: attacks(v,u@π) and the occurrence u@πu@π is contained in w. Definition 4.2 (Grounded labelling). An argumentation framework F=(,↝)F=(A, ) is a finite set of arguments with an attack relation. A set S⊆S defends a when every attacker of a is attacked by some member of S. The characteristic function maps S to the set of arguments S defends: ℱF(S)=a∈∣S defends aF_F(S)=\\,a S defends a\,\. This function is monotone on the subset lattice. Its least fixpoint (F) G(F), reached from ∅ in at most || iterations, is the grounded extension. The grounded labelling L maps an argument a to in when a∈(F)a∈ G(F), to out when some member of (F) G(F) attacks a, and to undec otherwise. Two monotonicities For a fixed framework, the characteristic function in Definition 4.2 is monotone, so evaluation is deterministic and terminating and cycles produce undec rather than nontermination. Lara is non-monotonic one level up, where the input framework can grow: a new checked argument may attack an argument labelled in and retract a claim’s justified status, even though the original support term remains well typed. Deletion is not a weakening operation either, since removing an attacker may move its target from contested or defeated to justified. The internal transfer operator is thus monotone on a finite-height lattice, while the external map from frameworks to accepted claims is not, as defeasible reasoning requires. Arguments as terms, not proofs That split locates Lara relative to the Curry–Howard correspondence. The judgment Σ;Π;Γ;R⊢w:(p)⊳O ; ; ;R w: supports(p) O is a typing judgment: the checker decides whether a supplied term inhabits its declared support type. It does not search for an inhabitant. Lara realizes the correspondence only at the strict seam, where a certificate is a proof term, its backend checks the proof, and acceptance is a monotone property of that instance (Theorem 6.10). Under Definition 4.3, by contrast, an inhabitant of (p) supports(p) settles nothing: it enters a framework where other terms may attack it, and a later argument can move the claim to defeated while w stays well typed. Typing a support term is arguing, not proving; otherwise the dead end of Section 2 could never overturn its claim. Why grounded semantics We use grounded semantics for the default report. Its extension is unique (the least complete one), so evaluation is deterministic; it is polynomial to compute (Proposition 6.2); and it is skeptical, labelling an argument in only when the argument is defended against every attacker. Preferred and stable semantics can admit multiple extensions, and stable extensions may fail to exist. Deterministic reporting is still possible by quantifying over all extensions, as we do in Section 6.3, but the computational cost changes (Section 6.7). Grounded semantics leaves an unsupported cycle of mutual attacks undec, so claims supported only by those arguments remain contested. Four-state aggregation A claim’s support comprises the complete checked arguments whose conclusions equal its target, and the aggregation follows a fixed priority: gap when the claim has no support, justified when some support argument is labelled in, contested when none is in but some are undec, and defeated when support exists and every support argument is out. Three of these lift the labels of Caminada (2006) from arguments to claims. The fourth, gap, has no labelling analogue because it records absent support before labelling begins, the difference between absence and refutation that a three-state or scored account collapses. Definition 4.3 (Claim status). Let L be the grounded labelling of (P)AF(P) and, for a claim c, let supp(c)=w∈A(P)∣concl(w)≡c.supp(c)=\\,w∈ A(P) (w)≡ c.formal\,\. Then status(c)=gapif supp(c)=∅justifiedif L(w)= for some w∈supp(c)contestedif none is in and L(w)= for some w∈supp(c)defeatedotherwise.status(c)= cases gap&if supp(c)= \\ justified&if L(w)=in for some w (c)\\ contested&if none is in and L(w)=undec for some w (c)\\ defeated&otherwise. cases An incomplete term never enters A(P)A(P): the checker rejects a program that declares one (Section 3.3). Conservative public reporting Quarantine forms F from the declared framework G by removing affected arguments and attacks. Let B be the forward closure in G of removed arguments and retained arguments that lost an incoming edge. A claim with declared complete support in B publishes evidence-blocked; its status in F is only a conditional diagnostic. Other claims publish their core status. The forward closure suffices because the grounded labelling reads only transitive attackers; with nothing blocked, verdict bytes are unchanged. The public report therefore flags claims whose status may depend on removed evidence rather than silently publishing a new justification. The running example, compiled Compiling both runs of the program from Section 2 shows what the aggregation reads (Figure 12). The undischarged question keeps a1 out of A(P)A(P) altogether in run 1, so the dead-end leaf is admitted but has no argument to target; discharging it in run 2 admits a1 and turns the declared undercut into the edge that defeats it. The lower panels show why reusing a checked term in another world need not preserve its status: the target can contain an additional attacker (Section 5). (a) Run 1: missing support(b) Run 2: challenged supportCheck s1 complete; a1 omitted declaring its mandatory hole would reject the program s1, a1, d1 complete declared undercut is well typed Compileand label s1: in s1: in a1: out d1: inundercutAggregatesupp()=∅supp( c1)= c1: gap c2: justifiedsupp()=supp( c1)=\ a1\; a1 is out c1: defeated c2: justified(c) Source world(d) Target worldReusewpw_p: inwpw_p: outwqw_q: insame checked supportidentity transportundermineonly support for p is wpw_p; p: justifiedsame support, additional attacker wqw_q; p: defeated solid arrows: attacks dashed arrow: identity support transport wpw_p, wqw_q: leaf arguments concluding p and its declared contrary q Figure 12: From checked support to claim status. Both running-example programs (a–b) are accepted; the empirical claim changes from missing support to defeated support, while the separate arithmetic claim stays justified. In the mechanized transport witness (c–d), the source declares only wpw_p, the target also wqw_q and its undermine. Transport preserves the complete support term and its empty obligation set, yet the additional attacker changes p’s status. Consistency With an arbitrary contrary relation and no transposition of strict rules, grounded semantics guarantees only closure under declared subarguments. Direct and indirect consistency can fail: two contrary claims may both become justified when their conflict appears only behind unattackable strict inferences. The calculus therefore imposes a compile-time restriction on policies (Definition 4.4): under it every conflict is rebuttable at a defeasible step, so strict closure introduces no new conflict and the two consistency notions coincide by construction. The rationality theorem assumes this restriction (Theorem 6.6). The cost is an expressiveness limit: strict chains may target only uncontested claims. Lifting this restriction would require a different consistency argument. Definition 4.4 (Strict-chain well-formedness). A proposition pattern is strict-reachable in Π it is the conclusion pattern of a declared strict rule; this finite set is closed under strict premises-to-conclusion steps, since every such step ends in a strict conclusion. Π strict-chain well-formed when no strict-reachable pattern may overlap either side of a declared contrary pair, where two patterns may overlap when they could share a canonically equivalent ground instance (a conservative, decidable check). 5 Cross-context comparison semantics Research papers are often comparable without using identical checking contexts. A vocabulary may be renamed, a policy extended, or additional evidence admitted. Comparing their claims requires stating what carries across and what must be checked again. We now formalize the possible-world account introduced in Section 2.1: each accepted program supplies a world with local claim statuses, and declared, applicable bridges determine which worlds a modal query compares. This layer preserves the local calculus. 5.1 Worlds and observations A review scenario Suppose an earlier paper’s encoded claim c is justified. A reviewer transports its supporting argument into a world that also records evidence from a new paper. The argument may still check, but an additional attacker can make the translated claim defeated. This is the shape of the mechanized transport counterexample in Section 6.8. If instead a proposed translation fails to preserve an admitted premise or policy rule, the structural-bridge contract fails before status preservation can be claimed. A difference in settings is therefore neither automatically irrelevant nor automatically a refutation. In the checked-program instance, a world is an accepted program, not a paper identifier. Several papers may contribute to one world; distinct worlds may share a context. Changes in evidence or attacks can distinguish worlds without changing their signature, policy, or registry. Context changes additionally require relating those checking parameters. In either case a bridge specifies the comparison. Definition 5.1 (Outer model). An outer frame carries a set of contexts, each with a type of worlds and queries. A bridge between two contexts carries a candidate relation on worlds, an applicability judgment, and a partial query translation. An edge is accepted when the candidate relation and the applicability judgment both hold, independently of the formula being evaluated. The modal language has status atoms over a world’s queries, negation, conjunction, and one box and diamond per bridge; satisfaction is Kripke-style over accepted edges. The valuation is a parameter assigning propositions to status atoms at worlds. In the checked-program instance, a context fixes a signature, policy, registry, and checker parameters, and its worlds are accepted checked units. We read this instance under either the direct source observation or compiled evaluation. Both valuations assign exactly one status to each query; the generic frame model imposes no such constraint. For a bridge b with claim translation τb _b, the formula ⟨b⟩(τbc) b Justified( _bc) asks whether some accepted successor justifies the translated claim; the corresponding box asks whether every accepted successor does. A robust-justification query also requires a successor to exist, so an empty comparison set cannot establish robustness vacuously. Accessibility ranges over declared, applicable comparisons, not every imaginable setting. The one-world, no-bridge instance recovers local semantics by definitional equality. 5.2 Structural bridges Definition 5.2 (Structural bridge). A structural bridge between two contexts sharing a canonicalizer comprises a partial symbol translation on the predicate and constructor namespaces, a total renaming of evidence leaves, and three clauses: an admitted leaf is admitted at the translated proposition; the target policy carries, at the same rule identifier, exactly the translated rule, with mode, parameters, premise order, question keys, and certifier allowlist preserved verbatim; and certificate acceptance survives translation of the encoded step. Everything else (variables, literals, rule identifiers, question keys, hole sets, assurances) is carried across verbatim, and a lift is undefined exactly at an out-of-vocabulary symbol. A structural bridge specifies how support terms translate. Preserving a claim’s status additionally requires every source argument to have a target transport, every target argument to arise from a source argument, and compiled attacks to correspond in both directions. The executable status checker tests source coverage, target coverage, forward attacks, and backward attacks. The support and status guarantees are stated in Section 6.8. Scope of transport The structural contract supports exact translations: it preserves rule identifiers, question keys, and obligations. A near match that changes a rule’s assumptions does not satisfy that contract merely because its vocabulary translates. Such a comparison requires additional evidence or a different bridge argument. General bridge applicability is a parameter; the executable status checker decides the stated structural correspondence conditions, not relevance to the domain. Undefined claim translations produce an incomparability reason; a defined query with no support produces gap. The layer supplies no approximation theory for limits or numerical error and no presentation syntax for the outer language. Its modal formulas describe support statuses in accepted worlds, preserving the non-factivity of the local calculus. 6 Metatheory A research artifact should let a reader inspect why a claim is supported, compute its standing among declared challenges, and determine what can be reused when evidence or context changes. The metatheory establishes guarantees for these operations. Checking makes support decidable and its dependencies auditable. The central local result, status preservation, connects the artifact’s declared arguments to the evaluator’s reports. Certificate soundness identifies what strict inference establishes, while update and transport results characterize how support and claim status behave under change. These guarantees make the distinction between checked support and claim justification precise. A well-formed argument can be defeated, and a transported argument can encounter new challenges. All results are relative to the declared checking inputs; they do not establish the accuracy of admitted measurements or the adequacy of the chosen policy. We retain the specification’s labels G1–G6 for decidability, accountability, compilation soundness with status preservation, strict-certificate soundness, backend replacement, and consistency. Cross-context results follow the local results in Section 6.8. The semantic results are mechanized in Lean 4. Three arguments remain on paper: the pipeline cost bound (Proposition 6.2), the machine-model bookkeeping for NP-completeness behind Theorem 6.18, and the closure and indirect-consistency clauses of Theorem 6.6. The Haskell implementation is validated by differential tests, which do not prove equivalence on arbitrary inputs (Section 7). Appendix A records the mechanized scope; Appendix I supplies the proofs. Details of realizability, extension-semantics distinctions, linking, and surface correctness appear in the appendix. 6.1 Checking An artifact producer supplies an explicit support term so that a reader can check the proposed inference independently. This requires a terminating acceptance procedure and an unambiguous account of what the term supports. G1 provides the procedure; conclusion uniqueness supplies the latter property and makes checking attacks well-defined. Theorem 6.1 (Decidability (G1)). Program and attack checking terminate. For any Σ , Π , Γ , and candidate term or attack, the checker decides acceptance. Proposition 6.1 (Conclusion uniqueness and support adequacy). A support term determines its conclusion and its obligation set: two derivations for the same w agree on both. Deciding whether w supports a claim therefore reduces to one run of the support checker followed by a normalized identity test on that unique conclusion, and the relation respects ≡. Uniqueness is what lets the attack rules name “the” conclusion of an attacker, so the proof of G1 consumes this proposition rather than merely restating it. Auditing also requires knowing what the accepted support depends on. For example, a reader investigating a disputed measurement must be able to find it among the leaves used by an argument; a strict certificate must account for the premises and theory entries it uses. G2 gives exact leaf accounting and coverage of backend dependencies. Theorem 6.2 (Dependency accountability (G2)). The reported leaf-dependency set of a checked term w equals leaves(w)leaves(w), every member is declared in Γ , and the reported backend dependencies certDeps(w)certDeps(w) contain every free premise and theory entry each accepted certificate uses. 6.2 Compilation and claim statuses The artifact’s claim report must reflect the support and challenges expressed in its source. A compilation error could instead introduce a spurious attacker or direct an attack at an unrelated argument. Compilation soundness rules out malformed compiled structure and misdirected closure edges. Determinism then ensures that fixed checking inputs yield a reproducible report. Status preservation establishes the central semantic guarantee: that report agrees with a direct reading of the source. Theorem 6.3 (Compilation soundness (G3)). No untyped node or attack enters the compiled framework; subargument closure adds edges only to arguments containing the attacked occurrence. Theorem 6.4 (Determinism and termination of evaluation). Grounded evaluation and claim aggregation are deterministic and terminating on the finite compiled framework. Termination and determinism alone do not connect the report to the source’s meaning. To state that connection, we define claim statuses directly from checked source attacks, without building the framework. The mutually inductive predicates below provide this independent side of the status-preservation theorem. Definition 6.1 (Direct claim status). For a checked program P, let directly in and directly out be the least predicates on A(P)A(P) satisfying two conditions. A term w is directly in when every term v that attacks an occurrence in w through a checked attack declared in P is directly out. A term v is directly out when some directly-in term attacks an occurrence in v. The direct status of a claim c is gap when supp(c)=∅supp(c)= , and justified when some member of supp(c)supp(c) is directly in. It is contested when no member is directly in and some member is not directly out. It is defeated when no member is directly in and every member is directly out. Theorem 6.5 (Status preservation (G3)). The direct source semantics and the compiled-framework semantics agree: for every claim, the direct status of Definition 6.1 is exactly the status of Definition 4.3, in both directions. Status preservation lets a reader interpret the computed report in terms of the source arguments, without inspecting the compiled graph. It does not by itself ensure that the source semantics treats strict inference and conflict coherently. G6 establishes that additional property. Its strict-chain hypothesis matters because otherwise a conflict can occur behind strict inferences that cannot be rebutted (Definition 4.4). Theorem 6.6 (Rationality postulates (G6)). Closure under declared subarguments holds without the strict-chain hypothesis, and so does closure under declared strict steps: a declared strict instance whose immediate premise arguments are declared and accepted is itself accepted. Under strict-chain well-formedness (Definition 4.4), direct consistency holds, so two contrary claims are never jointly justified, and closing the accepted conclusions under strict rules introduces no new conflict, so indirect consistency coincides with direct consistency. Direct consistency is mechanized for the reference checker over the complete claims of an accepted unit; the closure and indirect-consistency clauses are short paper arguments over the mechanized edge relation (Appendix I). Evidence admission creates a separate risk. Quarantining a questionable measurement can remove an argument that attacks another claim; ordinary grounded evaluation may then accept that claim. A public report should not gain justification merely because relevant material was excluded from checking. The conservative reporting rule prevents this promotion. Theorem 6.7 (Quarantine non-promotion). If the production checker publishes justified for a claim after quarantine, then that claim is justified in the declared framework with the quarantined material reinstated. The implication is one-way: status equality would require equal complete-support sets, which quarantine need not preserve (Appendix I). Realizable frameworks A framework is realizable when some accepted program compiles to it, up to an isomorphism preserving conclusions and attacks. Every realizable framework satisfies range and conflict-completeness invariants, but these conditions are insufficient for an arbitrary fixed policy. Appendix F gives the definitions and counterexample; the cost results below concern this realizable class. 6.3 Semantics-parametric observation Grounded evaluation is one choice among Dung’s semantics, so a fair question is which status guarantees depend on that choice. This subsection makes the semantics a parameter. Compilation never inspects it: the compiled framework stays fixed, and only the status observation varies. Definition 6.2 (Extension semantics). An extension semantics pairs a specification, a relation between a finite framework and a candidate extension, with an enumeration, such that on any duplicate-free carrier the enumeration lists exactly the carrier subsets satisfying the specification. We instantiate five: grounded, specified first-order as the least complete extension, and complete, preferred, stable, and semi-stable in their standard forms (Dung, 1995). Definition 6.3 (Claim observation). Fix an extension semantics and a framework F. The observation of a claim c is gap when supp(c)=∅supp(c)= ; the report no-extension when the enumeration of F is empty; justified when every extension contains a member of supp(c)supp(c); defeated when every extension attacks every member of supp(c)supp(c); and contested otherwise. The guards are evaluated in the stated order. Testing support first makes gap independent of the semantics and prevents empty support from satisfying the defeat condition vacuously. Testing extension existence next prevents both universal conditions from succeeding when no extension exists. For justified, the supporting argument may differ between extensions: every extension must contain some support, but no single argument need belong to them all. This separates two questions an artifact reader may ask: whether the artifact supplies any complete support, and whether that support survives a chosen treatment of conflict. The next theorem connects this general interface to the grounded report used throughout the paper. Theorem 6.8 (The printed status is the grounded instance). On a duplicate-free carrier, the grounded enumeration has one element, and the observation under grounded semantics is the status of Definition 4.3. Skeptical and credulous argument acceptance collapse under grounded semantics. The remaining results separate what depends on the extension semantics. Only gap is semantics-independent. Stable semantics may have no extension, which produces the explicit no-extension report; a source observation transport theorem generalizes agreement under attack-extensionality and bounded claim support. The statements, separation examples, and necessary hypotheses appear in Appendix H. 6.4 Strict-certificate backends A research argument may combine a checked numerical comparison with a logical derivation. The artifact must record what each proof tool establishes without treating either as a proof of the source claim’s truth. Isolation enforces this source boundary; G4 supplies the positive guarantee that an accepted certificate establishes the encoded consequence in its backend’s logic. Theorem 6.9 (Strict-certificate isolation and non-factivity). No support term, attack, or backend proof term crosses the strict-certificate interface, and no backend formula or proof term is eliminated into a source truth judgment. Programs cannot extend R. Theorem 6.10 (Strict-certificate soundness (G4)). For a certified strict instance of P1,…,Pn⇒CP_1,…,P_n C at θ, the encoded conclusion is a backend consequence of the encoded premise conclusions and declared theory: T;[β(Piθ)]⊧β(Cθ)T;[ encode_β(P_iθ)] _β encode_β(Cθ). The result excludes trusted-policy instances. Each registered backend discharges the obligation in its own way: nd@1 by induction on the natural-deduction derivation, ra@1 by witness cancellation over exact integer cross-multiplication, ord@1 by the decided order on the two canonical numerals, and insp@1 by checking membership, absence, or uniqueness in declared exhaustive inventories (Appendix I). For the comparison in the introduction, G4 validates the inference between encoded accuracy values under its declared premises. Whether those values describe comparable experiments remains a source-level support question. G5 addresses a different concern: changing the proof tool should preserve claim reports when it accepts exactly the same strict instances. Theorem 6.11 (Backend replacement (G5)). Source-identical programs related by an injective relabelling of certificate payloads, whose backends accept the same strict instances, compile to the same argumentation framework and assign every claim the same status. Replacement compares whole programs one backend at a time. Within one artifact, different inference steps may need different proof tools. Heterogeneous compositionality establishes that these steps can form one checked support term while each retains its own consequence guarantee and dependency account. Call a node of a support term a certified occurrence when it instantiates a strict rule under a certificate assurance. The occurrence records its rule, substitution, backend identity, theory digest, and certificate reference; its premises and conclusion are derived from the rule and substitution rather than stored, so an occurrence cannot disagree with its own typing. Theorem 6.12 (Heterogeneous backend compositionality). Let w be a checked support term. Every certified occurrence in w names a strict policy rule that allows its backend identity and theory digest, its instantiated premises and conclusion resolve, its own registered checker accepts its certificate against them, and the occurrence-local consequence holds: the encoded conclusion follows, in that backend’s own logic, from the selected encoded premises and resolved theory. The backend, its formula type, its theory, and its consequence relation are quantified independently at each occurrence. Moreover, certDeps(w)certDeps(w) is exactly the union of the occurrence-local reports, each computed by its occurrence’s own backend. A parent checks a child’s conclusion and obligations without inspecting its backend. Replacing a premise or discharge subterm by another with the same conclusion and obligation set therefore preserves typing. The theorem composes source support judgments; it requires no translation or common model theory between backends. Linking and certificate representation The replacement theorem also holds inside admissible linking contexts, including contexts that fill critical-question holes. The extension quantifies over all extension semantics and over partial-bijective relations between certificates. We give the fragment calculus, the precise admissibility conditions, and these results in Appendix E. 6.5 The source boundary Admission determines the checking context before core checking. Its eight properties are stated in Appendix A. Endpoint-safe pruning preserves declared argument identities and removes attacks whose endpoints disappear (Property 3). Tightening admission can only remove structure (Property 6), but removing an attacker can change a retained argument’s label. Source non-promotion applies the conservative reporting rule at this boundary: a published justified claim was already justified with the quarantined material reinstated (Property 8). 6.6 Source updates and status dynamics Research artifacts change as authors add evidence, supply an argument, or record a challenge. These edits have different meanings: a new measurement alone supplies no inference connecting it to a claim, while a new attack can defeat existing support. We therefore ask which status transitions each accepted source edit can cause. A closed, one-step update calculus makes this question precise. Every reachable transition carries an accepted witness program, every unreachable transition a theorem, and the public reporting layer recovers non-promotion as a corollary of the resulting matrix (Corollary 6.16). Definition 6.4 (Source states and updates). A source state carries exactly the raw inputs from which admission and whole-unit checking derive: signature, policy, admission table, leaves and metadata, raw arguments, raw attacks, duplicate groups, and ground input. It is accepted when admission accepts the raw carriers and the checker accepts the pruned unit that admission produces. A source update is one of four constructors, each with a decidable side condition: add-leaf (a fresh leaf and metadata row), tighten (move an admitted admission key to quarantine), add-attack (a raw attack between declared arguments), and add-instance (a fresh raw argument). Applying an update checks the side condition, edits only the corresponding raw carrier, and reruns admission and the whole-unit checker; it returns the edited state only when both accept, and otherwise one of a closed set of rejections. An edit must first leave an artifact that can still be checked. The following sufficient conditions expose the obligations on an editing tool, including freshness, endpoint retention, and attack completeness. Preserving acceptance permits the claim statuses themselves to change. Theorem 6.13 (Acceptance preservation). Each constructor maps an accepted source to an accepted target under explicit sufficient conditions: freshness and an admitted metadata key for add-leaf; a tightened table at least as restrictive, valid, and rejection-free, with retained-leaf agreement and surviving coverage witnesses, for tighten; resolution, typing, and endpoint retention for add-attack; and freshness, well-sortedness, complete support, and extended attack completeness for add-instance. No constructor succeeds unconditionally. Theorem 6.14 (Grounded transition matrices). For grounded observations, of the 64 cells of update kind by source status by target status, exactly 37 are reachable: 4 for add-leaf, 13 for tighten, 10 for add-attack, and 10 for add-instance (Table 15). Each reachable cell carries an accepted source and target program with a successful update between them, and a theorem excludes each unreachable cell under its constructor’s stated premises. In particular, add-leaf fixes every core status, and a fresh instance enters the old framework as an unattacked sink, so add-instance never maps justified or contested to defeated. These are individual edit operations. add-instance adds no attack declaration; adding an argument with attacks requires multiple operations and falls outside its one-step matrix. The matrices distinguish possible effects from guaranteed invariants; they do not predict a particular edit’s outcome without evaluating its arguments and attacks. One distinction survives every choice of extension semantics: supplying a leaf or a challenge cannot fill a missing support argument. The next result makes this boundary explicit. Theorem 6.15 (The gap boundary, semantics-parametrically). For every extension semantics: a successful add-attack preserves a source gap; no successful additive update (add-leaf, add-attack, or add-instance) moves a non-gap observation to gap; and every non-instance update (add-leaf, tighten, or add-attack) preserves a source gap. add-instance is the one constructor that can leave gap. The public layer Public reports take five values: the four statuses plus evidence-blocked. Call an accepted run clean when its prune removes nothing. On a clean source the public report equals the grounded core report, a successful additive update preserves cleanliness, and additive public transitions are therefore exactly the core transitions, never reaching evidence-blocked. Cleanliness cannot be dropped: on a real accepted, non-clean source, one added attack grows the blocked closure and moves a public justified to evidence-blocked while the conditional core status reads defeated. tighten may prune, so its public matrix is separate: of its 20 cells, 13 are reachable, three of them into evidence-blocked, and a public justified target is reachable only from a justified source. Corollary 6.16 (Matrix non-promotion). From a clean accepted source, if a successful tighten publishes justified for a claim, then that claim is justified in the source’s declared framework, the framework with the quarantined material reinstated. The proof reads the tighten column of the public matrix and the clean-source identities rather than Property 8, so the reporting-layer guarantee is recovered from the dynamics, not assumed. Against belief revision A belief-set projection exists, the set of claims observed justified, so AGM-style postulates are statable. The two we probed both fail by mechanized counterexample: success, because a fresh instance’s sole support can be defeated on arrival, and inclusion, because one added attack can remove a previously justified claim. Update in Lara is argumentation dynamics, not belief revision, and we claim no AGM compliance. Surface correctness An independent judgment for the parsed presentation syntax connects authoring to the core: elaboration preserves checking and reflects it on the supported fragment. Direct surface observations agree with compiled observations for attack-extensional extension semantics. Appendix G states the results and their parser boundary. 6.7 Cost A checkable artifact also needs a computational account of its reports. The realizability definition in Appendix F fixes the class of frameworks Lara programs can denote; this subsection bounds status queries on that class. Realizability matters here: a difficult arbitrary framework would say little about artifact evaluation if no accepted program could express it. The cost model counts attack-relation queries in an instrumented mirror of the grounded evaluator whose value provably equals the reference evaluator’s, in the short-circuit order the Boolean connectives actually evaluate. The bounds measure this evaluator, not a lower bound for every algorithm implementing grounded semantics. The two bounds of Theorem 6.17 apply to every input framework; the tightness witness and the reduction of Theorem 6.18 are statements about the realizable class, and each carries its own realization in one fixed context. Theorem 6.17 (Grounded query bounds). On every finite framework with n arguments, grounded evaluation issues at most n3(1+n)n^3(1+n) and at least n2n^2 attack queries, and a four-state status query issues at most n3(1+n)+2n2n^3(1+n)+2n^2. The upper bounds are tight up to degree on the realizable class: a family of accepted programs, realizable in one fixed signature, policy, and registry, has size 3k3k and costs at least k4k^4 queries for every k≥2k≥ 2. The quantifiers differ by design: the quadratic lower bound is universal, while the quartic cost is a worst case on a realizable family; no instance-wise cubic floor holds, the two-node all-attacks framework costing exactly four queries. The preceding bound describes the reference grounded evaluator. Choosing a richer acceptance query raises a separate question: do the language’s structural restrictions eliminate the difficulty of that query? The next reduction shows that credulous complete acceptance remains hard even when every constructed framework comes from an accepted artifact in one fixed checking context. Theorem 6.18 (Hardness on the realizable class). Fix one explicit signature, policy, and registry. A computable reduction maps each 3SAT formula φ to a structured framework that is realizable in that fixed context, with 2v+m+12v+m+1 nodes for v variables and m clauses and encoded size at most 64(|φ|+1)264\,( +1)^2, such that φ is satisfiable exactly when the framework’s query claim is credulously accepted under complete semantics. The statement is genuinely restricted: the one-node self-attacking framework is not realizable in the same context. Credulous complete acceptance on Lara-realizable frameworks is therefore NP-complete: hardness by the reduction, membership by guessing an extension and checking it in polynomial time. The reduction, its realization, and its size bounds are mechanized; the NP bookkeeping over encodings and the machine model stays on paper, with the counting argument below. Proposition 6.2 (Polynomial core checking and evaluation). Let N be the size of the explicit core checking input, including the signature, policy, evidence tables, substitutions, and support trees. Assume linear-time literal normalization and count backend encoding and replay as opaque calls. Support and attack checking, whole-program acceptance, compilation, and grounded claim-status computation perform polynomially many syntactic operations and backend calls in N. This bound excludes surface elaboration and the work inside backends; it does not assert linear time for the list-based checker. 6.8 Cross-context guarantees The outer model and structural bridges of Section 5 build on the local calculus. Direct source observations and compiled evaluation agree at every modal formula: Theorem 6.5 gives agreement at each world, and satisfaction is extensional in the valuation. The practical question is what an artifact reader may carry from one context into another. We separate an executable observation of declared worlds, reuse of a checked support term, and preservation of the claim’s status. Each requires its own guarantee. A bridge records an allowed comparison; its existence does not make the comparison reversible or ensure that successive comparisons compose into an available direct one. The modal laws respect this freedom. Comparison adequacy additionally ensures that the executable report answers the stated modal query and distinguishes failure to compare from a claim status. Theorem 6.19 (Modal normality and comparison adequacy). The K axiom, necessitation, and box–diamond duality hold in every generic outer model and hence in the checked-program instance. Each of T, D, B, 4, and 5 has a countermodel with unrestricted valuations; these establish neither checked-program counterexamples nor a complete axiomatization. An executable comparison decides the diamond: given a finite presentation of a bridge’s candidates and acceptance, its output contains a status exactly when the model satisfies the corresponding diamond formula, and an incomparable query is reported by reason, an undefined translation, no candidate, or all candidates rejected, never as a status. Reusing an argument requires more than an accessible world. Its translated steps must check, its obligations must survive, and its certificates must replay in the target registry. Exact support transport supplies this contract, including agreement between composite and stepwise translation. Theorem 6.20 (Exact support transport). Along a structural bridge, a checked support term whose translation is defined checks in the target context with the translated conclusion and the verbatim obligation set; completeness transports, claim-level support survives normalized identity, and every certified occurrence of the transported term replays against the target registry, in the sense of Theorem 6.12. Transport along a composite of bridges equals stepwise transport along the path, and a chosen direct bridge agrees with a chosen path exactly when their symbol and leaf maps are equal, a commuting condition that is characterized, not assumed. Transport is not status preservation. A mechanized witness transports a source argument whose claim is justified onto a target world where the same translated claim is defeated: the target may hold attackers the source lacks. Preservation needs the target’s arguments and attacks matched, and that is the next theorem. Theorem 6.21 (Conditional status preservation). Let a structural bridge with an injective translation relate two worlds such that (i) every source argument transports into the target program; (i) every target argument is a transport of some source argument; and (i) compiled attack edges correspond in both directions along the transport. Then for every translatable query, the target status of the translated claim equals the source status, in all four states. The support correspondence follows from the bridge contract; the argument and attack clauses supply a total attack bisimulation. The executable checker decides four clauses soundly and completely: source coverage, target coverage, forward attacks, and backward attacks. These hypotheses compose along bridge paths. With at least one accepted successor and every accepted successor so related, each local status atom agrees with its boxed and diamonded translation. These conditions identify when a reader can reuse a claim’s status as well as its support. The checker makes the conditions testable, while their composition permits reuse along a path of contexts. If they fail, support transport may still apply, but the target status must be established from the target’s arguments and attacks. 7 Mechanization and implementation We mechanize the semantic guarantees in Lean 4 and validate a Haskell implementation against the executable Lean semantics. A worked example shows how the implementation separates certified arithmetic from defeasible empirical support. 7.1 Mechanization At implementation revision b62d33e0, the Lean tree contains 144 files and roughly 117 000117\,000 lines. The audited public metatheory is sorry-free and uses only Lean’s standard trio (propext, Classical.choice, Quot.sound). Some private executable examples additionally trust native evaluation through native_decide; Appendix A details the audit boundary and workflow. We mechanize thirty-four of the thirty-five specification results in full, including backend dependency accounting for all four registered backends. Future backends must discharge the same interface laws (Section 6). The cross-context proofs and examples establish the behavior of declared bridges (Section 6.8); they do not evaluate bridge discovery or automated literature-based review. 7.2 Implementation conformance The Haskell implementation covers the checking pipeline and four strict backends. A differential harness uses the compiled Lean semantics as its reference interpreter and requires byte-identical reports and exit codes from both drivers. At b62d33e0, the core differential agrees on 673/673 verdict-bearing inputs, including accepted programs and semantic rejections, and 66/66 malformed inputs. These finite suites check implementation conformance; they do not prove equivalence of the two implementations. The surface elaboration theorems start at a parsed AST (Appendix G); tests validate the Haskell parser and elaborator. The trusted base, further conformance checks, and timings appear in Appendix B. An exploratory study of machine-annotated research artifacts appears in Appendix C. Its results describe the supplied encodings under a chosen policy; the semantic guarantees hold regardless. 7.3 Ablation study: effects of removing checks At revision 7d0f7384, we reran 655 inputs with selected acceptance checks disabled (Figure 11, Table 2). Removing obligation checking admits 18 incomplete-support programs; removing coverage admits five missing-attack programs; disabling attack typing as well admits 32 further invalid-target or unlicensed-attack cases. These seeded defects demonstrate detection of the intended failures, not their prevalence in research artifacts. The ablation, conformance, and timing revisions are recorded separately in Appendix B. Table 2: Removing checks admits malformed programs. Each configuration runs on 655 manifest inputs. Counts are newly admitted programs that the full checker rejects; all other outcomes are unchanged. Check removed Newly admitted defect Programs Obligation discharge Incomplete support 18 Conflict coverage Missing required attack 5 Attack typing and coverage Invalid target or unlicensed attack 32 Missing required attack 5 7.4 Arithmetic and empirical support The worked-example suite covers all four statuses and three attack kinds, with expected reports replayed by the differential harness. One example draws the boundary between arithmetic and empirical meaning. ord@1 certifies only a ground inequality between canonical decimal numerals, while a defeasible, attackable bridge rule states that those numerals measure the systems the claim names. One comparison block specifies the systems, measurand, dataset, relation, and evidence leaves, and a validated elaborator emits all three pieces: the strict arithmetic check, the defeasible bridge, and the arithmetic subclaim. Sibling programs show why the split matters. In a tie, arithmetic blocks the stronger claim without reviewer judgment: equal cells admit only the non-strict comparison certificate, replay rejects the strict version, and the bridge can conclude at least as good but never beats. Under attack, a settings audit undermines the bridge’s binding premise, the attestation that the two cells are comparable, so the bridge and the headline claim become defeated while the certified inequality remains justified (Listing J.1). The certificate established the arithmetic and nothing more, which makes the non-factivity of Theorem 6.9 visible in the verdict. 7.5 Demonstrations beyond empirical claims Two later demonstrations exercise the same calculus with assumed and attested premises (Section D.4 and Section D.5). A philosophical debate checks contestation and reinstatement without measurements or a strict backend. An axiom-withdrawal example checks source admission and certified hypothesis reuse, with a separate executable Lean witness for the structural transport boundary. We cite their sources at revision 0f2a6dce; these examples supplement the earlier conformance counts reported above and introduce no new kernel rule. 7.6 Limitations The prose-to-formal binding is untrusted by design, so a valid certificate can sit on an unfaithful formalization (Section 3.1). Strict-chain well-formedness excludes conflicts involving strict-rule conclusions (Section 4). The only producer exercised end to end so far is the deterministic lowering: how well other untrusted producers fare against the checker is untested, though no soundness result depends on the answer. Lowering itself also has a limit. ARA is an artifact format rather than a programming language, so an arbitrary artifact has no canonical compile step: the ARA Compiler already uses a language model to reconstruct an artifact from a finished paper (Liu et al., 2026), and lowering such an artifact to Lara inherits the same untrusted, model-mediated step. The architecture absorbs this by design, since the checker alone decides acceptance, but a rejected program then locates a fault in the proposed lowering, not necessarily in the research. The clean path runs through auto-research itself: an agent that already records claims, evidence, and attacks can emit Lara programs alongside them as one more intermediate artifact, so support becomes checkable at authoring time instead of reconstructed after the fact. We design the surface syntax only far enough to exercise the calculus end to end and left their design as an authoring language unexamined, because the contribution is the core calculus and semantics behind the elaborator boundary, which any surface can reach. Future work treats that surface as a target for language models: which syntax an agent emits most reliably and efficiently, and how emitting Lara programs fits into a model-driven research workflow. 8 Related work Abstract and structured argumentation Lara builds on the abstract frameworks of Dung (1995) and the argument labellings of Caminada (2006). The Handbook of Formal Argumentation surveys the wider family of formalisms (Baroni et al., 2018). Lara’s contribution is a checked language that generates such frameworks, with a proof that compilation preserves a direct source semantics (Theorem 6.5). Its additional gap status records claims with no complete support argument, before argument labelling begins. ASPIC+ gives arguments rule structure and distinguishes rebut, undercut, and undermine (Modgil and Prakken, 2014). Work on its rationality postulates studies closure and consistency (Caminada and Amgoud, 2007; Cramer and Friese, 2026). Lara builds on this structure and adds evidence admission, replayable strict certificates, and mandatory critical-question discharge (Section 3.3), following the argument-scheme account of critical questions (Yu and Zenker, 2020). Its consistency result requires both attack completeness and the explicit strict-chain restriction (Theorem 6.6). Thus the contribution is a checked instantiation and compilation discipline, rather than a new abstract defeat semantics. Semantic publishing Micropublications represent claims, evidence, and support relations in biomedical communication (Clark et al., 2014). The Argument Interchange Format provides a vocabulary for inference, conflict, and preference (Chesñevar et al., 2006). These representation models provide objects on which reasoning tools can operate. Lara specifies a certificate language, a decidable acceptance judgment, and a compilation whose claim statuses agree with the source judgment. Structured research artifacts (Liu et al., 2026) are one source of its declarations; their prose-to-formal bindings still require assessment. Explicit-evidence logics The Logic of Proofs makes proofs explicit within formulas (Artemov, 2001). Its factive reading permits elimination from a proof assertion to the asserted proposition. Dynamic logics of evidence-based belief study changes in evidence and belief (van Benthem and Pacuit, 2011; van Benthem et al., 2014). Pandžić (2022a); Pandžić (2022b) are particularly close in structure: they represent defeasible arguments as justification-logic terms with rebut, undercut, and undermine. Lara adopts this term structure and adds a certificate-checking discipline with versioned policies, critical-question obligations, provenance-based admission, and compilation to an argumentation framework. The Logic of Proofs can serve as an optional strict backend; its factive reasoning stays behind the interface (Theorem 6.9). Its realization theorem does not establish faithful formalization of a natural-language claim. Possible-world semantics and bisimulation Lara instantiates possible-world semantics (Kripke, 1963; Blackburn et al., 2001) with accepted programs as worlds, declared applicable bridges as accessibility, and claim statuses as the valuation (Definition 5.1). Its modal queries therefore describe support across declared checking contexts; they do not establish the truth of a research claim. Grossi (2010) connects the two fields from the other direction, reading a single framework as a Kripke frame whose worlds are arguments and whose accessibility relation is attack. Lara places the modality one level up, where a world is an accepted program and a bridge relates two checking contexts; the two readings are compatible and answer different questions. Lara uses total attack bisimulation to establish status preservation across a bridge between compiled frameworks (Theorem 6.21). Oikarinen and Woltran (2011) characterize strong equivalence through kernels, asking when two frameworks may replace each other under any addition. Lara asks a narrower question, whether a declared translation between two given programs preserves a claim’s grounded status, and its checker decides the four clauses soundly and completely. Neither result decides whether the compared settings are meaningfully comparable in the domain being studied. Proof-carrying architectures Proof-carrying code separates an untrusted producer from a trusted checker (Necula, 1997). Foundational proof certificates support multiple proof formats through a small checking interface (Miller, 2015). Lara applies this discipline to defeasible support. An accepted support term can later lose its claim’s justification, and evidence quarantine cannot create a public justification (Theorem 6.7). Different strict instances may use different registered backends without a shared backend logic (Theorem 6.12). Acceptance-preserving replacements leave claim statuses unchanged; the appendix extends this result to admissible linking contexts and partial-bijective certificate relations (Appendix E). These results do not establish full abstraction. Verified and agentic claim checking EG-VAR verifies tool-attested empirical claims through Lean 4 kernel proofs (Ren, 2026). Lara addresses a different part of the support relation: explicit attacks can defeat an otherwise checked argument, and mandatory critical questions can prevent an argument from entering the framework. Pramana attests claims at the protocol layer for agent networks (Kadaboina, 2026), whereas Lara computes claim statuses from support and attack declarations. LLM judges produce assessments and rationales (Alvarez et al., 2024); such output can propose a Lara certificate, but acceptance depends on replaying the checker. Work on faithful natural-language-to-Lean formalization (Zhang et al., 2026) addresses whether formal statements capture their prose. Lara leaves that question outside its semantic guarantee. 9 Conclusion We have presented Lara, a kernel language built on the thesis that support for research claims should be checked locally and transported across contexts only under explicit bridge conditions. Locally, a decidable checker compiles declared evidence, scheme instances, critical-question answers, and typed attacks into a grounded status for every claim, and compilation preserves the statuses of a direct source semantics. Across contexts, structural bridges transport checked support with its obligations, while preserving a claim’s status requires stronger correspondence conditions that an executable checker decides soundly and completely; a translated argument can therefore remain well formed while additional evidence defeats its claim. The case studies show that this support need not come from measurements. The same calculus represents objections and defenses in a philosophical debate, and an axiom-withdrawal witness makes the assumptions required for proof reuse explicit. Lara thus checks how support depends on premises and survives challenges across empirical and non-empirical arguments. The calculus does not automate domain judgment: choosing a bridge and defending its meaning remain the researcher’s task, and the checker makes the consequences of that choice inspectable. Three directions follow: lowering research artifacts to Lara programs beyond the deterministic path exercised here, growing versioned policies into community standards of review, and deciding the structural conditions of candidate bridges mined across a literature. On this substrate, we envision autonomous research becoming more robust: an agent that builds on a gap or defeated claim inherits a status the checker reports, not an error that propagates silently. As machines write and judge a growing share of science, whether evidence supports a claim in a given context can then become what well-typedness became for software: a question a checker answers. References Alvarez et al. (2024) C. Alvarez, M. Bennett, and L. Wang Zero-shot Scientific Claim Verification Using LLMs and Citation Text. In Proceedings of the Fourth Workshop on Scholarly Document Processing (SDP 2024), p. 269–276. External Links: Document, Link Cited by: §8. ARA-Labs (2026a) ARA-Labs A Philosophy-of-Mathematics Debate: Lara Demonstration. Note: Authored example, policy, golden verdict, and reproduction instructions; introduced in pull request 351 External Links: Link Cited by: Listing J.5, §D.4. ARA-Labs (2026b) ARA-Labs Withdrawing an Assumed Axiom: Lara Demonstration. Note: Source-admission examples and separate executable Lean structural-contract witness; introduced in pull request 352 External Links: Link Cited by: Listing J.6, §D.5. Artemov (2001) S. N. Artemov Explicit Provability and Constructive Semantics. Bulletin of Symbolic Logic 7 (1), p. 1–36. External Links: Document, Link Cited by: §8. Aygün et al. (2026) E. Aygün, A. Belyaeva, G. Comanici, M. Coram, H. Cui, J. Garrison, R. Johnston, A. Kast, C. Y. McLean, P. Norgaard, Z. Shamsi, D. Smalling, J. Thompson, S. Venugopalan, B. P. Williams, C. He, S. Martinson, M. Plomecka, L. Wei, Y. Zhou, Q. Zhu, M. Abraham, E. Brand, A. Bulanova, J. A. Cardille, C. Co, S. Ellsworth, G. Joseph, M. Kane, R. Krueger, J. Kartiwa, D. Liebling, J. Lueckmann, P. Raccuglia, X. J. Wang, K. Chou, J. Manyika, Y. Matias, J. C. Platt, L. Dorfman, S. Mourad, and M. P. Brenner An AI system to help scientists write expert-level empirical software. Nature 654 (8120), p. 909–916. External Links: Document, Link Cited by: §1. P. Baroni, D. Gabbay, M. Giacomin, and L. van der Torre (Eds.) (2018) P. Baroni, D. Gabbay, M. Giacomin, and L. van der Torre (Eds.) Handbook of Formal Argumentation. College Publications, London, England. External Links: ISBN 9781848902756, Link Cited by: §8. Bianchi et al. (2026) F. Bianchi, O. Queen, N. Thakkar, E. Sun, and J. Zou Exploring the use of AI authors and reviewers at Agents4Science. Nature Biotechnology 44 (1), p. 11–14. External Links: Document, Link Cited by: §1. Biswas et al. (2026) J. Biswas, S. Schoepp, G. Vasan, A. Opipari, A. Zhang, Z. Hu, S. Joseph, M. Lease, J. J. Li, P. Stone, K. L. Wagstaff, M. E. Taylor, and O. C. Jenkins AI-Assisted Peer Review at Scale: The AAAI-26 AI Review Pilot. External Links: 2604.13940, Link Cited by: §1. Blackburn et al. (2001) P. Blackburn, M. de Rijke, and Y. Venema Modal Logic. Cambridge University Press. External Links: ISBN 9781107050884, Document, Link Cited by: §2.1.3, §8. Caminada and Amgoud (2007) M. Caminada and L. Amgoud On the evaluation of argumentation formalisms. Artificial Intelligence 171 (5-6), p. 286–310. External Links: Document, Link Cited by: §I.2, §8. Caminada (2006) M. Caminada On the Issue of Reinstatement in Argumentation. In Logics in Artificial Intelligence, p. 111–123. External Links: ISBN 9783540396277, Document, Link Cited by: §4, §8. Chesñevar et al. (2006) C. Chesñevar, J. McGinnis, S. Modgil, I. Rahwan, C. Reed, G. Simari, M. South, G. Vreeswijk, and S. Willmott Towards an argument interchange format. The Knowledge Engineering Review 21 (4), p. 293–316. External Links: Document, Link Cited by: §8. Clark et al. (2014) T. Clark, P. N. Ciccarese, and C. A. Goble Micropublications: a semantic model for claims, evidence, arguments and annotations in biomedical communications. Journal of Biomedical Semantics 5 (1). External Links: Document, Link Cited by: §8. Cramer and Friese (2026) M. Cramer and T. Friese Satisfying Rationality Postulates of Structured Argumentation Through Deductive Support – Technical Report. External Links: 2604.21515, Link Cited by: §8. Dung (1995) P. M. Dung On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence 77 (2), p. 321–357. External Links: Document, Link Cited by: §1, §2.1.2, §4, Definition 6.2, §8. Grossi (2010) D. Grossi On the Logic of Argumentation Theory. In Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), p. 409–416. External Links: Link Cited by: §8. Howitt and Wilson (2014) S. M. Howitt and A. N. Wilson Revisiting “Is the scientific paper a fraud?”: The way textbooks and scientific research articles are being used to teach undergraduate students could convey a misleading image of scientific research. The EMBO Reports 15 (5), p. 481–484. External Links: Document, Link Cited by: §1. Kadaboina (2026) R. K. Kadaboina Pramāṇa: A Protocol-Layer Treatment of Claim Verification in Autonomous Agent Networks. Zenodo. External Links: Document, Link Cited by: §8. Kripke (1963) S. A. Kripke Semantical Considerations on Modal Logic. Acta Philosophica Fennica 16, p. 83–94. External Links: Link Cited by: §2.1.3, §8. Liu et al. (2026) J. Liu, J. Pei, J. Huang, C. Si, A. Qu, X. Tang, R. Lu, L. Chen, X. Bai, H. Zheng, C. Chen, Z. Chen, H. Ye, Y. Fu, Z. He, Z. Jin, Z. Zhang, S. Sun, M. Harmon, J. D. Wang, J. Zeng, J. Sun, M. Wu, B. Zhou, C. You, S. Lu, Y. Qiu, F. Lai, Y. Yuan, Y. Li, J. Hong, R. Zhu, B. Chen, A. Pentland, A. Chen, M. Chowdhury, and Z. Zhang The Last Human-Written Paper: Agent-Native Research Artifacts. External Links: 2604.24658, Link Cited by: §1, §2.1.1, §7.6, §8. Lu et al. (2024) C. Lu, C. Lu, R. T. Lange, J. Foerster, J. Clune, and D. Ha The AI Scientist: Towards Fully Automated Open-Ended Scientific Discovery. External Links: 2408.06292, Link Cited by: §1, §2.1.1. Medawar (1996) P. Medawar Is the scientific paper a fraud?. In The Strange Case of the Spotted Mice and other classic essays on science, p. 33–39. Note: Originally published in The Listener 70 (1963), p. 377–378 External Links: ISBN 9781383003093, Document, Link Cited by: §1. Miller (2015) D. Miller Foundational Proof Certificates. In All about Proofs, Proofs for All, D. Delahaye and B. W. Paleo (Eds.), Mathematical Logic and Foundations, Vol. 55, p. 150–163. External Links: Link Cited by: §1, §8. Modgil and Prakken (2014) S. Modgil and H. Prakken The ASPIC+ framework for structured argumentation: a tutorial. Argument & Computation 5 (1), p. 31–62. External Links: Document, Link Cited by: §8. Necula (1997) G. C. Necula Proof-carrying code. In Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL ’97, POPL ’97, p. 106–119. External Links: Document, Link Cited by: §1, §2.3, §8. Oikarinen and Woltran (2011) E. Oikarinen and S. Woltran Characterizing strong equivalence for argumentation frameworks. Artificial Intelligence 175 (14-15), p. 1985–2009. External Links: Document, Link Cited by: §8. OpenAI (2026) OpenAI Research Acceleration: The View Inside OpenAI. Note: OpenAI Economic Research External Links: Link Cited by: §1. Pandžić (2022a) S. Pandžić A logic of defeasible argumentation: Constructing arguments in justification logic. Argument & Computation 13 (1), p. 3–47. External Links: Document, Link Cited by: §8. Pandžić (2022b) S. Pandžić Structured argumentation dynamics: Undermining attacks in default justification logic. Annals of Mathematics and Artificial Intelligence 90 (2-3), p. 297–337. External Links: Document, Link Cited by: §8. Recht et al. (2019) B. Recht, R. Roelofs, L. Schmidt, and V. Shankar Do ImageNet Classifiers Generalize to ImageNet?. In Proceedings of the 36th International Conference on Machine Learning, K. Chaudhuri and R. Salakhutdinov (Eds.), Proceedings of Machine Learning Research, Vol. 97, p. 5389–5400. External Links: Link Cited by: §1. Ren (2026) J. Ren Evidence-Grounded Verified Agentic Reasoning: A Path Toward Eliminating LLM Hallucination in Empirical Inference via Tool-Attested Kernel Proofs. External Links: 2607.12650, Link Cited by: §8. Tang et al. (2026) Q. Tang, T. Sun, X. Hu, X. Liu, Y. Chen, Y. Shao, B. Li, C. Lv, C. Xu, C. Huang, C. Li, D. Xue, H. Bai, H. Duan, H. Guo, H. He, H. Chen, H. Shen, J. Yuan, J. Sun, J. Cheng, J. Xu, J. Tong, J. Chen, J. Liu, J. Leng, J. Yu, K. Jiang, K. Xiang, K. Yao, L. Feng, L. Yuan, L. Gao, M. Li, Q. Jia, Q. Sun, S. Ding, S. Gong, S. Zhong, T. J. Zhang, T. Gu, T. Liang, W. Liu, W. Yang, W. Fei, X. Wang, X. Liu, X. Ding, Y. Tang, Y. Wang, Y. Jiang, Y. Yang, Z. He, Z. Chen, Z. Xu, Z. Li, and Z. Huang FARS: A Fully Automated Research System Deployed at Scale. External Links: 2606.31651, Link Cited by: §1. Tregoning (2026) J. S. Tregoning Is the scientific paper still a fraud?. PLOS Biology 24 (8), p. e3003912. External Links: Document, Link Cited by: §1. van Benthem and Pacuit (2011) J. van Benthem and E. Pacuit Dynamic Logics of Evidence-Based Beliefs. Studia Logica 99 (1-3), p. 61–92. External Links: Document, Link Cited by: §8. van Benthem et al. (2014) J. van Benthem, D. Fernández-Duque, and E. Pacuit Evidence and plausibility in neighborhood structures. Annals of Pure and Applied Logic 165 (1), p. 106–133. External Links: Document, Link Cited by: §8. Walton et al. (2008) D. Walton, C. Reed, and F. Macagno Argumentation Schemes. Cambridge University Press. External Links: ISBN 9780511802034, Document, Link Cited by: §3.3. Yu and Zenker (2020) S. Yu and F. Zenker Schemes, Critical Questions, and Complete Argument Evaluation. Argumentation 34 (4), p. 469–498. External Links: Document, Link Cited by: §8. Zhang et al. (2026) K. Zhang, P. G. Candela, S. Murthy, Y. Xie, Z. Wang, and M. Raissi Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization. External Links: 2606.31002, Link Cited by: §8. Appendix Appendix A Mechanization status We map each formal result of Section 6 to its Lean 4 status. Five tables record the thirty-five mechanized specification results, one per pipeline stage: checking and compilation (Table 3), semantics-parametric observation and aggregation (Table 4), strict-certificate backends and linking (Table 5), source updates and the surface layer (Table 6), and cross-context guarantees, presentation, and cost (Table 7). The named guarantees G1–G6 all fall in the first three stages, and each row there names the guarantee it serves. A sixth table (Table 8) lists the source-boundary admission family of Property 1–Property 8. The audited public theorems are sorry-free and stay within Lean’s standard axiom trio. The audit checks their transitive axiom dependencies and requires coverage of public theorems and lemmas. Some private executable examples use native_decide, whose generated axioms add trust in native evaluation; the three-axiom claim excludes those examples. The local Lean gate and optional Lean CI workflow run the audit. Required CI checks Haskell; cross-language checks run locally. The pipeline cost bound (Proposition 6.2), the NP-completeness bookkeeping behind Theorem 6.18, and the closure and indirect-consistency clauses of Theorem 6.6 are argued on paper (Appendix I); the first two have no row. Table 3: Mechanization status, stage 1: checking and compilation. Results 1–8 of the thirty-five mechanized specification results. # Guarantee Result Stated as Lean status 1 G1 Decidable checking Theorem 6.1 mechanized 2 – Conclusion uniqueness, support adequacy Proposition 6.1 mechanized 3 G2 Dependency accountability Theorem 6.2 leaf half mechanized; backend half mechanized for all four backends (Section 3.4) 4 G3 Compilation soundness Theorem 6.3 mechanized 5 – Grounded termination, determinism Theorem 6.4 mechanized 6 G3 Status preservation Definition 6.1, Theorem 6.5 mechanized 7 – Image necessity, invariant transport Theorem F.1 mechanized 8 – Fixed-policy non-sufficiency Proposition F.1 mechanized, with an executable accepted anchor Table 4: Mechanization status, stage 2: semantics-parametric observation and aggregation. Results 9–13. # Guarantee Result Stated as Lean status 9 – Parametric observation; the printed status is the grounded instance Definition 6.2–Theorem 6.8 mechanized 10 – gap independence; stable nonexistence; ten pairwise separations Proposition H.1, Proposition H.2 mechanized, observation table generated from the definitions 11 – Source-level observation transport Theorem H.1 mechanized, with a counterexample for the dropped support bound 12 G6 Consistency of the aggregation Theorem 6.6 direct consistency mechanized, reference checker; closure clauses on paper 13 – Quarantine non-promotion Theorem 6.7 mechanized Table 5: Mechanization status, stage 3: strict-certificate backends and linking. Results 14–22. # Guarantee Result Stated as Lean status 14 – Strict-backend isolation, non-factivity Theorem 6.9 mechanized 15 G4 Strict-certificate soundness Theorem 6.10 mechanized 16 G4 Backend soundness, dependency accounting Section 3.4 mechanized 17 – Heterogeneous compositionality, dependency union Theorem 6.12 mechanized, with a mixed-backend witness 18 G5 Backend replacement Theorem 6.11 mechanized, with transport 19 – Contextual representation independence Theorem E.1 mechanized, with a certificate-bearing witness 20 – Contextual congruence at every semantics; grounded instance as an equivalence Theorem E.2 mechanized, with an all-context separation 21 – Typed term-level critical-question holes Theorem E.3 mechanized, nested witness with a substituted attack 22 – Relational parametricity over partial-bijective certificate relations Theorem E.4 mechanized; partial bijectivity witnessed necessary at the observation Table 6: Mechanization status, stage 4: source updates and the surface layer. Results 23–28; no named guarantee falls in this stage. # Result Stated as Lean status 23 Update acceptance preservation Theorem 6.13 mechanized 24 Grounded transition matrices Theorem 6.14 mechanized; matrices generated from the witnesses 25 gap boundary; public layer; matrix non-promotion Theorem 6.15, Corollary 6.16 mechanized, with the non-clean counterexample 26 Surface elaboration preservation Theorem G.1 mechanized 27 Supported-fragment reflection Theorem G.2 mechanized 28 Surface observation coherence Theorem G.3 mechanized, five instantiated corollaries Table 7: Mechanization status, stage 5: cross-context guarantees, presentation, and cost. Results 29–35; no named guarantee falls in this stage. # Result Stated as Lean status 29 Outer modal layer: normality, comparison adequacy, conservativity Theorem 6.19 mechanized; T/D/B/4/5 refuted in generic models 30 Exact cross-context support transport, path composition Theorem 6.20 mechanized, with the status-flip boundary witness 31 Conditional cross-context status preservation, modal collapse Theorem 6.21 mechanized, with a sound and complete bridge decider 32 Presentation-codec round trip Section 3 mechanized, with a cross-language shape guard 33 Well-sortedness of every atom an accepted unit reaches Section 3 mechanized 34 Direction-of-goodness contract for comparison Section 3 mechanized 35 Grounded query bounds, quartic tightness; 3SAT reduction correctness, realization, size Theorem 6.17, Theorem 6.18 mechanized; NP-completeness bookkeeping on paper A.1 Narrower scopes and component-level results Two guarantees have narrower scopes. The backend half of dependency accountability (G2, Theorem 6.2) is an interface obligation: we mechanize it for all four registered backends and require future backends to discharge it. The direct-consistency clause of G6 (Theorem 6.6) is proved for the executable reference checker over complete claims from an accepted unit, not over arbitrary caller-supplied claims; its closure and indirect-consistency clauses are paper arguments over the mechanized edge relation. The byte-exact tests against that reference provide conformance evidence rather than a replacement for the theorem. Four further results are unnumbered because they concern components rather than the calculus: each registered backend’s soundness and dependency accounting (Section 3.4); the presentation-codec round trip over the complete program and policy syntax of Section 3, which a cross-language shape guard pairs with a constructor-by-constructor comparison of the Lean and Haskell abstract syntax, so neither can change alone; well-sortedness of every atom an accepted unit reaches, which a substitution lemma carries from the sorted policy patterns (Section 3.1); and the direction-of-goodness contract for comparison, where the generated ord@1 goal holds exactly when the favored system is better under the measurand’s declared polarity, so a polarity error requests the opposite comparison rather than a weaker one. Two representation details fall outside the shape comparison: both languages normalize sort names to bare strings, and each keeps its own s-expression type for certificate payloads. The round trip concerns abstract syntax rather than parsing. The surface calculus separately proves elaboration preservation, reflection, and observation coherence above the parsed-AST boundary (Appendix G). The Haskell parser and elaborator remain validated implementations of those definitions. Lean also verifies the lowering of symbolic certificate premise references to numeric slots, with conformance vectors for the Haskell implementation. A.2 The source-boundary admission family The admission judgment of Figure 10 carries eight properties, numbered on their own counter and kept separate from the specification results because they fix the checking context rather than the core semantics. The metatheory overviews the three that carry its results to the boundary (Section 6): Property 3, Property 6, and Property 8. We state all eight here, each citing its headline Lean declaration. Property 1 (Judgment/evaluator correspondence). The declarative admission relation and the executable evaluator agree in both directions (evaluateAdmission_iff_judgment), so the relation is functional (admission_deterministic). Property 2 (Exact aligned checker context). Accepted outcomes require the metadata and declared leaf-id sequences to agree position-by-position (accepted_metadata_aligned). A leaf is policy-admitted iff it is declared with decision admit (policy_admitted_iff), and it is in the final checked context iff it is policy-admitted and not group-quarantined (checked_admitted_iff). That context is exactly the leaf table carried to the checker (accepted_checked_context_exact); policy-quarantined leaves are absent from it (policy_quarantined_absent). Property 3 (Endpoint-safe attack pruning). An accepted outcome’s semantic attack list is the successful resolution of the declared raw attacks (accepted_resolved_aligned). Resolution first establishes that every raw attack names declared argument identifiers. The retained semantic attacks are then exactly the raw-endpoint-filtered aligned projection of that validated list (retained_attacks_selectAligned), and every retained raw attack names retained endpoints (retained_attack_endpoints). Thus, two arguments with equal support terms stay distinct. Property 4 (Canonical audit exactness). The audit equals the combined prune’s exact projection with canonical multiplicity and order (admission_audit_exact). Property 5 (All-admit checker-outcome identity). When every table row admits (including an empty table), the prune, keep predicates, and blocked queries coincide with the group-only path (policy_all_admit_group_identity). Applying the actual checkUnit function produces the identical accept/reject outcome (policy_all_admit_checkUnit_identity). Property 6 (Restrictiveness monotonicity). Tightening decisions from admit to quarantine can only remove leaves, arguments, and attacks (more_restrictive_cannot_add_structure); claim statuses are deliberately non-monotonic, which is exactly the hazard Theorem 6.7 manages. Property 7 (Rejection carries no checked unit). An R8 outcome names the first rejected leaf and carries no checked unit (source_reject_no_checked_unit). Property 8 (Source non-promotion). A query published justified by the checked source result (with the prune’s exact keep predicates and aligned attacks) remains justified in the declared framework with the policy- and group-quarantined material reinstated (source_justified_nonpromotion). This instantiates the production blocking theorem of Theorem 6.7 from the admission carrier. Table 8: Mechanization status of the source-boundary admission family (Section 4, Figure 10), stated as Property 1–Property 8. Every result has an audited public theorem that is sorry-free and uses only Lean’s standard axiom trio. The local Lean gate and optional Lean CI workflow run the audit. # Result Stated as Lean status 1 Judgment/evaluator correspondence Property 1 mechanized 2 Exact aligned checker context Property 2 mechanized 3 Endpoint-safe attack pruning Property 3 mechanized 4 Canonical audit exactness Property 4 mechanized 5 All-admit checker-outcome identity Property 5 mechanized 6 Restrictiveness monotonicity Property 6 mechanized 7 Rejection carries no checked unit Property 7 mechanized 8 Source non-promotion Property 8 mechanized Appendix B Measurement inventories This appendix records the trusted base, implementation conformance checks, ablations, and checker timings that support Section 7. Measurements are generated from the implementation repository at separately recorded revisions. The current implementation inventory and differential checks use b62d33e0; the ablations use 7d0f7384, and the performance table uses 5d326b8. Historical measurement-harness counts below retain their 89c25ef snapshot. B.1 The trusted base Acceptance depends on nine trusted components: the decode boundary (presentation parser and wire decoder), the proposition normalizer and its identity relation, the static checker for leaf admission, policy instantiation, and support-term typing, the policy well-formedness validator, the typed-attack checker, the strict-backend registry and each shipped adapter, the compiler, the status engine, and the located rejection diagnostics. The signature Σ , the versioned policy Π , the backend registry R, and the policy-allowlisted theory digests are trusted inputs rather than trusted code: a program may instantiate them but can never define them at run time (Theorem 6.9). Everything else is untrusted, including the elaborator, every backend proof term, and any producer of the wire program. The strict kernel performs normalization, mediates the backend interface, and runs the four registered certificate checkers. Its guarantees depend on each backend’s encoding, consequence relation, and dependency laws. B.2 Conformance checks The production checker implements the complete pipeline in Haskell: parser, policy validator, support and attack checker, the nd@1, ra@1, ord@1, and insp@1 strict backends, compiler, grounded evaluator, and status engine. Its trusted base is a strict subset of that pipeline, enumerated in Section B.1. For the core calculus, compiled Lean semantics is the executable reference interpreter, and a differential harness runs every committed fixture, example program, and replay bundle through both drivers, requiring byte-identical reports and exit codes. A separate admission differential compares the Haskell pruning primitives with Lean: all 15 semantic outcomes agree byte for byte, and five malformed adapter fixtures fail at both codec boundaries. Properties also exercise the integration of admission with checking. The surface elaboration theorems start at a parsed AST (Appendix G); the Haskell parser and elaborator are validated by tests. The property suite and minimal negative programs exercise rejection classes and acceptance invariants. At b62d33e0, the core differential agrees on 673/673 verdict-bearing inputs and 66/66 malformed inputs; three further depth-bound cases also agree. The verdict-bearing inputs include both accepted programs and expected semantic rejections. Seeded answer keys check diagnostic locations. A digest-pinned replay bundle rejects tampered inputs, and a 78-row constructor inventory checks agreement between the Lean and Haskell abstract syntax. A separate 25-case suite checks surface conformance. These are conformance checks on finite suites, not an equivalence proof for the implementations. The mutant and rejection-class inventory follows below. B.3 Mutants and rejection classes The historical measurement harness at 89c25ef drove 541 mutant programs and 60 corpus units, agreeing with expected rejection classes and Lean on 601/601 inputs. Among its mutants, 113 are signature attacks, nine are quarantine-attacker mutants, and 31 are localization mutants whose defect manifests away from the edited site or at two sites at once. The localization families carry a seeded answer key re-derived from the mutant rather than copied from the checker, and a generation-time gate compares the two, so a mislocating checker fails the build instead of lowering a reported rate. The checker has fourteen rejection classes, each with a runnable minimal negative program: eleven use core fixtures, signature and codec failures have separate fixture families, and admission rejects at the source boundary. Both the production driver and the Lean reference driver reject malformed inputs at the codec boundary. B.4 Ablating the checks Three ablations test whether obligations, typed attacks, and the conflict scan affect acceptance. Each reruns the 655-input manifest at 7d0f7384 with a check removed: no-CQ skips the discharge of open critical-question obligations, no-conflict-scan skips the scan that demands an attack between contrary complete arguments, and no-typed disables the typed-attack check together with that scan, reducing the checker to nodes with arbitrary attack edges. Since all three only remove rejections, every regression is a program that the full checker rejects and the weakened checker accepts. The ablations expose distinct failure classes (Table 2). Removing obligation discharge admits precisely the 18 incomplete-argument mutants. Removing the conflict scan admits precisely the five mutants that drop the covering attack between contrary complete arguments, the configuration Theorem 6.6 presupposes never survives checking. The no-typed baseline admits those five plus the 32 bad-target or unlicensed-attack mutants, 11 in class R10 and 21 in R11; no ablation changes any other case. The admitted mutants span justified, defeated, and contested outcomes, so the weakened checkers issue statuses for programs that should have been rejected. B.5 Checker performance Table 9: Production-checker performance. End-to-end is decode + check + verdict render. Marginal decode cost is estimated by subtracting the predecoded kernel median from the end-to-end median per unit. Other phases use pre-forced inputs; check and evaluation include result rendering, so phases need not sum exactly. median worst Corpus unit, end-to-end (µs s) 629.6629.6 675.3675.3 estimated marginal decode (µs s) 351.8351.8 377.6377.6 check + render, pre-decoded (µs s) 281.3281.3 316.4316.4 validate (µs s) 0.00.0 0.20.2 check (µs s) 269.9269.9 313.0313.0 compile (µs s) 0.00.0 0.90.9 evaluate (µs s) 0.90.9 1.91.9 Per-artifact total (27 artifacts, µs s) 1278.91278.9 2503.72503.7 Framework size (nodes / edges) 0 / 0 2 / 1 Lean reference driver, subprocess (msms) 4.04.0 5.05.0 601-record harness, one full pass (msms) 246.8246.8 We report wall-clock time for the 60 corpus units and the 601-record harness at 5d326b8, measured on one machine with an Apple M5 Pro chip, 64 GB64\,GB RAM, darwin/aarch64, GHC 9.14.1, and Lean 4.32.0. Each Haskell time in Table 9 is an in-process median over 5 sections of 100 batched runs each. The median corpus unit takes about 630 µs630\, s end to end, and the predecoded check-plus-render kernel takes 280 µs280\, s. For each unit, the harness estimates marginal decode cost as the nonnegative difference between these two medians; the reported median of those estimates is about 352 µs352\, s. This row is not a separately timed parser stage. The check and evaluation phases include rendering their results to force evaluation. The check phase includes signature and sort checking, but the timings do not isolate their contribution. Validation, compilation, and evaluation each remain below 2 µs2\, s in this protocol. One pass over the 601-record harness takes about 250 ms250\,ms, so the differential suite runs interactively. The Lean reference driver handles the same inputs in about 4 ms4\,ms of subprocess wall time, including startup and decoding. This protocol is not comparable to the in-process production measurements, but it is fast enough to adjudicate every test input. Two independent benchmark runs agree within 3% on every reported median and within 1% on most. A make bench target in the supplemental artifact regenerates the table. The compiled frameworks contain at most two nodes and one edge per corpus unit. These timings establish low overhead on small inputs, not scalability on large argumentation frameworks. Appendix C Exploratory corpus study Table 10: Critical-question obligations generated by the 60-claim sample. Unmet mandatory questions surface as located gaps; only three act as defeaters: the gap-versus-defeated split in the data. Met Unmet (gap) Unmet (defeater) Total Mandatory 105 68 3 176 Optional 34 39 0 73 Total 139 107 3 249 The corpus study is exploratory. Its statuses describe the encoded artifacts under the selected policy and machine annotations, rather than the validity of the underlying research claims. We began with a 32-artifact corpus of paper-derived and agent-generated research artifacts. From its 231 claims and 279 recorded dead ends we drew a stratified 60-claim sample spanning 27 artifacts. One machine annotation pass per artifact classified each claim’s inference scheme, leaf grain, critical questions, strict-certifier demand, and attack candidates under a shared codebook; the supplemental artifact ships that codebook and the stratification. A second machine annotation pass, blind to the first, reclassified the claim type for 18 of the 60 claims and agreed on 14 (κ=0.73κ=0.73). Three measurements follow, each stated over its own denominator. Missing support in the encoded artifacts Of the 60 sampled claims, 48 are gap, nine are justified, and three are defeated. None is contested. Four claims in five lack complete support in their encodings under the selected policy; this does not establish that the original investigations lacked support. The 249 critical-question obligations those claims raise locate where the support stops (Table 10): 71 of the 176 mandatory questions go unmet, 68 of them as located gaps and three as defeaters. The verdicts that do go through rest on 38 load-bearing leaves, all agent-produced, of which 20 are attested and 18 observed; 15 point directly to an equation, table, figure, or theorem in a paper. Table 11: Inference-scheme families over the 60-claim sample; the top three carry 77%. Scheme family Claims Controlled comparison 25 Intervention and ablation 14 Observation and measurement 7 Analytic argument 4 Benchmark or stress evaluation 3 Code inspection 3 Statistical correlation 2 Inductive generalization 1 Blind paired human evaluation 1 Total 60 Scheme coverage Nine inference-scheme families cover all 60 sampled claims, and the top three cover 46 of them (Table 11). The sample also demands little heavyweight logic: 35 of the 60 claims call for a domain checker, mostly to recompute arithmetic from reported tables, while three call for the Logic of Proofs and one for natural deduction. That distribution motivates a registry of small certified checkers rather than one fixed calculus, and the corpus exercises exactly one of them on an accept path. adaptive-pruning/C04 rechecks score cells from Table 5 through the strict rational_drop_recheck scheme, and a checked ra@1 certificate representing the claimed drop as an exact reduced fraction discharges it; the headline claim nonetheless stays gap because its variance question is unmet. Four of the five units documenting strict-flavored steps carry no checked certificate in this study snapshot. A preliminary annotation and design assessment judged roughly 90% of the 60 sampled argument shapes expressible under the proposed encoding conventions. Its six residual cases concerned equivalence schemes, monotone functional relationships, parametric growth rates, distribution-valued leaves, negative existentials over code, and graded or undefined predicates. This assessment measures judged expressibility, not compiler acceptance. The nine scheme families classify all sampled claims without establishing successful encoding of every argument shape. The later insp@1 backend checks a restricted form of negative existential over a declared exhaustive inventory; it does not verify that the inventory faithfully describes the source code. Few recorded attacks Three typed attacks validate across the 60 claims, all of them undercuts: two from exploration traces and one from a paper’s own table. Among 194 classified dead ends, four are undercut candidates and only one executes as a claim-defeating attack, the rest being rejected alternatives rather than defeaters. The sample does not establish why so few attacks are recorded: it cannot separate omissions in the original record from annotation or encoding limitations. Both trace-sourced undercuts defeat their target claims. We use authored adversarial programs to exercise defeat structures absent from the corpus, with further case studies in Appendix D. C.1 Study limitations The study uses a single machine annotation pass per artifact, with human review pending. We double-annotated only the claim-type field on 18 of the 60 claims. The 32-artifact corpus was assembled rather than sampled from a frame, so its distributions carry no external-validity claim. The study does not evaluate bridge discovery or automated literature-based review. Appendix D Case studies These case studies ask what researchers gain by expressing their claims and evidence as Lara programs. Lara makes the connection between evidence, inference, and objection explicit: the checker validates the declared support and attacks, then computes which claims remain supported. We first demonstrate three uses of this capability: replaying how a rebuttal changes support, explaining a verdict as a review comment, and distinguishing conflicting conclusions from conclusions about different settings. Two further studies use no measurements: a philosophical debate shows how assumptions and attributed premises support defeasible arguments, and an axiom-withdrawal example shows when a checked deduction can be reused in another context. Together, the studies demonstrate that Lara checks the structure and standing of support across different kinds of inquiry. The sampled corpus retains little defeat (Appendix C): three undercuts, no rebuttals or underminings, no contested claims, and no round in which new evidence changes a status. The worked-example suite does exercise defeat, reinstatement, and contestation, but each of those programs isolates one behavior in an authored setting. The first three studies exercise these mechanisms over material from real corpus units or families. The differential harness replays the underlying checked programs byte-for-byte through the production checker and the Lean reference driver. Below we show only the declarations that distinguish the relevant rounds or outcomes; the fuller listings are Listing J.2, Listing J.3, and Listing J.4, and the anonymized supplemental artifact carries the complete programs, policies, replay commands, and golden reports. Scope We hand-lowered the first three studies under the corpus-unit discipline and anchored them to real units and families. We did not mine them from review threads at scale. In particular, the first study derives its reviews and rebuttal from a documented corpus gap rather than from an OpenReview exchange. Scaling to real review threads and correlating Lara verdicts with human complaints require a separate empirical study. The two non-empirical studies are authored demonstrations; we cite their committed programs and distinguish their execution paths below. Within that scope, the studies establish that Lara’s support checks and attack semantics work together in these research situations. Researchers still supply the formal claims, evidence declarations, and objections; Lara checks their consequences under the chosen policy. These studies do not establish automatic extraction from papers, agreement with human reviewers, or the truth of the encoded claims. Table 12: Per-claim status across the rebuttal exchange, in which only the argument population grows. c_bench is reinstated across an undermine and a rebut, c_kurt discharges the variance gap the corpus unit already records, and c_measure is conceded. Claim Round 0 Round 1 Round 2 submission reviews rebuttal c_bench (APT vs. dense on OpenLLM) justified defeated justified c_kurt (kurtosis-salience term critical) gap gap justified c_measure (low training-memory footprint) justified defeated defeated D.1 A rebuttal exchange as three checked programs The first study asks whether a reader can trace exactly why a claim gains or loses support during review. The submitted paper, the review round, and the rebuttal form one framework whose argument population grows: reviews add typed attacks to the paper’s arguments, and a rebuttal adds evidence leaves and counterattacks. Lara represents each round as a separate program, all three sharing one artifact identity and one fixed policy because they concern the same paper under the same standard. Grounded semantics re-adjudicates the graph after each round, so claim statuses change non-monotonically while the policy stays fixed. ⬇ 1 # ROUND 0 -- missing variance evidence means no a_kurt 2 claim c_kurt 3 formal = contributes(kurtosis_salience, apt_llama2_7b, openllm_avg) 4 # ROUND 1 -- one attack of each kind 5 undermine d_um a_bench.protocol_fixed.leaf 6 rebut d_rebut a_bench 7 rebut a_bench d_rebut 8 undercut d_meas a_meas.rule 9 # ROUND 2 -- new evidence completes a_kurt; counter-attacks reinstate a_bench 10 leaf rk_var : variance_reported(e03) 11 arg a_kurt : supports(c_kurt) by component_ablation(kurtosis_salience, apt_llama2_7b, openllm_avg, e03) 12 discharge variance_reported with rk_var 13 undermine r_um d_um.leaf 14 undercut r_rebut d_rebut.rule Figure 13: The language-level deltas across the three rounds (non-contiguous excerpts). Round 2 adds no defense for the conceded measurement claim. The supplemental artifact holds the repeated declarations, evidence metadata, policies, and complete programs, which the differential harness replays byte-for-byte through both drivers (Table 12). The exchange starts from adaptive-pruning/C04. Its kurtosis-salience ablation has only one run, and no leaf discharges the mandatory variance_reported question. The corpus therefore assigns the claim gap (Appendix C). We lift three claims from that paper into the exchange. We show the declarations that change across rounds in Figure 13; the fuller presentation appears in Listing J.2. At submission, c_bench and c_measure have complete arguments. The missing variance leaf leaves c_kurt without a supporting argument and reproduces the corpus gap. We omit that argument because an instance with an unanswered mandatory question would be rejected; the claim itself can remain in the accepted program. The reviews use different attack forms because their objections challenge different parts of the support. The protocol objection disputes an evidence premise, so an undermine targets the benchmark’s fixed-protocol leaf. The replication supplies a conflicting conclusion, so a rebut targets the benchmark argument’s conclusion. The memory objection challenges the inference from a measurement to the claimed footprint, so an undercut targets that argument’s rule. These positions tell the checker which support each objection can defeat. The rebuttal supplies the variance leaf and adds an ablation argument that uses it to discharge the obligation, so c_kurt moves from gap to justified. The new leaf alone would not supply an argument. A counter-undermine and counter-undercut defeat both benchmark attackers, reinstating c_bench. The author concedes the memory point by adding no counterargument, so c_measure remains defeated: concession is the absence of a defense rather than a special construct. Every one of these moves comes from the growing graph, since the standard never shifts. The case shows why Lara is useful for a rebuttal: it separates completing missing support, defending existing support, and leaving a defeat unanswered. A reader can replay each outcome from the declared changes under the same policy. The status table therefore records the consequences of the exchange, with the responsible arguments and attacks available for inspection. D.2 Verdicts rendered as reviews The second study asks whether a checked verdict can explain what an author needs to address. Lara distinguishes a claim with no complete supporting argument (gap) from one whose complete arguments have been defeated (defeated). This distinction matters for review: supplying a missing argument and answering an objection are different tasks. A deterministic renderer reads the checker’s per-claim verdict and located diagnostic, then fills a fixed phrasing table keyed on the diagnostic shape. It uses no free-text generation and adds no trusted code. We condense the two diagnostic shapes in Figure 14 and give the verbatim rendered output in Listing J.3. gap: adaptive-pruning/C04. No checked argument assembles the unit’s evidence; the complete-support set is empty. The review asks for a support argument at the corpus-v1 evidential bar. defeated: fre/C04. The only support a1 is out: unattacked undercut d1 challenges its variance_reported critical question. The review names both the attacker and the failed question. Figure 14: Two diagnostic shapes rendered from checked verdicts. The box compresses the renderer output to the located information a reviewer acts on; we give it verbatim in Listing J.3. Over the 60-unit corpus the renderer emits 51 review comments: 48 for gap claims and 3 for defeated ones; the 9 justified claims raise none. The templates report the checked status and relevant declarations, and a freshness test pins the rendered bytes. For the ablation gap, the comment identifies the absence of a complete argument; for the defeated claim, it names the attacker and the challenged question. The case shows that Lara can provide a traceable basis for review comments: readers can follow a diagnosis back to the checked support. The renderer does not discover scientific objections or assess novelty. Its contribution is to communicate the consequences of the evidence and objections already encoded in the program. D.3 Genuine versus apparent disagreement The third study asks whether apparently opposing findings actually concern the same comparison. We encode each conclusion with the systems, metric, and experimental setting it concerns. The policy declares better and not_better contrary only when these arguments match. Including the setting in the proposition lets Lara check whether a declared rebuttal concerns the same comparison. Two proposition pairs from the pruning family carry the same prose-level disagreement (Table 13); we give the complete encoding in Listing J.4. P1 shares one setting atom, so its declared mutual rebut becomes a 2-cycle and both claims are contested. P2 differs only at the setting atom, so no contrary instance and no edge form; both claims remain justified. The mutual attacks leave P1 without an accepted argument that resolves the conflict; contested preserves that unresolved state. Table 13: Cross-paper agreement map. Splitting the shared arguments from the setting atom exposes the semantic hinge: whether that one atom matches decides whether a contrary instance, and so an edge, exists. Pair Polarity Shared arguments Setting atom D Compiled outcome P1 better apt, cofi, accuracy roberta_mnli_s60 mutual rebut ⇒ both contested not_better roberta_mnli_s60 P2 better magnitude_pruning, dense_baseline, accuracy bert_glue_s50 no edge ⇒ both justified not_better llama_openllm_s90 Declining to attack is not asserting agreement. The setting-mismatch non-attack leaves an open comparability critical question naming the missing measurement, so non-comparability becomes a concrete request: a bridging experiment must report both systems at a shared setting. P1’s headline conclusions rest on defeasible steps only and satisfy the strict-chain restriction of Section 4. The case shows how Lara can make the scope of disagreement inspectable. Readers can see whether the encoded conflict concerns a shared setting or whether comparison still requires additional evidence. This capability depends on the supplied formalization: researchers must judge whether the setting identifiers faithfully represent the experiments. D.4 A philosophical debate without measurements Can Lara check an argument whose premises are assumptions and attributed positions rather than observations? This study reconstructs a small philosophy-of-mathematics debate under an authored philmath-v1 policy (ARA-Labs, 2026a). Every evidence leaf is assumed or attested, and the program uses no strict backend. The policy supplies the inference schemes, mandatory questions, contraries, and exceptions; the existing checker evaluates their instances. The encoding makes the disputed commitments explicit. An indispensability argument supports the existence of abstract mathematical objects, but must discharge a mandatory question about why indispensability warrants that commitment. A nominalist argument challenges its indispensability premise, subject to a separate assumption that the reconstruction covers the scientific fragment under discussion. We keep this claim separate from the stronger claim that numbers are intrinsically particular sets. The latter faces a mutual rebuttal from a structural-role account of number identity. These two arguments remain contested: the checker exposes the unresolved disagreement without choosing a side. A second exchange shows how a defense restores support. A fictionalist argument claims that mathematical usefulness need not require literal mathematical truth. An objector undercuts that inference; a reply that consistency suffices for the conservative applications at issue undercuts the objector in turn. The reply is unattacked, so the objector becomes out and the fictionalist argument becomes in. The committed defense-removal test deletes just the reply’s undercut and checks that the fictionalist claim changes from justified to defeated. We give the relevant declarations in Listing J.5; the complete program also defeats the indispensability argument through both a premise challenge and an undercut. This case demonstrates why Lara is useful beyond empirical review: it can require an argument to expose its assumptions, check that an objection targets the stated premise or inference, and compute the effect of a defense. The program and its golden verdict are registered in the worked-example and Haskell–Lean differential suites. These checks concern the encoded debate: the policy is authored, the prose-to-atom bindings remain explicitly unreviewed, and the result does not settle the philosophical positions it represents. D.5 Withdrawing an assumption blocks proof reuse The final study asks what happens to a checked deduction when another context withholds its premise. The source declares one assumed atom, parallel_postulate(), and a strict argument that reuses that premise through the production nd@1 backend (ARA-Labs, 2026b). The certificate (hyp 0) selects premise zero; the backend theory is empty, so the certificate cannot obtain the conclusion from an axiom hidden in that theory. The atom names an assumption for the demonstration: the program proves no geometric consequence. The source and admission choices appear in Listing J.6. The three admission policies isolate different outcomes (Table 14). Admission retains the premise and its argument, making the claim justified. Quarantine removes both but accepts the remaining program, whose claim is gap because no support remains. Rejection stops source admission and yields no checked claim status. Withdrawing a premise therefore differs from defeating an argument: this example contains no attack. Table 14: Assumption admission and proof reuse. The source files differ only in policy selection; each policy makes a different admission decision for the assumed leaf. Structural results come from the separate Lean witness. Decision Admitted support Local status Structural result admit Premise and argument retained justified Identity bridge transports checked support quarantine Premise and argument removed gap No structural bridge to the empty target evidence environment reject Source admission stops None No target checking environment supplied A separate executable Lean witness checks the structural transport boundary. When the assumption is retained at both ends, an identity bridge preserves the leaf and the support-transport theorem applies to the certificate-bearing argument. When it is withdrawn, the target has no admitted leaves. The executable leaf-preservation check fails, and the theorem no_withdrawn_bridge rules out any structural bridge to that empty target environment: no mapping can supply the required image of the source premise. This establishes a failure of the bridge contract, in addition to the locally computed change in status. Support transport alone does not assert status preservation. This case demonstrates what Lara adds around a deductive certificate: it makes admission of the certificate’s premises explicit and checks the conditions under which that support can be reused. The Haskell tests check source admission, local statuses, and the certificate’s dependency on premise zero; the Lean executable and proofs check the transport boundary. The current lara pw command refuses the quarantined world before loading bridges, so its refusal is not the structural-bridge result. Both demonstrations use the existing calculus; the new policy instances and Lean witness require no change to its kernel rules. Appendix E Contextual representation independence Backend replacement compares two whole programs. Interchangeability, however, is a claim about use: replacing a backend inside one fragment of a program must go unnoticed by every program that links against that fragment. This appendix adds the context quantifier. We define fragments and linking contexts, observe exported claim statuses, and prove that no admissible context can observe an acceptance-preserving backend replacement (Theorem E.1). Definition E.1 (Fragments, contexts, and linking). A fragment declares a signature, a policy, evidence leaves, a finite ground input, support terms, attacks, the leaf identifiers it imports from its environment, and the conclusions it exports for observation. A context is a fragment-shaped surrounding program. Linking a context C with a fragment F first runs a hygiene guard that rejects duplicate or clashing identifiers, unsatisfied imports on either side, and any signature or policy mismatch, so a context may add evidence, arguments, and attacks but may never redefine Σ or Π , and the registry R stays a fixed parameter of observation. A successful link merges the two sides, adds the cross-boundary attacks that the attack-completeness scan (Section 3.5) requires, and submits the linked program to the unchanged checker. Definition E.2 (Observation and contextual equivalence). The observation obsR(C,F)obs_R(C,F) is the link fault when the hygiene guard rejects, the checker error when the linked program is rejected, and otherwise the list of grounded claim statuses (Definition 4.3) of F’s exported conclusions in the linked program’s compiled structured framework. Fragments F1F_1 and F2F_2 are contextually equivalent under R when obsR(C,F1)=obsR(C,F2)obs_R(C,F_1)=obs_R(C,F_2) for every context C. A pair (C,F)(C,F) is admissible under R when the guard passes, each side’s terms and attacks check relative to the linked leaf environment, the linked program passes the signature stage, and the shared policy is well formed with distinct, in-scope rule declarations. A backend relabeling f maps certificate assurances to certificate assurances; f⋅Ff· F relabels F’s assurances pointwise and touches nothing else, and C is fixed by f when relabeling changes none of C’s terms or attacks. Theorem E.1 (Contextual representation independence). Let f be an injective backend relabeling and R1R_1, R2R_2 registries such that whenever R1R_1 accepts an assurance for a rule instance, R2R_2 accepts its relabeling under f. For every pair (C,F)(C,F) admissible under R1R_1 with C fixed by f, obsR1(C,F)=obsR2(C,f⋅F).obs_R_1(C,F)\;=\;obs_R_2(C,f· F). In particular, a registry that accepts every assurance R1R_1 accepts observes identically on every pair admissible under R1R_1, and the equation survives embedding C into a composed context that remains admissible and fixed by f. Each hypothesis carries content. Acceptance preservation runs forward only, so R2R_2 may accept assurances R1R_1 rejects; because the observation separates a rejection from a status list, an unconditional statement over every context would then be false. Admissibility cannot be dropped either, since linking is partial and a rejected pair observes its fault. The witnesses are not degenerate: a fragment carrying a checked nd@1 certificate, relabeled by a non-identity injection into a registry that expects the relabeled spelling, changes syntactically and keeps its observation (cert_congruence_witness). The theorem extends backend replacement (G5, Theorem 6.11) along the context quantifier, and the two results are incomparable: G5 quantifies over arbitrary whole checked programs with no admissibility hypothesis, while the congruence quantifies over admissible linking pairs, so the whole-program instance cites G5 rather than re-deriving it. Theorem E.2 (Contextual congruence at every semantics). Replace the grounded status readout in Definition E.2 by the claim observation of Definition 6.3 at an arbitrary extension semantics. Then Theorem E.1 holds verbatim at every extension semantics, with no additional hypothesis and in particular no attack-extensionality, and so do its acceptance-profile, composed-context, and whole-program forms. The grounded instance recovers Definition E.2 exactly, as an equivalence of relations. The generalization is not vacuous. The congruence needs no new hypothesis because it transports an equality of compiled carriers rather than pointwise attack agreement, yet the parameter matters at the context level: on a linked three-cycle, stable semantics observes the no-extension report where grounded observes contested, an arm the grounded reading cannot reach; and grounded contextual equivalence does not imply equivalence at every adequate semantics, since two fragments provably equivalent in every context under grounded are separated by an adequate singleton-selector semantics at one accepted context. That counterexample refutes the unrestricted implication only; it separates none of the four standard non-grounded instances. gap remains semantics-independent at the context level. Contexts can also owe a fragment more than evidence: an answer to a critical question is a support term inside a discharge map, which leaf imports cannot supply. A hole template extends support terms with named holes at answer positions; two nested instances may ask the same question yet demand different answers, and sharing a hole identifier forces the demanded answers to agree through a declared hole signature. A filling maps hole identifiers to core support terms. Theorem E.3 (Typed hole substitution). Erasing a template’s unanswered holes to open questions yields a typed source support term. Substituting a typed filling, complete support terms whose conclusions are equivalent to the demanded answers, derives support of the instantiated term with the same root conclusion and residual obligations, and an obligation-free instantiation crosses the unchanged compilation boundary. Instantiated linking is checked, closed embeddings recover the observations and contextual equivalence of Definition E.2 exactly, and the congruences of Theorem E.1 and Theorem E.2 pass through instantiation, provided the relabeling also fixes the certificates in the context’s fillings. That proviso is substantive: a mechanized witness fixes a context’s frame while a certified filling moves. The congruence quantifier itself also strengthens from a function to a relation, which is the sense in which backend interchangeability is parametric rather than merely representation-independent. Theorem E.4 (Relational parametricity). Let R relate certificate assurances such that (i) R is the graph of a partial injection; (i) acceptance transports from R1R_1 to R2R_2 along the pairs R relates, and only those; (i) fragments F1F_1 and F2F_2 agree on signature, policy, declared leaves, ground input, imports, and exports, with arguments and attacks pointwise R-related; and (iv) R relates the context’s own material to itself. Then for every pair (C,F1)(C,F_1) admissible under R1R_1, obsR1(C,F1)=obsR2(C,F2),obs_R_1(C,F_1)\;=\;obs_R_2(C,F_2), at every extension semantics. The graph instance of this theorem re-derives Theorem E.1 exactly, and the acceptance hypothesis can be localized to the fragment’s own certificate occurrences at the cost of two context-containment side conditions, a trade rather than a strengthening. Partial bijectivity is necessary, and the necessity is witnessed at the observation: a relation that collapses two distinct certificate payloads lets structural deduplication merge two wrappers of the same conclusion, an undercut on one wrapper then reaches the merged node, and the same exported claim changes from justified to defeated with every other hypothesis intact. Finitely much related material is always realized by some total injective relabeling that also fixes the context, while extending an arbitrary such relation to a total injection is refuted, so the residual gap between the relational and functional forms is acceptance scope alone. The honest name is therefore parametricity over partial-bijective certificate relations, not over arbitrary relations; and none of this is full abstraction, since we prove no logical-relation characterization of contextual equivalence. Two recorded obstructions gate that characterization. First, a fragment’s semantic interface is wider than its declared imports: the attack-completeness scan ranges over all argument pairs, and subargument closure feeds non-exported arguments back into exported statuses, so a logical relation over declared imports alone is refuted in both directions. Second, completeness is policy-conditional: under a policy with no declared conflict, no attack types and no context can separate fragments by forcing a label, the same degenerate policy as Proposition F.1. Appendix F The image of compilation We next ask which frameworks a checked program can denote. Every realizable structured framework satisfies the compiler invariant below, but the invariant is not sufficient for realizability under an arbitrary fixed policy. This result retains conclusion labels; it does not characterize the class of label-erased Dung frameworks. Definition F.1 (Structured framework and isomorphism). A structured framework F pairs a finite sequence of node conclusions with a total attack relation ↝F _F on positions. An isomorphism from F to G is a bijection σ on positions such that position i carries conclusion c in F exactly when σiσ i carries c in G, and i↝Fji _Fj iff σi↝Gσjσ i _Gσ j. Isomorphism is reflexive, symmetric, and transitive. An accepted program compiles to the structured framework whose conclusions are those of its complete arguments in declaration order and whose attack relation is the edge relation of Definition 4.1, read positionally. Definition F.2 (Compiler invariant). Fix Π ’s declared conflict data: its contrary pairs and exception conditions. A structured framework F satisfies the compiler invariant when (i) every edge stays in range: i↝Fji _Fj implies positions i and j both carry conclusions; and (i) conflict is complete: whenever the conclusions at positions i and j match under Π ’s declared contrary relation, i↝Fji _Fj. Definition F.3 (Realizability). Fix Σ , Π , and R. A realization of a structured framework F comprises a leaf table, a finite ground input, and a raw program that the executable checker accepts under them, such that the accepted program carries exactly the fixed Σ and Π , the ground input covers every leaf a declared argument uses, and the accepted program’s compiled structured framework is isomorphic to F. We call F realizable in that fixed context when a realization exists. Theorem F.1 (Image necessity). For every fixed Σ , Π , and R: a realizable structured framework satisfies the compiler invariant for Π ’s declared conflict data. The invariant transports across isomorphism, so the choice of realization witness does not matter. Necessity also carries sorts: in any realization, every node conclusion is well sorted under Σ , by the coverage hypothesis and the substitution lemma of Section 3.1 (node_conclusion_wellSorted). Proposition F.1 (The invariant does not imply realizability). Consider the structured framework with one node and one self-edge. For every Σ , Π , and R in which Π declares no contrary pair and no exception, that framework satisfies the compiler invariant, since conflict completeness is vacuous, yet it is not realizable: no attack can type under such a policy, so every compiled framework is edgeless, and an isomorphism preserves edges. The hypothesis is executable rather than degenerate, because the checker accepts a program under one such fixed context. The counterexample refutes sufficiency over arbitrary fixed policies. Sufficiency for policies with declared conflict remains open. Appendix G The verified surface boundary The surface calculus formalizes the presentation syntax of Section 3 above the parser boundary. We define an independent judgment for the full structured surface AST, prove that elaboration preserves and reflects checking, and prove that a claim observation taken directly on the surface output agrees with the core observation for every attack-extensional extension semantics. Parsing bytes into the AST stays validated, and every theorem begins at the parsed AST. Definition G.1 (Supported fragment and surface judgment). A surface input pairs a complete presentation program with its policy; the registry, identifier classifier, and proposition encoder stay parameters. The supported fragment is a decidable structural predicate over the full AST: the program names the supplied policy, and declaration identifiers, rule namespaces, value bindings, comparisons, inferred arguments, named certificates, attack paths, and premise labels satisfy the supported syntax restrictions. The surface judgment is a syntax-directed relation defined independently of the elaborator: it carries the supported fragment, independent expansion relations for values, prose interpolation, and comparisons, role, status, and group well-formedness, and declarative core obligations rather than a wrapper around executable success. Its executable checker is sound, complete, and deterministic for it. Theorem G.1 (Elaboration preservation). A derivable surface input elaborates successfully to its output, and the actual core checker accepts that output. Elaboration preserves the authored obligation ledger exactly, retains exactly the resolved attacks, preserves each reconstructed argument’s conclusion, and aligns the authored argument order with the core-visible question sequence. Theorem G.2 (Supported-fragment reflection). If a supported input elaborates successfully and the core checker accepts the result, then the surface judgment derives that elaboration. Both hypotheses are load-bearing: successful elaboration alone establishes neither the supported fragment nor core acceptance. The theorem reflects the given surface input, not arbitrary core units, so it claims neither surjectivity onto the core nor unique source recovery. Binding is verified at two grains: genuine binders (rule parameters and named certificate lambdas) admit alpha-equivalence with identical lowerings, and a typed global renaming of non-binder identifiers is equivariant for the whole pipeline under explicit structural and environment hypotheses, while replay-significant identities (backend names and versions, digests, policy identifiers) are not renamable at all. Theorem G.3 (Surface observation coherence). For a derivable surface input whose output the core checker accepts, a direct observation computed from the surface output alone, its retained arguments, resolved attacks, and reconstructed claims, without compiling, equals the core observation of the compiled framework, for every extension semantics with an attack-extensional specification, and hence for the five named instances. The stable instance preserves the no-extension report, and a missing claim identifier stays missing on both sides rather than becoming an empty-support gap. Appendix H Extension-semantics distinctions and source transport These results supplement the observation definitions of Section 6.3. They vary the extension semantics within a framework; the possible-world layer of Section 5 instead relates accepted programs and their checking contexts. Proposition H.1 (gap alone is semantics-independent). For every extension semantics and framework, a claim’s observation is gap if and only if its support is empty, with no further hypothesis. Each of the other three statuses varies with the semantics: on a two-cycle whose two arguments support the same claim, grounded observes contested where preferred observes justified, and a claim supported by an argument both cycle members attack moves from contested to defeated. All ten pairwise separations among the five instances are witnessed in one mechanized statement. Proposition H.2 (Stable nonexistence is reported, not resolved). The bare three-cycle has no stable extension, while the other four instances enumerate at least one there, so nonexistence belongs to stable semantics rather than to the framework; and it belongs to the bare cycle, since one added argument attacking all three members restores a stable extension. On the bare three-cycle, stable observation of any supported claim is the no-extension report, never a four-state status. Preferred extensions, by contrast, exist for every finite framework. Two refutations bound what any observation function could be. No four-state function realizes the credulous reading: under preferred semantics on the two-cycle, one claim is accepted in some extension and defeated in some extension at once, and the two cycle members carry identical acceptance profiles, so no framework-internal tie-break recovers a verdict (credulous_not_functional); the credulous reading stays exposed as per-argument bits, never as a status. The observation also does not factor through per-argument acceptance data (observe_not_determined_by_profile). Theorem H.1 (Source-level observation transport). Call a specification attack-extensional when two frameworks with equal carriers that agree on attacks between carrier members satisfy it for the same extensions; all five instances are. Fix such a semantics, a checked program P, and a claim whose support indices all lie among P’s arguments. Then a direct source-level observation, defined over every edge oracle that agrees with the declared checked attacks on declared arguments, holds of an observation exactly when that observation equals the one computed on the compiled framework. The support-boundedness hypothesis is necessary: the observation deliberately reads attacks at support positions outside the carrier, exactly where oracle agreement says nothing, and a mechanized counterexample refutes the hypothesis-free statement. Status preservation (Theorem 6.5) is therefore not the grounded instance of this theorem and stands as proved, with no support hypothesis; a separate equivalence connects the two under the support bound (srcStatus_iff_srcObservation). Appendix I Proofs for the metatheory This appendix proves the results of Section 6 and of the appendix sections that extend it, grouped by pipeline stage. Each proof follows the structure of its Lean counterpart, whose status Appendix A records; the artifact’s name map lists the declaration behind every displayed object. Three arguments are on paper only: the pipeline cost bound (Proposition 6.2), the NP-completeness bookkeeping behind Theorem 6.18, and the subargument-closure, strict-closure, and indirect-consistency clauses of Theorem 6.6. The admission properties of Appendix A cite their declarations in their statements and need no separate proof. Throughout, we abbreviate Σ;Π;Γ;R⊢w:(p)⊳O ; ; ;R w: supports(p) O to ⊢w:p⊳O w:p O when the contexts are fixed, and we write G for the grounded extension of the framework under discussion. I.1 Checking Proof of Theorem 6.1 (decidability, G1).The support checker is defined by structural recursion on w and mirrors Figure 6. At a leaf it looks up Γ(l) (l). At an instance it looks up r, instantiates the premise and conclusion patterns under θ (which fails exactly when a parameter is unbound; terms are ground, so no capture arises), recurses on the premise and discharge subterms, and decides the remaining side conditions: the domain of θ, the premise count, the identities pi≡Piθp_i≡ P_iθ and pq≡Aqθp_q≡ A_qθ, the partition qj=D⊎H\q_j\=D H, and the assurance. Each test is finite; ≡ is decidable (Section 3.2); and the assurance test on a certified instance is one call to β check_β, total by law B1. The checker therefore terminates, and it is sound and complete for the judgment: soundness by induction on w, reading each passed test as the matching premise of Rule; completeness by induction on the derivation, since each premise forces the matching test to pass and the induction hypotheses force each recursive call to return the derived conclusion and obligations. The attack checker runs the support checker on the attacker, walks the finite position π in the target, and scans the finite contrary and exception tables. The contrary test matches a declared pattern pair against two ground atoms by first-order matching, which is deterministic. Adequacy for Figure 9 is a case analysis on the attack kind, using Proposition 6.1 to identify the attacker’s checked conclusion with the derivation’s. Program checking adds finitely many bounded scans over these two checkers: duplicates, O=∅O= , endpoint declaration, and attack completeness. ∎ Proof of Proposition 6.1 (conclusion uniqueness and support adequacy).Uniqueness is by induction on the first derivation with inversion of the second. At a leaf both read Γ(l) (l). At an instance both resolve the same rule from the identifier, and the conclusion is CθCθ for the instance’s own explicit θ; instantiation is a function, so the conclusions agree without consulting the subterms. The obligation sets agree because O is a function of the subterms’ obligation sets, equal by induction, and of r and H. Hence wcw supportsc iff concl(w)≡c.concl(w)≡ c.formal for the unique concl(w)concl(w): one run of the checker and one comparison of normal forms. The relation respects ≡ because ≡ is transitive. ∎ Proof of Theorem 6.2 (dependency accountability, G2).Leaves. leaves(w)leaves(w) is a leaf’s own name, or the union over the premise and discharge subterms of an instance. Every leaf of a checked term is declared, by induction on the derivation: at a leaf the Leaf premise is the witness; at an instance the leaf lies in a subterm with its own derivation. Certificates. certDeps(w)certDeps(w) collects, over the certified occurrences u of w, the slot set that u’s backend reports for its certificate, resolving a slot i below the premise count n to premise i and a slot i≥ni≥ n to theory entry i−ni-n of the digest-resolved theory. A dependency is in certDeps(w)certDeps(w) iff some certified occurrence reports it, and every certified occurrence of a checked term is itself checked, so each report comes from an accepted certificate. Each entry is genuine: a premise entry names the premise subterm at its position, up to ≡, and a theory entry is in range of the resolved theory by the validity clause of law B4. The coverage and accounting clauses of law B4, discharged by each registered backend, say that replay reads nothing outside the report and that the conclusion follows from the reported entries alone. Because a digest resolves only to theory data for one fixed checker, coverage also holds across digests. ∎ I.2 Compilation and claim statuses Proof of Theorem 6.3 (compilation soundness, G3).Every node w∈A(P)w∈ A(P) carries ⊢w:concl(w)⊳∅ w:concl(w) by Accept. For the edges, the attacked occurrence is a function of the attack: a rebut names its whole target, and an undercut or undermine names the subterm at its recorded position. By Definition 4.1, v↝wv w iff some declared attack has source v and its occurrence is contained in w; Accept types every declared attack, so no untyped attack contributes an edge, and containment of the occurrence is the only way w becomes a target. The direct edge from each attack’s source to its target is present, since a target contains its own attacked occurrence. ∎ Proof of Theorem 6.4 (determinism and termination).Let n=||n= , S0=∅S_0= , and Sk+1=ℱF(Sk)S_k+1=F_F(S_k). The characteristic function is monotone, since a defender in S is a defender in any T⊇ST S, so the chain ascends. If Sk+1⊈SkS_k+1 S_k then |∖Sk+1|<|∖Sk| S_k+1 < S_k , so at most n rounds are strict, and once a round is stable all later rounds are, by monotonicity. Hence Sn=ℱF(Sn)S_n=F_F(S_n). It is the least fixpoint, since every fixpoint contains each SkS_k by induction on k. Equivalently, SnS_n is the least predicate I closed under the defence rule of Definition 6.1 read over F’s own edges: Sk⊆IS_k I by induction on k, and I⊆SnI S_n by induction on the derivation, because SnS_n is a fixpoint. The labelling and the cascade of Definition 4.3 are total functions of SnS_n, so evaluation is deterministic. ∎ Proof of Theorem 6.5 (status preservation).Index the declared arguments positionally; A(P)A(P) is duplicate free, so node i of (P)AF(P) is the i-th declared term. The compiled attack relation is decided by a structural scan for the attacked occurrence inside the target. The scan agrees with positional containment because checked terms have duplicate-free discharge keys (Figure 6), so it decides the edge relation of Definition 4.1 exactly on in-range indices and is false off range. The direct judgment (Definition 6.1) and the same judgment read over the compiled edges are least predicates closed under the same two rules and differ only in the edge relation they read; the decider translates each edge, so the two coincide by mutual induction on derivations. On the compiled framework, directly in is membership in G and directly out is being attacked by G (Theorem 6.4), so an argument is labelled in iff it is directly in, out iff directly out and not directly in, and undec otherwise. The four cases of Definition 6.1 are mutually exclusive, each lower case carrying the negation of the higher ones, and the cascade of Definition 4.3 derives exactly one of them: a successful scan of the support set yields the existential witness and a failed scan the universal negation. A functional relation that holds at the computed value is that value: the direct status equals the compiled status. ∎ Proof of Theorem 6.6 (rationality postulates, G6).Write J for the set of conclusions of members of G. Closure under declared subarguments. Let s be a declared argument and a subterm of w∈w∈ G. Positions compose, so every occurrence contained in s is contained in w, and every attacker of s attacks w (Definition 4.1). G defends w, hence defends s, and s∈s∈ G by the fixpoint property. Closure under declared strict steps. Let w=r⟨θ;w1,…,wn;∅;∅;α⟩w=r θ;w_1,…,w_n; ; ;α be a declared strict instance with each wiw_i declared and in G. No rule of Figure 9 targets the root of w: rebuttal and undercutting need a defeasible rule, and undermining needs a leaf. Every attack on w therefore targets an occurrence inside some wiw_i and so attacks wiw_i; G defends each wiw_i, hence w, and w∈w∈ G. This is closure for declared instances; the calculus never manufactures an undeclared one. Conflict-freedom. No two members of G attack each other, a=ba=b allowed. By induction on the round: if a,b∈Sk+1a,b∈ S_k+1 and a↝ba b, defence of b yields c∈Skc∈ S_k attacking a, and defence of a yields d∈Skd∈ S_k attacking c, contradicting the hypothesis for SkS_k. Direct consistency. Suppose contrary claims p and q are both justified. Then some ws,wt∈w_s,w_t∈ G have concl(ws)≡pconcl(w_s)≡ p and concl(wt)≡qconcl(w_t)≡ q, and since contrary matching respects ≡ their conclusions form an instantiated contrary pair. The target wtw_t is attackable at its root: a leaf can be undermined, and if the root rule were strict its conclusion pattern would be strict-reachable and would share a ground instance, up to ≡, with a contrary side, which the conservative overlap check reports and Definition 4.4 forbids; so the root is defeasible and can be rebutted. Attack completeness (Accept) then supplies a declared attack from wsw_s onto an occurrence of wtw_t, so ws↝wtw_s w_t, contradicting conflict-freedom. Hence J is contrary free and no two contrary claims are both justified. Indirect consistency. Let Cl(J)Cl(J) close J under the ground instances of Π ’s strict rules. Every atom of Cl(J)∖JCl(J) J instantiates a strict-reachable pattern, so by Definition 4.4 it is a side of no instantiated contrary pair. A contrary pair in Cl(J)Cl(J) therefore lies in J, which is contrary free. Direct and indirect consistency thus coincide, in the sense of Caminada and Amgoud (2007). ∎ Proof of Theorem 6.7 (quarantine non-promotion).Let G be the declared framework and F the checked one. Both are indexed by the declared argument list: F’s carrier is the retained indices, and F’s attacks are those declared attacks whose endpoints survive, aligned by declared identity rather than by term equality, so F’s edges are a subset of G’s. Let the seed be the removed arguments together with the retained arguments that lost an incoming edge, and let B be its forward closure along G’s edges, computed by the bounded iteration of Theorem 6.4. Outside B the two frameworks agree: an argument y∉By∉ B is retained and lost no incoming edge, so its attackers in F and in G coincide. Locality. If a∉Ba∉ B is directly in for F then it is directly in for G, and if b∉Bb∉ B is directly out for F then it is directly out for G, by mutual induction on the derivation. For a: a G-attacker b of a is retained, since a removed attacker would seed B and closure would put a in B; so b is an F-attacker, b∉Bb∉ B by closure, and the induction hypothesis transfers its out-derivation. For b: its F-defeater c is a G-defeater by edge agreement at b, and c∉Bc∉ B by closure. Grounded labelling reads only transitive attackers, which is why forward closure suffices. Conclusion. The checker publishes justified for c only when F labels some w∈suppF(c)w _F(c) in and no member of suppF(c)supp_F(c) lies in B (Section 4). By locality w is in for G, and suppF(c)⊆suppG(c)supp_F(c) _G(c) because reinstating removed material only adds support; so c is justified in G. The converse fails because the other three statuses read universal or emptiness conditions over a support set that quarantine may have shrunk. ∎ I.3 The image of compilation Proof of Theorem F.1 (image necessity).The compiled framework of every accepted program satisfies the invariant. Edges join positions of declared complete arguments, which carry conclusions. For conflict completeness, an accepted program’s policy is strict-chain well formed, so every contrary target is attackable at its root (as in Theorem 6.6), and attack completeness turns each contrary-matching pair into a declared attack and hence a compiled edge. Both clauses are stated in terms of conclusions and edges, which an isomorphism preserves, so the invariant transports; composing along the realization’s isomorphism gives the claim. Sortedness of node conclusions follows from the coverage hypothesis and the substitution lemma of Section 3.1. ∎ Proof of Proposition F.1 (non-sufficiency).Under a policy with no contrary pair and no exception, the one-node self-edge framework satisfies the invariant, conflict completeness being vacuous. But every attack rule demands conflict data, so no attack types, every compiled framework is edgeless, and an isomorphism would carry the self-edge onto a compiled edge. The context is inhabited: the checker accepts the empty program under it, and a nonempty accepted program realizes its own framework up to a non-identity renaming. ∎ I.4 Semantics-parametric observation Proof of Theorem 6.8 (the printed status is the grounded instance).On a duplicate-free carrier exactly one carrier subset is the least complete extension, namely G, so the grounded enumeration is a one-element list. Unfolding Definition 6.3 at a singleton: the gap arm is the emptiness test; the no-extension arm is impossible; “every extension contains a support member” is “some support argument is in”; “every extension attacks every support member” is “every support argument is out”; and the residual arm is contested on both sides. On a singleton enumeration the skeptical and credulous quantifiers coincide. ∎ Proof of Proposition H.1 (gap alone is semantics-independent).The gap arm is the first guard and reads only the support set, and every other arm lies past it. For the separations, take the two-cycle 0↔10 1 with both nodes supporting c: its grounded extension is ∅ and its preferred extensions are 0\0\ and 1\1\, so grounded observes contested where preferred observes justified. Adding a node 22, attacked by both and alone supporting c, yields contested against defeated. The ten pairwise separations among the five instances are one mechanized statement. ∎ Proof of Proposition H.2 (stable nonexistence).No subset of the three-cycle is conflict free and attacks every outside node, so its stable enumeration is empty, while the other four semantics enumerate at least one extension there; a fourth node attacking all three restores the stable extension 3\3\. For a supported claim the gap guard passes and the empty-enumeration guard fires, so the observation is the no-extension report. Preferred extensions exist for every finite framework: ∅ is admissible, and an admissible set of maximum size is maximal. ∎ Proof of Theorem H.1 (source-level observation transport).Each of the five specifications reads the attack relation only between carrier members, so it is attack-extensional; conflict-freedom must be relativized to the carrier for this to hold. Fix an edge oracle that agrees with the declared attacks on declared arguments. Its framework and the compiled one share the carrier and agree on attacks within it, so they have the same extensions; the observation also reads attacks at the claim’s support positions, and the support bound keeps those in the carrier. Existence and uniqueness of the source observation close the equivalence. The oracle hypothesis is strictly weaker than faithfulness, and dropping the support bound is refuted by a counterexample. ∎ I.5 Strict-certificate backends Proof of Theorem 6.9 (isolation and non-factivity).A registry entry exposes an encoding into an abstract formula type, a consequence relation and an acceptance predicate over that type, a Boolean replay, and a slot-index dependency report (Definition 3.1). No operation returns a source proposition, support term, or attack, and a certificate is an opaque payload that replay receives unchanged; so no elimination of a backend formula or proof term into a source judgment is expressible. Non-factivity is refuted positively: no uniform projection sends every certified step to a premise-free consequence of its encoded conclusion, over all canonicalizers, backends, and theories. The identity step p⇒p p is certified against nd@1 by 0 hyp\ 0, yet the all-false valuation refutes p from no premises; the same step is a consequence of its premise by Theorem 6.10. A program carries theory data addressed by digest and nothing else backend-related. An unregistered name, version, or digest makes acceptance false, and a digest resolves only to theory data for the identity’s one fixed checker, so a program selects among registered backends but adds none. ∎ Proof of Theorem 6.10 (strict-certificate soundness, G4).The assurance test replays κ against the goal β(Cθ) encode_β(Cθ) under the encoded premises [β(Piθ)][ encode_β(P_iθ)] followed by the resolved theory T. Law B1 turns the verdict into acceptance, and law B3 then gives T;[β(Piθ)]⊧β(Cθ)T;[ encode_β(P_iθ)] _β encode_β(Cθ). A trusted instance has no certificate, so the hypothesis of law B3 is unavailable. It remains to discharge that law for each registered backend. nd@1. Consequence is propositional entailment. Replay decodes κ to a term e and type-checks it by the structural recursion of Figure 8, which agrees with the typing relation. Soundness is induction on Δ⊢e:ϕ e:φ for a valuation v satisfying Δ : Hyp reads a satisfied context formula, Abs extends the satisfied context, App is modus ponens, and Abort has an unsatisfiable premise. The relevance form restricts the hypothesis to the free indices of e, which is the accounting clause of law B4. ra@1. A certificate names two premise slots and carries a witness fraction in lowest terms. Replay checks, over exact integers, that the cited cells carry the goal’s numerals, that the full value is nonzero, that the recomputed relative drop equals the witness, that the witness equals the claimed drop, and that the claimed drop meets the threshold. The consequence omits the witness; it cancels by multiplying the claimed-drop identity through by the witness denominator, positive by the grammar. ord@1. A certificate names two premise slots; both numerals appear in the goal, so replay decides the order on them and checks that the cited cells carry them. The decided order is the consequence. Strict and non-strict order over transposed operands exclude each other by arithmetic, which is why the strict and non-strict order predicates declare no contrary pair. insp@1. A certificate selects one inventory premise, or two for a planned-versus-shipped comparison. Replay checks that each selected premise contains exactly one inventory for the source named in the goal, then decides the goal’s membership, absence, or uniqueness condition. For a comparison it checks presence in the plan inventory and absence in the implementation inventory. These conditions are the backend consequence relation. Soundness is relative to the declared inventories; it does not establish that an inventory exhaustively describes the referenced source bytes. ∎ Proof of Theorem 6.11 (backend replacement, G5).Let f be an injective map on certificate payloads such that one backend accepts a strict instance with payload α iff the other accepts it with fαfα; by law B1 acceptance is a function of the source, so this is what “accept the same strict instances” means. Write f⋅wf· w for w with f applied at every assurance and everything else fixed. Typing transports. By induction on the derivation, ⊢w:C⊳O w:C O implies ⊢f⋅w:C⊳O f· w:C O with the same C and O, because only the assurance premise of Rule reads the payload. Attack typing transports because positional lookup commutes with f⋅f· and no other premise of Figure 9 reads a certificate. Since f⋅f· is injective on terms, the relabelled program is duplicate free and is a checked program over the second backend. Frameworks coincide. Nodes are list positions and f⋅f· maps the argument list pointwise, so the carriers are equal. The edge test between two positions compares attack sources for equality and scans the target for the attacked occurrence; both are invariant under an injective relabelling. Hence (P)=(f⋅P)AF(P)=AF(f· P), conclusions correspond index for index, and every claim has the same status. Injectivity is load bearing: collapsing distinct payloads to one marker can identify subterms and add closure edges. ∎ Proof of Theorem 6.12 (heterogeneous backend compositionality).Fix a certified occurrence o of w. Strict soundness lifts through the derivation: at o’s node the derivation binds a registered backend and a resolved theory and yields the rule, the instantiated premises and conclusion, and the occurrence-local consequence. The node is itself checked, and inverting its assurance premise is acceptance by its own checker. The two inversions name the same rule, premises, and conclusion because all three are values of the same lookups. The backend is bound existentially inside each occurrence, so conjoining two occurrences relates no formula types, theories, or consequence relations. The dependency union is the collection identity of Theorem 6.2 applied per occurrence. For the firewall, Rule reads a subterm only through its conclusion, its obligations, and, for a discharge, its question key; so replacing a subterm by one with the same conclusion and obligations preserves the parent’s typing. A witness performs such a swap under an nd@1 parent and leaves a term that uses two backends. ∎ I.6 Contextual representation independence Proof of Theorem E.1 (contextual representation independence).The observation is the hygiene guard, then the checker on the linked program, then the status readout; each stage is blind to the relabelling. The guard reads identifiers, signatures, policies, imports, and exports, none of which f changes. Since C is fixed by f, linking commutes with relabelling: the merged lists of (C,f⋅F)(C,f· F) are the f-images of those of (C,F)(C,F), and the cross-boundary attacks the link inserts depend only on conclusions. Acceptance transports along f as in Theorem 6.11, with well-sortedness and attack completeness reading conclusions only. The compiled structured framework reads conclusions and positional attacks and never an assurance, so the two linked programs compile to the same framework and export the same statuses. The acceptance-profile form is the case f=idf=id, and the composed form instantiates the congruence at the composed context, whose admissibility is assembled from its halves under explicit cross-side coverage hypotheses. ∎ Proof of Theorem E.2 (contextual congruence at every semantics).Both observations factor as one generic observation composed with a projection of the compiled framework: the grounded status, or the claim observation of Definition 6.3 at the chosen semantics. The proof of Theorem E.1 concludes an equality of compiled frameworks and never inspects the projection, so it holds for every projection at once, and the grounded instance is definitional. For the separations: on a linked three-cycle, stable semantics reports no extension where grounded reports contested; and two fragments that differ only in their exported atom, each with unattacked leaf support under a policy with no conflict, are grounded-equivalent in every context yet separated by an adequate singleton-selector semantics at one accepted context. ∎ Proof of Theorem E.3 (typed hole substitution).Template typing factors the side conditions of Rule so that a named hole receives its demanded answer from the hole signature. Erasing the unanswered holes moves each question key into H, so the erased term is a source term and its derivation follows by the same induction, with mandatory questions becoming obligations. Substituting a typed filling closes each discharge condition up to ≡ and returns the same root conclusion and residual obligations. Substitution may identify templates, so the linker deduplicates the instantiated lists and re-imposes attack coverage after substitution. Closed embeddings recover the original observations definitionally, and the congruences pass through because relabelling commutes with substitution. The context’s fillings become part of the substituted fragment, so a relabelling must fix their certificates too; a witness fixes a context’s frame while a certified filling moves. ∎ Proof of Theorem E.4 (relational parametricity).Lift R structurally through terms, attacks, and fragments and re-run Theorem E.1 with the function replaced by the relation. Support and attack typing transport along R by acceptance transport, and saturation commutes because conclusions are preserved. Partial bijectivity is consumed exactly where the calculus compares terms: deduplication in the merge, source comparison in the coverage decider, and the checker’s duplicate-freedom premise. The two linked programs then compile to equal frameworks, after which the relation is erased and every projection agrees. The graph of f recovers Theorem E.1 definitionally. Partial bijectivity is necessary. Dropping it refutes coverage transport; and a relation that collapses two payloads merges two wrappers of one conclusion under deduplication, so an undercut on one wrapper reaches the merged node and an exported claim moves from justified to defeated. Finitely much related material is realized by a total injection that fixes the context, built by composing one swap per constraint, while an arbitrary such relation need not extend to a total injection. ∎ I.7 Source updates and status dynamics Proof of Theorem 6.13 (acceptance preservation).Each constructor edits one raw carrier and reruns admission and the checker, so preservation is a matter of discharging both stages’ premises on the edited state. For add-leaf, freshness keeps the duplicate scans clean and the admitted key keeps the new row out of the prune, so the retained arguments and attacks are unchanged and every derivation transports by monotonicity in Γ . For tighten, the new prune restricts the old one, retained-leaf agreement keeps the surviving environments equal, and the coverage hypothesis re-closes attack completeness. For add-attack, the new attack resolves, types, and has retained endpoints, so it extends an already typed list. For add-instance, freshness, well-sortedness, complete support, and extended attack completeness are the checker’s remaining premises. In each case completeness of the checker (Theorem 6.1) accepts the edited state. ∎ Table 15: The four grounded core transition matrices of Theorem 6.14. Rows are source statuses and columns target statuses: justified (J), defeated (D), contested (C), gap (G). A ✓ cell carries a mechanized witness, an accepted source and target program with a successful update between them; a mechanized theorem excludes each blank cell under the constructor’s stated premises. Lean generates the matrices from those witnesses and a committed golden pins them, so the table cannot drift from the proofs. add-leaf tighten add-attack add-instance from J D C G J D C G J D C G J D C G J ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ D ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ C ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ G ✓ ✓ ✓ ✓ ✓ ✓ ✓ Proof of Theorem 6.14 (grounded transition matrices) and Theorem 6.15 (gap boundary).Each reachable cell is a fixture: an accepted source, an accepted target, and a successful update between them, with both observations evaluated by reduction. The matrices and their counts are computed from the fixtures and pinned by a committed golden. Four lemmas exclude the rest. A fresh admitted leaf changes no retained argument or attack, so the framework and every status are fixed. Non-instance updates add no argument, so empty support stays empty; additive updates remove none, so nonempty support stays nonempty. These read only the support set and hence hold for every extension semantics, which is Theorem 6.15. Finally, a fresh instance is a sink of the old framework, since no old attack names it, so old labels persist: an in argument stays in and an undec argument never becomes out, which excludes the three cells from justified or contested into defeated. This last lemma is what corrected the predicted count of 13 reachable add-instance cells to 10. ∎ Proof of Corollary 6.16 (matrix non-promotion) and the public layer.On a clean source the seed of Theorem 6.7 is empty, so the blocked set is empty and the public report is the core report. An additive update removes nothing, so its target is clean and the additive public transitions are the core ones, never reaching evidence-blocked. Cleanliness is necessary: an accepted non-clean source exists on which one added attack grows the blocked set and moves a public justified to evidence-blocked while the core status reads defeated. For the corollary, a public justified target under tighten forces a core justified source, and on a clean source the checked framework is the declared one. The two AGM probes are fixtures: an add-instance whose only new support is defeated on arrival refutes success, and an add-attack that removes a justified claim refutes inclusion. ∎ I.8 The verified surface boundary Proof of Theorem G.1 (elaboration preservation).Elaboration runs a fixed sequence of passes: validation, value and prose interpolation, comparison expansion, argument reconstruction with substitution inference and certificate lowering, attack resolution, unit assembly, and admission. A surface derivation carries, for each pass, that pass’s independent relation, and each pass has a completeness lemma that drives it to success on the derivation’s own output. Core acceptance does not come from rerunning elaboration: the derivation’s declarative core obligations feed the core checker’s completeness theorem directly. The four projections are output-component equalities the derivation carries. ∎ Proof of Theorem G.2 (supported-fragment reflection).Invert a successful elaboration pass by pass: each adjacent pair of passes has a boundary lemma recovering the earlier pass’s output, and each pass’s soundness lemma yields its relation. The supported fragment supplies the structural facts elaboration never checks, and the successful core check supplies the core obligations. Both hypotheses are necessary: inputs exist that elaborate while unsupported, and supported inputs exist that elaborate while the core checker rejects the result. Determinism of the judgment pins the derivation’s output to the elaborated one. ∎ Proof of Theorem G.3 (surface observation coherence).The direct framework has the retained argument positions as carrier and the resolved attacks as edges, computed without the compiler. For an accepted derivation it equals the compiled framework exactly, and the direct and core claim ledgers agree, a missing identifier staying missing on both sides. The direct claim’s support lies in the carrier, so Theorem H.1 transports the observation for every attack-extensional semantics, and the five corollaries discharge that hypothesis per instance. Carrier-locality is necessary. ∎ I.9 Cross-context comparison Proof of Theorem 6.19 (modal normality and comparison adequacy).Satisfaction of a box quantifies over accepted edges, and acceptance does not depend on the formula, so K and necessitation follow by unfolding and duality is classical negation over the same edge set. T, D, B, and 5 fail on a two-world frame with one accepted edge and a valuation separating the worlds, and 4 fails on a three-world chain whose composite edge is not accepted. These countermodels inhabit the generic frame type with arbitrary valuations, rather than the checked-program instance with computed claim statuses. The executable comparison guards translation, candidates, and acceptance in that order and returns either a reason or the statuses of the accepted candidates; when its candidate list and acceptance test present the bridge, a status is output iff the diamond holds, and an incomparable query has no accepted witness. The one-context, no-bridge instance is local evaluation by definition, and Theorem 6.5 at each world makes the direct and compiled valuations agree, so they satisfy the same formulas. ∎ Proof of Theorem 6.20 (exact support transport).By induction on the derivation. The leaf case is the bridge’s leaf clause. In the instance case the rule clause supplies the translated rule at the same identifier; instantiation commutes with translation, and ≡ survives it because normalization touches literals while translation touches names; question keys, discharge keys, and holes cross verbatim, so O is unchanged; and the certificate clause handles the assurance. Completeness and claim-level support follow, and the certified occurrences of the transported term replay against the target registry by Theorem 6.12. Definedness of the term’s translation is a genuine hypothesis: θ may bind an unused parameter outside the bridge’s vocabulary, so a translatable conclusion does not imply a translatable term. Symbol maps compose in Kleisli fashion with both unit laws, every structural lift satisfies a composition law, and stepwise transport along a path equals transport along the folded bridge. A direct bridge commutes with a path iff their symbol and leaf maps agree, because support terms expose both maps; two negative triangles, one disagreeing only on a leaf renaming and one only on a predicate, show each component necessary. ∎ Proof of Theorem 6.21 (conditional status preservation).Grounded status is invariant under a total attack bisimulation of finite frameworks: directly in and directly out transfer in both directions by induction on derivations, so labels correspond, and a support correspondence then carries all four statuses. Nodes are positions, so relate i to j when the j-th target argument is the transport of the i-th source argument; then (i) is left-totality, (i) right-totality, and (i) the forth and back conditions. The support correspondence for a translatable claim follows: forward by Theorem 6.20 and conclusion uniqueness, backward by (i) and reflection of ≡ along the injective translation, which is where injectivity is used; a non-injective bridge must supply the correspondence itself. The statuses therefore agree, also at the source observation through Theorem 6.5 at both worlds. Each hypothesis is load bearing: the witness of Theorem 6.20 satisfies (i) and the forth half of (i), yet its target holds an argument that is no transport, (i) fails, and the status flips. The four clauses are bounded quantifications over indices, so a Boolean checker decides them. A declared-attack correspondence yields (i) when the leaf renaming is injective, since a collapsing renaming can merge subterms. The hypotheses compose along paths, and statuses are values, so pathwise preservation is transitivity of equality. When every accepted successor is so related and one exists, the boxed and diamonded translations are each equivalent to the local status atom. ∎ I.10 Cost Proof of Theorem 6.17 (grounded query bounds).The instrumented evaluator counts one query per attack-relation evaluation, in the reference evaluator’s short-circuit order, and its value projection equals the reference evaluator. Each of the n rounds tests defence for at most n arguments; each test scans at most n attackers, each costing one outer query and at most n inner queries; this gives n3(1+n)n^3(1+n). Each round issues at least one query per argument per scan, which gives n2n^2. A status query adds one support scan and one defeat scan over at most n members, at most 2n22n^2. The quartic family places k−1k-1 neutral nodes and a defender before k attacked nodes and k targets, with edges from the defender to each attacked node and from each attacked node to each target; it is realizable in the fixed context, and its repeated defence scans cost at least k4k^4 queries for k≥2k≥ 2. The two-node all-attacks framework costs exactly four queries, so no instance-wise cubic floor holds. ∎ Proof of Theorem 6.18 (hardness on the realizable class).Gadget. For each variable, two literal roots that undermine each other; for each clause, an instance undermined at each literal position by the opposing literal root; and one query argument undermined by every clause root. All leaves come from one closed vocabulary with an injective spelling table, under one frozen signature, policy, and registry. Realizability and size. The checker accepts every output: the lemmas cover duplicate-freedom, sortedness, support for literal and clause arguments, typed attacks, and attack completeness, the last using injectivity of the spelling, without which two variables with colliding payloads would demand an undeclared attack. With the compilation isomorphism this is realizability in the fixed context; the node count and byte bound hold by construction. The one-node self-edge framework is not realizable there, since no policy row licenses its edge. Correctness. From a satisfying assignment, the set of the query and the true literal roots is complete and contains the query. From a complete extension containing the query, every clause root is attacked, so each clause has a literal root in the extension, and the mutual literal attacks keep the read-off assignment consistent. On paper. Constructing the reduction takes polynomial time: the construction enumerates literal and clause nodes and their pairs, decides each gadget edge by bounded scans, and writes the encoded carrier. The node count and byte bound limit these operations polynomially in the encoded formula’s length. Membership of credulous complete acceptance in NP is guess-and-check: an extension has polynomial size, and completeness and query membership are polynomial-time checkable. With the polynomial-size reduction this gives NP-completeness on the realizable class under standard encodings. ∎ Proof of Proposition 6.2 (polynomial core checking and evaluation).The input contains explicit support trees and substitutions. At each support node, the checker scans finite tables and lists, instantiates policy patterns, checks normalized identities, and combines obligation lists. A pattern instantiation copies only substitution terms already present in the input, so its expanded size is polynomial in N. Duplicate and membership checks may be quadratic in their list lengths; the number and lengths of these lists are bounded by the explicit input and its instantiated patterns. The structural recursion therefore performs polynomial work, with backend encoding and replay charged as opaque calls. Attack checking adds bounded position walks and pattern matching. Whole-program acceptance checks argument pairs for conflict coverage. Compilation examines argument pairs, scanning declared attacks and testing structural containment to decide each edge. These operations are polynomial in N. Grounded evaluation makes polynomially many edge queries by Theorem 6.17; either recomputing an edge or looking it up in a materialized relation preserves the bound. Aggregation scans complete support sets and labels, so the stated core pipeline is polynomial. This argument gives no bound in compact surface-source size or on backend internals. The timings in Section B.5 measure overhead on small inputs and do not test this bound. ∎ Appendix J Case-study and worked-example listings This appendix collects the longer listings behind the compact case-study presentation in Appendix D and the certified-comparison worked example of Section 7. The accompanying supplemental artifact contains the complete runnable programs, versioned policies, replay commands, and golden reports; the listings below retain the paper-facing elisions noted in their captions. To read the programs, a claim names the proposition whose support we want to assess, a leaf declares evidence, and an arg applies a policy rule to construct support or a challenge. The clause discharge q with e supplies evidence for a named critical question; open q records an unanswered optional question. Attack declarations name both the challenging argument and the part of the target argument it disputes. A status query asks what support survives these attacks under the declared policy. J.1 Certified comparison under attack This example asks what a certified numerical comparison establishes about an empirical claim. We separate the arithmetic check from the inference that the reported scores demonstrate a better system. The comparison block generates both steps; its binding premise declares that the scores are comparable. The settings audit challenges that premise, so the attack targets the empirical bridge. Lara can therefore preserve the certified inequality while reporting that the headline claim’s support is defeated. The example demonstrates how checked arithmetic and revisable empirical reasoning coexist in one program without giving the empirical conclusion the certificate’s guarantee. ⬇ 1 artifact ord_setting_demo at sha256:5454545454545454 2 policy ord-setting-v1 3 use backends [ord@1] 4 # the headline claim; the two measured cells below are not disputed 5 claim c1 6 formal = better(sys_new, sys_base, accuracy, imagenet_val) 7 leaf e1 : reports(exp1, score_cell(sys_base, accuracy, imagenet_val, 0.71)) 8 leaf e2 : reports(exp1, score_cell(sys_new, accuracy, imagenet_val, 0.74)) 9 # the binding: the only place the artifact asserts the two cells are comparable 10 leaf e3 : comparison_setup(sys_new, sys_base, accuracy, imagenet_val, 0.74, 0.71) 11 # the audit’s evidence 12 leaf e4 : audits_settings(aud1, sys_new, sys_base, accuracy, imagenet_val) 13 # one block generates the strict re-check a1, the bridge a2, and the sub-claim c2 14 comparison : better(sys_new, sys_base) on accuracy @ imagenet_val 15 relation = strictly-better 16 recheck = a1 17 bridge = a2 18 result = e2 19 baseline = e1 20 binding = e3 21 claims c2 22 nl = "The reported baseline accuracy cell e1 is strictly below the reported system accuracy cell e2" 23 binding = author = alice, audit-status = reviewed 24 supports c1 25 # the critic: x1’s conclusion is the declared contrary of the binding leaf 26 arg x1 : challenges(e3) by setting_audit(sys_new, sys_base, accuracy, imagenet_val, 0.74, 0.71, aud1) 27 # a2.binding.leaf names the disputed premise; a2.1.leaf is the same position spelled positionally 28 undermine x1 a2.binding.leaf 29 status c1 # defeated: every complete argument for c1 is out 30 status c2 # justified: a1 is in, untouched by the attack Listing J.1: The certified comparison under attack, from the worked-example suite, authored in an earlier revision of the surface of Section 3. One comparison block generates the strict re-check a1, the defeasible bridge a2, and the arithmetic sub-claim c2; the author names only the system pair, measurand, dataset, relation, and evidence leaves. Claim prose and leaf metadata are elided except inside the block, whose sub-claim prose and attestation the block itself must declare. The audit’s conclusion is the declared contrary of the binding leaf e3, so x1 undermines the bridge a2 at its binding premise; the label binding resolves to the same position as a2.1.leaf and never reaches the core. The grounded labelling puts a1 and x1 in and a2 out: the headline claim c1 is defeated while the certified inequality c2 stays justified. J.2 Rebuttal replay Read the rounds as additions to the same dispute under a fixed standard. The first round records what has support; the review identifies the premises, conclusions, and inferences being challenged; the rebuttal adds support and defenses. The three final queries distinguish a restored benchmark claim, a conceded measurement claim, and a newly supported ablation claim. Lara computes these different outcomes from the declared changes, so a reader can check why each claim’s status changed or persisted. ⬇ 1 # ROUND 0 -- submission: the paper alone 2 artifact adaptive-pruning at sha256:de3685165a53 3 policy rebuttal-v1 4 use backends [nd@1] 5 claim c_bench 6 formal = performs(apt, dense_baseline, openllm_avg) 7 arg a_bench : supports(c_bench) by benchmark_evaluation(apt, dense_baseline, openllm_avg, e02) 8 discharge protocol_fixed with pb2 9 discharge benchmark_valid with pb3 10 open environment_match as environment_match 11 # claim c_measure + arg a_meas: measurement, justified (elided) 12 claim c_kurt 13 formal = contributes(kurtosis_salience, apt_llama2_7b, openllm_avg) 14 leaf pk1 : reports(e03, ablation_effect(kurtosis_salience, apt_llama2_7b, openllm_avg, positive)) 15 leaf pk2 : isolated(kurtosis_salience, e03) 16 leaf pk3 : matched_protocol(e03) 17 # no arg for c_kurt: variance_reported(e03) is mandatory, so the claim is gap 18 # ROUND 1 -- reviews: paper unchanged, three typed attacks added 19 leaf ru_np : not_fixed_protocol(apt, dense_baseline, e02) 20 arg d_um : challenges(pb2) by leaf(ru_np) 21 undermine d_um a_bench.protocol_fixed.leaf 22 arg d_rebut : supports(c_bench_neg) by null_benchmark(apt, dense_baseline, openllm_avg, e_rep) 23 discharge protocol_fixed with ru_nb2 24 discharge environment_match with ru_nb3 25 rebut d_rebut a_bench 26 rebut a_bench d_rebut 27 leaf ru_ma : measurement_artifact(low_memory_footprint, apt) 28 arg d_meas : challenges(instrument_validity(a_meas)) by leaf(ru_ma) 29 undercut d_meas a_meas.rule 30 # ROUND 2 -- rebuttal: paper + reviews unchanged, author responds 31 leaf rk_var : variance_reported(e03) 32 arg a_kurt : supports(c_kurt) by component_ablation(kurtosis_salience, apt_llama2_7b, openllm_avg, e03) 33 discharge single_variable with pk2 34 discharge protocol_parity with pk3 35 discharge variance_reported with rk_var 36 arg r_um : challenges(ru_np) by leaf(rk_pc) 37 undermine r_um d_um.leaf 38 arg r_rebut : challenges(environment_match(d_rebut)) by leaf(rk_em) 39 undercut r_rebut d_rebut.rule 40 # c_measure not defended (concession) => stays defeated 41 status c_bench 42 status c_measure 43 status c_kurt Listing J.2: The rebuttal exchange as three checked Lara programs over one artifact and one policy. Each comment header marks a program boundary; rounds 1 and 2 repeat the round-0 paper verbatim, elided here, as are claim prose/bindings and leaf metadata. The reviews add one attack of each kind; the rebuttal supplies the missing variance evidence and counter-attacks both benchmark attackers. J.3 Mechanical-reviewer output These comments illustrate two different requests an author may need to address: provide a complete argument, or answer an attack on an existing argument. The first comment reports an empty support set; the second names the defeated support and its attacker. Lara supplies the checked diagnosis, which a fixed template turns into review prose. ⬇ 1 **51 review comments** — 48 gap, 3 defeated. 2 3 ## adaptive-pruning.C04 — gap 4 Claim ‘c04‘: ‘contributes(kurtosis_salience, apt_llama2_7b, openllm_avg)‘ 5 > No argument assembles the unit’s evidence into a checked support for this claim; its complete-support set is empty, so at the ‘corpus-v1‘ evidential bar the claim is unsupported — status **gap**. 6 7 ## fre.C04 — defeated 8 Claim ‘c04‘: ‘contributes(reward_diversity, fre_all, antmaze_total_score)‘ 9 > The claim’s only support ‘a1‘ is labelled ‘out‘: the undercut ‘d1‘ (challenging the ‘variance_reported‘ critical question of ‘a1‘) is unattacked and defeats ‘a1‘ — status **defeated**. Listing J.3: Two of the mechanical reviewer’s 51 rendered comments, verbatim from the renderer output except that each claim’s natural-language statement is elided. The renderer uses the checker’s verdict and located diagnostic; it performs no free-text generation. J.4 Agreement map The final argument of each formal claim identifies its experimental setting. Within P1, both conclusions concern the same setting and the declared rebuttals express an unresolved conflict. Within P2, the settings differ, so the policy does not license the corresponding conflict. Lara makes this distinction explicit in the verdicts: opposing wording alone does not determine whether the encoded claims attack each other. ⬇ 1 # P1 -- genuine disagreement: same atoms => contested 2 claim c_pos 3 formal = better(apt, cofi, accuracy, roberta_mnli_s60) 4 arg pa : supports(c_pos) by controlled_comparison(apt, cofi, accuracy, roberta_mnli_s60, paperA_exp1) 5 claim c_neg 6 formal = not_better(apt, cofi, accuracy, roberta_mnli_s60) 7 arg pb : supports(c_neg) by null_comparison(apt, cofi, accuracy, roberta_mnli_s60, paperB_exp1) 8 rebut pb pa 9 rebut pa pb 10 # P2 -- setting mismatch => no edge 11 claim c_low 12 formal = better(magnitude_pruning, dense_baseline, accuracy, bert_glue_s50) 13 arg pc : supports(c_low) by controlled_comparison(magnitude_pruning, dense_baseline, accuracy, bert_glue_s50, paperC_exp1) 14 claim c_high 15 formal = not_better(magnitude_pruning, dense_baseline, accuracy, llama_openllm_s90) 16 arg pd : supports(c_high) by null_comparison(magnitude_pruning, dense_baseline, accuracy, llama_openllm_s90, paperD_exp1) 17 # D differs, so no contrary instance and no edge 18 status c_pos 19 status c_neg 20 status c_low 21 status c_high Listing J.4: The agreement map as one program. Claim leaves, discharges, and natural-language/binding fields are elided so that the formal conclusions and attack structure remain visible. The single setting-index difference flips the pair from contested to justified. J.5 Philosophical assumptions, objections, and defenses The philosophy program makes two obligations visible: why indispensability warrants belief in abstract objects, and whether a nominalist reconstruction covers the fragment being discussed. The policy requires explicit answers to both. The attacks then locate the disagreements: a challenge to the indispensability premise, a dispute over number identity, and a chain of objection and reply about usefulness and truth. The final undercut restores the fictionalist argument by defeating its attacker. ⬇ 1 artifact philmath_debate at sha256:p1-illustrative-snapshot 2 policy philmath-v1 3 use backends [] 4 5 leaf commitment : ontological_commitment() 6 kind = assumed 7 provenance = ai-executed 8 refs = [] 9 leaf scope : scope_adequate() 10 kind = assumed 11 provenance = ai-executed 12 refs = [] 13 14 arg a_realism : supports(c_realism) by indispensability from [indispensability_premise] 15 discharge commitment with commitment 16 arg a_field : supports(c_field) by nominalization from [field] 17 discharge scope with scope 18 arg a_sets : supports(c_sets) by set_identification from [set_proposal] 19 arg a_structure : supports(c_structure) by structural_explanation from [benacerraf] 20 arg a_fiction : supports(c_fiction) by fictionalist_reading from [conservativity] 21 arg a_objection : supports(c_objection) by truth_objection from [truth_assumption] 22 arg a_reply : supports(c_reply) by leaf(reply) 23 24 undermine a_field a_realism.0.leaf 25 rebut a_structure a_sets 26 rebut a_sets a_structure 27 undercut a_fiction a_realism.rule 28 undercut a_objection a_fiction.rule 29 undercut a_reply a_objection.rule 30 31 status c_realism 32 status c_sets 33 status c_structure 34 status c_fiction Listing J.5: Selected declarations from the philosophy-of-mathematics program (ARA-Labs, 2026a). Claim declarations and most leaves are omitted; all leaves in the full program are assumed or attested. The authored policy makes the commitment and scope questions mandatory. The number-identity pair remains contested; the reply reinstates the fictionalist argument. These are outcomes of the encoded debate. J.6 A certificate that depends on an admitted assumption The source below exposes the assumption used by its certificate. The strict citation rule has that atom as both premise and conclusion, and its backend theory is empty. The certificate (hyp 0) therefore checks reuse of the declared premise. The three policy variants admit, quarantine, or reject leaves with the pair (assumed, ai-executed). Quarantine removes the only premise and its dependent argument, so the surviving claim has status gap. The separate Lean witness proves why a structural bridge cannot preserve that premise in the empty target evidence environment (Section D.5). ⬇ 1 artifact axiom_withdrawal at sha256:axiom-demo 2 policy admitted 3 use backends [nd@1] 4 5 claim c 6 nl = "The parallel postulate is available under this admission policy" 7 formal = parallel_postulate() 8 binding = author = demo_author, audit-status = unreviewed, 9 rationale = "An assumed atom reused as itself, not a geometric consequence." 10 11 leaf p : parallel_postulate() 12 kind = assumed 13 provenance = ai-executed 14 refs = [] 15 16 arg a : supports(c) by citation from [p] 17 assurance = cert(nd@1, sha256:empty, (hyp 0)) 18 19 status c Listing J.6: The admitted source of the axiom-withdrawal demo (ARA-Labs, 2026b), with its introductory comment omitted. The withdrawn and rejected sources select their respective policies; the leaf, argument, and claim declarations are identical. The certificate establishes hypothesis reuse, not a geometric theorem or unconditional truth of the postulate.