Beyond Natural Language: An Agent-Native Language for Autonomous Science

1 Introduction

• Research agents can run automated regression tests on declared hypotheses and support, receiving deterministic checker verdicts instead of prompt-based evaluations.Lara is presented as an epistemic kernel for agents building later research on verified findings.Source: §1 · p. 2
• Declared bridges connect claims across contexts into an auditable network, where later attacks can make an earlier claim no longer justified in every accessible context.A literature-scale knowledge graph is described as a possible downstream application.Source: §1 · p. 2
• Typed attacks let failed experiments or philosophical objections defeat targeted support while distinguishing unsupported claims from claims whose support was defeated.The checker thus treats objections and limitations as explicit parts of the argument.Source: §1 · p. 2
• Lara separates validity of a support term from acceptance of its claim, so later objections can defeat a claim without invalidating a checked comparison.A benchmark inequality can remain arithmetically valid even after confounders undermine the performance claim it was used to support.Source: §1 · p. 2
• A deterministic checker compiles declared claims, evidence, inference steps, obligations, and typed attacks into justified, defeated, contested, or gap statuses.Strict deductions use registered backends; defeasible steps must answer mandatory critical questions, and arguments can defeat or reinstate support.Source: §1 · p. 3
• Case studies span empirical review, philosophical disagreement, and withdrawn axioms; the semantic results are mechanized in Lean 4 across roughly 117,000 lines.The audited public metatheory uses Lean’s three standard axioms; some executable examples additionally trust native evaluation, and three arguments remain on paper.Source: §1 · p. 3

2.1.1 Agent-native research: records that agents read and write

• Agent-native records connect claims and evidence to methods, code, conditions, and investigation history, while Lara makes proposed relationships between records explicit and checkable.ARA can preserve both an improvement and a later experiment where it disappears; Lara lets authors declare how those records relate.Source: §2.1.1 · p. 4

2.1.2 Formal argumentation: reasons and objections

• Defeasible reasoning lets support lose force under an unanswered challenge and regain it when that challenge is defeated; Lara checks declared support and attacks before assigning claim statuses.Statuses distinguish justified, defeated, contested, and gap; they describe the declared case, not measurement accuracy or truth.Source: §2.1.2 · pp. 4–5

2.1.3 Possible worlds: comparing research settings

• Declared bridges specify which worlds to compare and how claims correspond; the checker can ask whether a claim is justified in some or every compared record without changing its original verdict.A researcher remains responsible for choosing an appropriate comparison.Source: §2.1.3 · p. 5, Figure 1 · p. 6

2.2 A running example

• In the running example, run 1 has gap status because its mandatory external-validity question is unanswered; run 2 adds complete support and an undercut, leaving the claim defeated.The undercut challenges the inference’s applicability, not the empirical claim’s truth; adding the off-distribution evidence alone would not produce the transition.Source: §2.2 · p. 6

2.3 Trust architecture

• The checker verifies declared support relative to the signature, policy, registry, and admitted evidence, but not claim truth, evidence accuracy, policy suitability, or prose-to-formal fidelity.Modal answers cover only declared comparisons, not settings unreachable by a bridge.Source: §2.3 · p. 8

3 The claim-support language

• A Lara program declares evidence leaves, policy-rule instances, obligations, and typed attacks, interpreted against a signature, versioned policy, backend registry, and artifact snapshot.Claims pair natural-language sentences with formal targets, but the checker does not establish that the signed binding is faithful.Source: §3 · p. 9, §3.1 · p. 9

3.1 Propositions, leaves, and claims

• Propositions use a fixed, many-sorted vocabulary; leaves record a proposition, kind, provenance, and source references, while claims are supported by positional identity with a formal target.The checker does not infer that a formal atom entails a claim’s prose meaning.Source: §3.1 · p. 9

3.2 Proposition normalization

• Normalization canonicalizes literals and recurses structurally without reordering arguments, making proposition identity decidable, total, and linear in term size.Surface differences are removed before equality is checked.Source: §3.2 · p. 10

3.3 Claim-support policies and obligations

• Versioned policies define strict or defeasible schemes, contrary relations, and exceptions; defeasible instances must account for critical questions, and unanswered mandatory questions block acceptance.Only optional questions may remain open in an accepted program; such holes add no obligation.Source: §3.3 · p. 10, Figure 6 · p. 11

3.4 Strict-certificate backends

• Strict instances require explicit policy trust or an opaque certificate from a registered backend, whose one-way interface checks encoded conclusions against premises and declared theory.The reference backend uses intuitionistic natural deduction; its atomic source encoding exposes propositional consequences, not undeclared domain laws.Source: §3.4 · pp. 10, 12, Figure 8 · p. 12

3.5 Typed positional attacks

• Typed attacks target positions in support terms: rebuttals challenge defeasible conclusions, undercuts target rule occurrences, and undermines target leaves; whole-program checking requires complete conflict coverage.Dead-end tags, confidence scores, and provenance downgrades do not attack on their own.Source: §3.5 · pp. 12–13, Figure 9 · p. 13

4 Compilation and claim-support semantics

• Admission applies policy decisions and duplicate-report checks before evaluation, pruning removed leaves, affected arguments, and unresolved attacks from the checking context.The combined pruning pass uses the reconstructed support graph and emits a canonical audit.Source: §4 · pp. 13–14, Figure 10 · p. 14
• Whole-program acceptance requires complete arguments, licensed attacks, and coverage of required conflicts; accepted programs may still contain defeated arguments.Incomplete terms are excluded from the compiled argument set.Source: §4 · pp. 13–15
• Complete checked terms become framework arguments, and compiled typed attacks become edges to arguments containing the attacked occurrence; grounded labelling assigns in, out, or undec.The grounded characteristic function is monotone, and its least fixpoint is reached in at most |A| iterations.Source: §4 · p. 15
• Grounded evaluation is deterministic and terminating for a fixed framework, but adding an argument can retract justified status and removing an attacker can promote its target.The framework-to-accepted-claims map is nonmonotonic even though the internal transfer operator is monotone.Source: §4 · p. 15
• Claims are gap without complete support, justified with an in-labelled support, contested when support is undecided but none is in, and defeated when every support is out.Gap distinguishes absent support from refutation.Source: §4 · p. 16
• Quarantine can block public reporting when a claim’s declared complete support lies in the affected closure, preventing a conditional diagnostic from appearing as a new justification.Claims outside that closure publish their core status.Source: §4 · p. 16
• A compile-time restriction ensures conflicts are rebuttable at defeasible steps, so strict closure introduces no new conflict and consistency follows by construction.The expressiveness cost is that strict chains may target only uncontested claims; lifting the restriction requires a different consistency argument.Source: §4 · p. 17

5 Cross-context comparison semantics

• The cross-context layer addresses how to compare claims across differing checking contexts while preserving the local calculus.Contexts may differ in vocabulary, policy, or admitted evidence.Source: §5 · p. 17

5.1 Worlds and observations

• An outer model defines contexts, worlds, bridge relations, applicability, and partial query translations; accepted bridge edges determine modal comparison rather than every imaginable setting.In the checked-program instance, worlds are accepted units and contexts fix signature, policy, registry, and checker parameters.Source: §5.1 · p. 17
• Bridge queries ask whether some or every accepted successor justifies a translated claim, and robust justification additionally requires at least one successor.A one-world instance without bridges recovers local semantics.Source: §5.1 · p. 17

5.2 Structural bridges

• Structural bridges preserve exact translated rules, admitted leaves, and certificate acceptance; status preservation additionally requires source and target argument coverage and attack correspondence in both directions.A near match that changes rule assumptions falls outside the contract, and the checker does not decide domain relevance.Source: §5.2 · p. 18

6.1 Checking

• A support term has a unique conclusion and obligation set; program and attack checking terminate, and reported leaf and backend dependencies are accountable.The dependency report equals the term’s leaves, all are declared, and certificate dependencies include every free premise and theory entry used.Source: §6.1 · p. 19

6.2 Compilation and claim statuses

• Compiled reports preserve direct source claim statuses; under strict-chain well-formedness, accepted claims are consistent, and quarantine cannot promote a claim to justified.Evaluation is deterministic and terminating; closure under declared subarguments and strict steps holds without the strict-chain condition.Source: §6.2 · pp. 19–20

6.3 Semantics-parametric observation

• Grounded observation reproduces Lara’s printed status, while other extension semantics can vary reports; only gap is semantics-independent, and stable semantics may yield no extension.For justified status, each extension must contain some supporting argument, though the supporting argument may differ across extensions.Source: §6.3 · pp. 20–21

6.4 Strict-certificate backends

• Strict certificates are isolated from source truth judgments, and accepted certificates establish encoded consequences in their backend logic, excluding trusted-policy instances.Replacing a backend that accepts the same strict instances preserves the compiled framework and every claim status; heterogeneous certificate occurrences retain local consequence and dependency guarantees.Source: §6.4 · pp. 21–22

6.5 The source boundary

• Admission pruning preserves declared argument identities and removes attacks with deleted endpoints, but tightening admission can change retained arguments’ labels.The conservative reporting boundary ensures a published justified claim was already justified with quarantined material reinstated.Source: §6.5 · p. 22

6.6 Source updates and status dynamics

• Of 64 grounded update-kind and status-transition cells, 37 are reachable; add-leaf preserves core status, while add-instance cannot turn justified or contested into defeated.Gap persists under add-leaf, tighten, or add-attack, and successful additive updates cannot create a gap; public transitions also depend on cleanliness, and two tested AGM-style postulates fail. Surface elaboration preserves and reflects checking on the supported syntax, with direct observations agreeing for attack-extensional semantics.Source: §6.6 · p. 23

6.7 Cost

• Grounded evaluation uses between n^2 and n^3(1 + n) attack queries on every finite framework, and credulous complete acceptance is NP-complete even on Lara-realizable frameworks.A realizable family attains at least k^4 queries at size 3k; the 3SAT reduction establishes hardness in one fixed context, while its NP bookkeeping remains on paper.Source: §6.7 · p. 24
• Core support and attack checking, program acceptance, compilation, and grounded status computation use polynomially many syntactic operations and backend calls in input size N.The bound excludes surface elaboration and work inside backends, and does not establish linear time for the list-based checker.Source: §6.7 · p. 24

6.8 Cross-context guarantees

• The modal K axiom, necessitation, and box–diamond duality hold, while executable comparison reports a status exactly when the corresponding diamond holds.Unrestricted-valuation countermodels for T, D, B, 4, and 5 establish neither checked-program counterexamples nor a complete axiomatization; incomparable queries are reported with a reason rather than a status.Source: §6.8 · pp. 24–25
• Exact support transport preserves checked support and its verbatim obligations when translation is defined, with certified occurrences replaying against the target registry.Transport along a composite bridge agrees with stepwise transport; a direct bridge agrees with a path exactly when their symbol and leaf maps are equal.Source: §6.8 · p. 25
• Claim-status preservation requires a structural bridge with injective translation, complete source–target argument coverage, and attack correspondence in both directions.Under these conditions, translated claims retain the same status in all four states; the checker decides the four correspondence clauses, and the conditions compose along bridge paths. Support transport alone does not preserve status.Source: §6.8 · p. 25

7.1 Mechanization

• Thirty-four of thirty-five specification results are fully mechanized in a 144-file, roughly 117,000-line Lean tree; the audited public metatheory is sorry-free and uses only Lean’s three standard axioms.Some private executable examples additionally trust native evaluation.Source: §7.1 · p. 25

7.2 Implementation conformance

• The differential harness agrees with the compiled Lean reference on 673 verdict-bearing and 66 malformed inputs, while finite tests do not prove implementation equivalence.The Haskell checker covers the checking pipeline and four strict backends; tests validate its parser and elaborator.Source: §7.2 · p. 26

7.3 Ablation study: effects of removing checks

• Disabling obligation checks admits 18 incomplete-support programs, removing coverage admits five missing-attack programs, and also disabling attack typing admits 32 further invalid-attack cases.These seeded defects demonstrate detection of intended failures, not their prevalence in research artifacts.Source: §7.3 · p. 26

7.4 Arithmetic and empirical support

• When equal benchmark cells are compared, certified arithmetic permits only a non-strict comparison, while attacking the comparability premise defeats the bridge and headline claim but leaves the inequality justified.The strict arithmetic certificate establishes the numeral inequality, not the empirical meaning of the measurements.Source: §7.4 · p. 26

7.5 Demonstrations beyond empirical claims

• The demonstrations exercise contestation and reinstatement in a philosophical debate without measurements, and source admission and certified-hypothesis reuse when an axiom is withdrawn.A separate executable Lean witness illustrates the structural transport boundary.Source: §7.5 · pp. 26–27

7.6 Limitations

• The prose-to-formal binding is untrusted, and strict-chain well-formedness excludes conflicts involving strict-rule conclusions.The guarantees therefore do not establish that formal targets faithfully represent prose claims.Source: §7.6 · p. 27
• Lowering an artifact reconstructed from a finished paper is model-mediated, so rejection identifies a fault in the proposed lowering, not necessarily in the research.Agents that record claims, evidence, and attacks during research could emit Lara programs directly instead.Source: §7.6 · p. 27
• The surface syntax was developed only to exercise the calculus end to end; its reliability and efficiency for language-model authoring remain future questions.The paper leaves authoring-language design unexamined.Source: §7.6 · p. 27

Abstract and structured argumentation

• Lara builds on Dung-style frameworks and Caminada labellings, but adds a checked language that generates frameworks and a gap status for claims lacking complete support.Compilation is proved to preserve a direct source semantics.Source: §8 · p. 27
• Building on ASPIC+, Lara adds evidence admission, replayable strict certificates, and mandatory critical-question discharge; its contribution is a checked instantiation, not a new abstract defeat semantics.Its consistency result also requires attack completeness and an explicit strict-chain restriction.Source: §8 · p. 27

Semantic publishing

• Unlike representation models that supply objects for reasoning tools, Lara specifies a certificate language, decidable acceptance, and compilation that aligns claim statuses with source judgments.Its realization theorem does not establish faithful prose-to-formal binding.Source: §8 · p. 27

Possible-world semantics and bisimulation

• Lara’s possible worlds are accepted programs, bridges are accessibility, and claim statuses are valuations; its modal queries concern support across declared contexts, not claim truth.A declared bridge preserves grounded status under checked conditions, but does not establish domain comparability.Source: §8 · p. 28

Proof-carrying architectures

• Applying proof-carrying discipline to defeasible support, Lara permits accepted support to lose justification and supports different strict backends without a shared backend logic.The results do not establish full abstraction.Source: §8 · p. 28

Verified and agentic claim checking

• Lara computes statuses from declared support and attacks, while leaving faithful natural-language formalization outside its semantic guarantee.LLM assessments can propose certificates, but acceptance depends on replaying the checker.Source: §8 · p. 28

9 Conclusion

• A decidable checker derives claim statuses from declared evidence, obligations, and attacks; cross-context status preservation requires stronger correspondence than transporting support.A translated argument can remain well formed while added evidence defeats its claim.Source: §9 · p. 28
• Researchers still choose bridges and defend their meaning; the checker makes the consequences inspectable, while broader artifact lowering and bridge discovery remain future directions.The conclusion envisions versioned policies developing into community review standards.Source: §9 · p. 29

A Mechanization status

• Thirty-five specification results are mechanized across five pipeline stages, while the source-boundary admission family has a separate set of eight properties.The audited public theorems are sorry-free and use only Lean’s standard three axioms; three arguments remain on paper, and some private executable examples trust native evaluation.Source: A Mechanization status · p. 33

A.1 Narrower scopes and component-level results

• G2’s backend dependency-accounting result is an interface obligation, while G6’s executable direct-consistency proof covers complete claims from accepted units, not arbitrary caller-supplied claims.G6’s closure and indirect-consistency clauses are paper arguments over the mechanized edge relation.Source: §A.1 · p. 33
• Additional component results cover backend soundness, syntax round trips, atom well-sortedness, and comparison polarity; representation checks exclude normalized sort names and certificate-payload types.The round trip concerns abstract syntax, while surface-calculus theorems separately cover elaboration above the parsed-AST boundary.Source: §A.1 · p. 33

A.2 The source-boundary admission family

• Property 1 establishes bidirectional agreement between declarative admission and executable evaluation, while Property 3 validates attack endpoints and retains their raw-endpoint-filtered aligned projection; Property 6 says stricter decisions only remove structure.Claim statuses are deliberately non-monotonic when decisions tighten from admit to quarantine.Source: §A.2 · pp. 33, 36

B Measurement inventories

• The appendix records implementation inventories at distinct repository revisions, and the performance measurements use a separate snapshot from current conformance checks and historical harness counts.Current differential checks use b62d33e0, ablations use 7d0f7384, performance uses 5dd326b8, and historical harness counts retain 89c25ef.Source: B Measurement inventories · p. 36

B.1 The trusted base

• Acceptance trusts a defined set of decoding, checking, backend, compilation, status, and diagnostic components; signatures, policies, registries, and allowlisted theory digests are trusted inputs.Other components, including the elaborator and backend proof terms, are untrusted; kernel guarantees depend on backend laws.Source: §B.1 · p. 37

B.2 Conformance checks

• The finite conformance suites report agreement on 673/673 verdict-bearing and 66/66 malformed inputs, but do not prove implementation equivalence.The Haskell production checker is differentially tested against compiled Lean semantics; tests also cover admission, constructors, and surface conformance.Source: §B.2 · p. 37

B.3 Mutants and rejection classes

• A historical harness drove 541 mutants and 60 corpus units, agreeing with expected rejection classes and Lean on 601/601 inputs; the checker has fourteen rejection classes.Localization mutants use a seeded answer key re-derived from each mutant.Source: §B.3 · p. 37

B.4 Ablating the checks

• Removing obligation discharge admits 18 incomplete-argument mutants; removing conflict scanning admits five missing-covering-attack mutants, and disabling typed attacks admits those five plus 32 more.The weakened checkers issue statuses for admitted mutants that should have been rejected; no ablation changes other cases.Source: §B.4 · pp. 37–38

• About 630 µs is the median end-to-end corpus-unit time, versus 280 µs for the predecoded check-plus-render kernel.The estimated marginal decode cost is about 352 µs; it is derived from per-unit median differences, not a separately timed parser stage.Source: §B.5 · p. 38
• About 250 ms covers one pass over the 601-record harness, while the Lean reference driver takes about 4 ms including startup and decoding.These protocols are not comparable to the in-process production measurements.Source: §B.5 · p. 38
• The compiled frameworks contain at most two nodes and one edge per corpus unit, so the timings establish low overhead only on small inputs.Source: §B.5 · p. 38

C Exploratory corpus study

• 48 of 60 sampled claims are gaps, nine justified, and three defeated; unmet mandatory questions locate where encoded support stops, not whether the original investigations lacked support.The sample’s 249 obligations include 71 unmet mandatory questions, 68 producing located gaps and three defeaters.Source: C Exploratory corpus study · p. 39, Table 10 · p. 39
• Nine inference-scheme families cover all 60 claims, while only three typed attacks validate; the sample cannot explain whether sparse attacks reflect source records or annotation and encoding limits.The preliminary expressibility assessment concerns judged expressibility, not compiler acceptance.Source: C Exploratory corpus study · pp. 39–40, Table 11 · p. 39

C.1 Study limitations

• The 32-artifact corpus was assembled rather than sampled from a frame, and human review is pending after one machine annotation pass per artifact.Only the claim-type field was double-annotated for 18 of 60 claims; bridge discovery and automated literature review were not evaluated.Source: C Exploratory corpus study · p. 39, §C.1 · p. 40

D Case studies

• The case studies replay checked programs and show support checks across empirical and non-empirical arguments, but researchers supply the formal claims, evidence, and objections.The studies do not establish automatic extraction, agreement with human reviewers, or truth of encoded claims.Source: D Case studies · p. 40

D.1 A rebuttal exchange as three checked programs

• A rebuttal completes c_kurt’s missing variance support and restores c_bench by defeating its attackers, while conceded c_measure remains defeated under the unchanged policy.The exchange separates completing missing support, defending an existing claim, and leaving a defeat unanswered.Source: §D.1 · pp. 41–42, Table 12 · p. 41, Figure 13 · p. 41

D.2 Verdicts rendered as reviews

• The deterministic renderer produces 51 review comments for 48 gap and three defeated claims, tracing each diagnosis to checked declarations rather than discovering objections.The nine justified claims raise no comments.Source: §D.2 · p. 42

D.3 Genuine versus apparent disagreement

• When compared propositions share a setting, mutual rebuttal leaves both claims contested; a setting mismatch creates no attack and leaves a comparability question requiring shared-setting evidence.Researchers must judge whether setting identifiers faithfully represent the experiments.Source: §D.3 · p. 42, Table 13 · p. 43

D.4 A philosophical debate without measurements

• In the philosophical debate, assumptions and attributed premises support arguments without measurements; a defense can reinstate a claim, while other positions remain contested.The authored policy and unreviewed prose-to-atom bindings mean the checked result does not settle the philosophical positions.Source: §D.4 · p. 43

D.5 Withdrawing an assumption blocks proof reuse

• Admission retains the premise and argument, quarantine removes both and leaves a gap, while rejection stops admission without producing a claim status.The table summarizes the three policy choices; structural results come from the separate Lean witness.Source: §D.5 · p. 43, Table 14 · p. 44
• Withdrawing a premise differs from defeating an argument: this example contains no attack.Source: §D.5 · p. 44
• Withdrawing the assumed premise changes the target context’s admitted leaves, so the structural bridge contract fails and no mapping can supply the source premise.The Lean witness also distinguishes this transport failure from the locally computed status change.Source: §D.5 · p. 44
• The case checks premise admission and certificate dependency, using Haskell tests for admission and local statuses and Lean for the transport boundary.The current lara pw command refuses the quarantined world before loading bridges; that refusal is not the structural-bridge result.Source: §D.5 · p. 44

E Contextual representation independence

• Contextual representation independence proves that acceptance-preserving injective backend relabeling leaves observations unchanged for admissible fragment-context pairs when the context is fixed.The observation is the link fault, checker error, or grounded statuses of exported conclusions; the result also survives embedding in a composed context.Source: E Contextual representation independence · pp. 44–45
• The congruence extends to every extension semantics without attack-extensionality, but grounded contextual equivalence does not imply equivalence under every adequate semantics.A linked three-cycle separates stable from grounded observation; a singleton-selector semantics supplies the counterexample to the unrestricted implication.Source: E Contextual representation independence · p. 45
• Typed hole substitution fills named critical-question answer positions with support terms, deriving support with the same root conclusion and residual obligations.An obligation-free instantiation crosses the unchanged compilation boundary, and congruences pass through instantiation when relabeling also fixes certificates in context fillings.Source: E Contextual representation independence · pp. 45–46
• Relational parametricity generalizes the context quantifier to certificate-assurance relations, with the graph case recovering the earlier theorem and localized acceptance requiring side conditions.The required relation is partial-bijective: collapsing distinct certificate payloads can merge wrappers and change an exported claim from justified to defeated.Source: E Contextual representation independence · p. 46
• The appendix does not establish full abstraction; declared imports alone miss attack-completeness and subargument dependencies, and completeness depends on policy.The fragment’s semantic interface is wider than its declared imports, and policies with no declared conflict cannot separate fragments by forcing a label.Source: E Contextual representation independence · p. 46

F The image of compilation

• Every realizable structured framework satisfies the compiler invariant for the fixed policy’s declared conflict data, and this necessity is preserved under isomorphism.Realizations also require every node conclusion to be well sorted under the signature.Source: F The image of compilation · p. 47
• A one-node self-edge framework satisfies the invariant under a policy with no contrary pair or exception, yet is unrealizable because that policy permits no attack.Source: F The image of compilation · p. 47
• The counterexample refutes sufficiency for arbitrary fixed policies; sufficiency remains open for policies with declared conflict.The result retains conclusion labels and does not characterize label-erased Dung frameworks.Source: F The image of compilation · pp. 46–47

G The verified surface boundary

• The independently defined surface judgment has a deterministic, sound, and complete executable checker for a decidable supported fragment of the presentation AST.The judgment includes syntax restrictions and declarative core obligations rather than merely wrapping executable success.Source: G The verified surface boundary · p. 47
• A derivable surface input elaborates to core output accepted by the checker while preserving the authored obligation ledger, resolved attacks, reconstructed conclusions, and question order.Source: G The verified surface boundary · p. 47
• For supported inputs, successful elaboration plus core acceptance reflects to a surface derivation; neither condition alone suffices.Reflection is for the given surface input, not a claim of surjectivity onto core units or unique source recovery.Source: G The verified surface boundary · p. 47
• Direct surface observations equal compiled core observations for attack-extensional extension semantics, including the five named instances.A missing claim identifier remains missing on both sides rather than becoming an empty-support gap.Source: G The verified surface boundary · p. 48

H Extension-semantics distinctions and source transport

• Gap is semantics-independent exactly when support is empty, but other statuses vary; stable nonexistence is reported for the bare three-cycle and disappears when an argument attacks all three members.On the bare three-cycle, stable observation of a supported claim is a no-extension report, not a four-state status.Source: H Extension-semantics distinctions and… · p. 48
• Source-level observations match compiled observations only under support-boundedness, which is necessary; credulous readings cannot be represented as four-state statuses or determined by acceptance profiles alone.The credulous reading remains exposed as per-argument bits.Source: H Extension-semantics distinctions and… · p. 48

I Proofs for the metatheory

• Three arguments remain on paper only: the pipeline cost bound, NP-completeness bookkeeping, and clauses of the rationality-postulates theorem.The appendix identifies the Lean declarations for the mechanized proofs.Source: I Proofs for the metatheory · p. 49

I.1 Checking

• Structural recursion yields a terminating, sound, and complete support checker; finite matching and scans check attacks and program-level conditions.The support checker verifies instantiated patterns, premise counts, identities, partitions, and assurances.Source: §I.1 · p. 49

I.2 Compilation and claim statuses

• Grounded evaluation terminates deterministically, and compiled statuses equal direct statuses; quarantine guarantees non-promotion only for justified claims.The quarantine result does not establish the converse for the other statuses.Source: §I.2 · pp. 50–51
• The grounded extension is closed under declared subarguments and strict steps, conflict-free, and cannot justify two contrary claims.Strict-step closure applies to declared instances; the calculus does not manufacture undeclared ones.Source: §I.2 · pp. 50–51

I.3 The image of compilation

• Every accepted program’s compiled framework satisfies the stated invariant, but satisfying that invariant is not sufficient for a framework to be compilable.The non-sufficiency example uses a one-node self-edge framework under a policy with no contrary pair or exception.Source: §I.3 · p. 51

I.4 Semantics-parametric observation

• Grounded observation reduces to the singleton extension, while source-level observation transports across attack-extensional semantics under carrier-local support.The gap arm depends only on the support set; stable semantics can have no extension, producing a no-extension report for a supported claim.Source: §I.4 · pp. 51–52

I.5 Strict-certificate backends

• Strict-certificate backends expose opaque encodings and replay, while injective payload relabelling preserves checked programs, frameworks, and claim statuses across backend replacement.Backend composition is occurrence-local, so combining certified occurrences does not relate their formula types, theories, or consequence relations.Source: §I.5 · pp. 52–53

I.6 Contextual representation independence

• Contextual relabelling preserves linked-program observations, and typed-hole substitution and relational parametricity extend congruence under partial-bijection constraints.Partial bijectivity is necessary: collapsing payloads can merge wrappers and change an exported claim from justified to defeated.Source: §I.6 · pp. 53–54

I.7 Source updates and status dynamics

• 10 add-instance status transitions are reachable; fresh leaves preserve status, and non-instance or additive updates cannot cross the gap boundary.On clean sources, additive public transitions match core transitions and do not reach evidence-blocked; cleanliness is necessary for that result.Source: Table 15 · p. 55, §I.7 · p. 55

I.8 The verified surface boundary

• Verified elaboration preserves accepted core programs, reflects supported fragments only when both support and core acceptance hold, and yields surface observations coherent with the compiled framework.The direct and compiled observations agree for attack-extensional semantics when support remains in the carrier.Source: §I.8 · pp. 55–56

I.9 Cross-context comparison

• Cross-context bridges transport support and preserve grounded statuses when a Boolean-checkable total attack bisimulation and support correspondence hold.With an accepted successor for every context, boxed and diamonded translations are equivalent to the local status atom; modal K and necessitation hold, but T, D, B, 4, and 5 fail on generic frames.Source: §I.9 · pp. 56–57

I.10 Cost

• Grounded evaluation uses at least n^2 and at most n^3(1 + n) attack queries, and a realizable family requires at least k^4 queries for k ≥ 2.Credulous complete acceptance is NP-complete on the realizable class; the core pipeline is polynomial in explicit input size, but no bound is established for compact surface-source size or backend internals.Source: §I.10 · pp. 57–58

J Case-study and worked-example listings

• The listings use claims to name propositions, leaves to declare evidence, and arguments to construct support or challenges under policy rules.Discharges supply evidence for named critical questions, open declarations record unanswered optional questions, and attack declarations identify the challenged argument part.Source: J Case-study and worked-example listings · p. 58

J.1 Certified comparison under attack

• The certified inequality remains justified while the headline claim is defeated because the attack targets the declared comparability premise, not the arithmetic.The comparison block generates both the strict re-check and defeasible bridge; the audit undermines the bridge at its binding premise.Source: §J.1 · pp. 58–59

J.2 Rebuttal replay

• The rebuttal restores the benchmark claim, leaves the conceded measurement claim defeated, and supports the ablation claim after adding variance evidence.The response also counterattacks both benchmark attackers; Lara computes each claim’s outcome from the declared changes.Source: §J.2 · pp. 59–60

J.3 Mechanical-reviewer output

• Lara’s renderer produced 51 review comments—48 gap and 3 defeated—using checker verdicts and located diagnostics in fixed templates, with no free-text generation in the rendered comments.The examples show an empty support set and a defeated support with its attacker, illustrating requests to provide a complete argument or answer an attack.Source: §J.3 · p. 60

J.4 Agreement map

• Opposing claims in the same setting remain contested, while a setting mismatch prevents the corresponding conflict and leaves the claims justified.A single setting-index difference flips the pair from contested to justified; opposing wording alone does not create an attack.Source: §J.4 · pp. 60–61

J.5 Philosophical assumptions, objections, and defenses

• The philosophy program requires answers about indispensability and nominalist scope; number identity remains contested, while a reply restores the fictionalist argument.The final undercut defeats the fictionalist argument’s attacker.Source: §J.5 · p. 61

J.6 A certificate that depends on an admitted assumption

• The certificate reuses an admitted parallel-postulate premise rather than proving a geometric theorem; quarantining that premise removes its support and leaves the claim a gap.A separate Lean witness shows that a structural bridge cannot preserve the premise in an empty target evidence environment.Source: §J.6 · p. 62