ARCADIA-Studio/harness/release-analysis-baseline-contract-20260911.md

Analysis baseline, effective cases and complete freezing: candidate contract

Codex-956atf /root/requirements_delta, 2026-09-11. Ownership: this report and the isolated analysis-baseline fixtures. No production, Cargo, native, prior frozen report, ledger, commit or push changes. Read current goal, Gitea issue #1 through #131, the 218-assertion context experiment, paired review, current reference/session/source/API boundaries, and coordinated the library contract with /root/library_compatibility. Root selected B as the next active-study architecture; this document closes a candidate for criticism and implementation, not a shipped capability or final release scope.

The experiment supports B's reduction in repeated assumptions: 62 versus 480 bindings in the controlled twenty-case task. It also falsifies evaluation of an inherited formula in its baseline context and demonstrates why a shallow copy cannot freeze a study. It does not prove native usability, actual Studio source admission, numeric/unit behavior or package correctness. Its factored D variant correctly changes a shared threshold in one definition; do not justify B by denying that result.

1. Normative candidate and boundaries

Each EngineeringProperty owns one explicit base binding. ModelBaseline means the collection of those bindings in the captured project. A Case selects that same collection and replaces exactly its listed bindings. The evaluator always receives ModelBaseline or Case(id) explicitly. Checks are shared identified predicates, independent of cases.

There is no separately created AnalysisBaseline element, baseline UUID, selected/default case, case inheritance, property fallback search, or implicit connection to a DataValue/default/unit string. A baseline context has identity without requiring an extra authored record: the model identity, captured accepted document identity and ModelBaseline selector identify it. Two captures of the same project at different accepted revisions are different evaluation contexts even if the baseline arithmetic happens to match.

Retain the existing proposed pure definitions, typed expressions and quantities, with the amendments below. Source/JSON names are concrete candidates. Schema 8 in the fixtures denotes the proposed successor to inspected source7, not an already allocated production version. Root must assign the actual next schema version with the combined library/language change.

enum Binding { Unbound, Expression(Expr) } // required; literal is an Expr leaf
enum BaselineBase { ModelBaseline }       // one admitted variant
enum EvaluationContext { ModelBaseline, Case(Id) }
enum AnalysisSubject { Element(Id), Relation(Id) }
enum ScalarType { Boolean, Number, Quantity(DefinitionRef) }
enum AnalysisType { Scalar(ScalarType), List(ScalarType) } // finite, flat

// New SharedBody variants in existing OA/SA Elements, each with parent == None:
EngineeringProperty {
    subject: AnalysisSubject,
    value_type: AnalysisType,
    display_unit: Option<DefinitionRef>,
    base: Binding,
},
AnalysisCase {
    subject: Option<AnalysisSubject>,
    base: BaselineBase,
    overrides: BTreeMap<Id, Binding>, // EngineeringProperty IDs; duplicate keys reject
},
AnalysisCheck {
    subject: Option<AnalysisSubject>,
    documented_constraint: Option<Id>,
    predicate: Binding,              // required Boolean expression, or Unbound
},

// Neutral Project.definitions catalog; library import/mount/instance additions
// use the paired library contract. Parameters are scoped, not Elements.
struct Definition { id: Id, alias: String, name: String, description: String,
                    body: DefinitionBody }
enum DefinitionBody {
    QuantityKind(QuantityKindDefinition), Unit(UnitDefinition),
    Calculation(CalculationDefinition),
}
struct Parameter { id: ParameterId, name: String, value_type: AnalysisType }
struct CalculationDefinition {
    parameters: Vec<Parameter>, result: AnalysisType, body: Binding,
}
enum DefinitionRef {
    Local(Id),
    Imported { import: Id, package: PackageId, member: Id },
}
struct EvaluationTargets { properties: Vec<Id>, checks: Vec<Id> }
struct EvaluationRequest {
    context: EvaluationContext, targets: EvaluationTargets,
    numeric_profile: ProfileId,
}

The scalar/Expr/unit structures and exact rational wire representation remain those in the earlier proposal, sections 3.2 and 4, except the complete R6 algebra below replaces its incomplete anonymous-type rules. Binding replaces ambiguous optional expressions everywhere. Missing a required base/predicate/body field, supplying null for a Binding, or duplicating an override/argument key rejects. Optional explanatory references may be null. Unknown closed-record fields reject.

The three analysis kinds are layer-root Elements, preserving the current Element identity/name/alias/description and OA/SA body structure. Property subject is required; case/check subject is optional. Subjects must be existing same-layer semantic Elements or Relations, excluding analysis records. Subjects associate analysis with architecture; they do not create containment, lookup scope, a case selection or an implicit check set. Documented Constraint references must identify a same-layer descriptive Constraint. Formal evaluation uses the check predicate; it does not parse that Constraint's prose.

Every expression owned by a property/check/case may read only same-layer EngineeringProperties. A Case can be evaluated only with targets in its layer. ModelBaseline may select targets in either/both layers, each retaining separate same-layer dependency graphs. Cross-layer studies require an explicitly reviewed extension; the first integration must not weaken existing layer/reference rules accidentally. Properties are not implicitly restricted to the subjects of the selected check or case.

Neutral definition IDs share the live project identity reservation domain with existing project records. Parameter IDs are unique within one CalculationDefinition and are qualified by that definition's resolved identity; they are not ordinary project references. Parameter names are unique source identifiers within that definition. Definition aliases follow local source alias uniqueness; imported aliases use the library-qualified resolver.

2. Resolution, shared checks and reusable definitions

For every property p and explicit context c:

effective(p, ModelBaseline) = p.base
effective(p, Case(k)) =
    k.overrides[p], if that key exists;
    p.base, otherwise.

The selected binding supplies an expression, not a previously evaluated result. Every Property(q) read recursively evaluates effective(q, c), preserving the original requested c, even when the caller's formula came from p.base. No evaluator API may accept a property ID without an explicit context. A cache key containing only a case's source or override map is invalid.

Authored/command state	Meaning	Result when the base is a known value
Property base is Unbound	The model assumption is explicitly unknown.	Baseline is Missing; an explicit case expression may supply a value.
Override key absent	Use that property's base.	The base expression is evaluated in this case.
Override key present with Unbound	This case explicitly lacks the value.	Missing; the known base is masked.
SetOverride(case, property, Expression(expr))	Create/replace one override.	Use expr in the case.
ClearOverride(case, property)	Remove the override key; absent key is an exact no-op.	Use the base. Clearing a key whose base is Unbound remains Missing.
SetBase(property, Unbound)	Change the model assumption to unknown.	Affects baseline and cases that do not override it.

Clear is an editing operation, never a persisted third Binding state or null synonym. In full source/JSON replacement, removing an override row is Clear; writing unbound is SetOverride(Unbound). There is no ResetBaseToDefault operation because there is no hidden default. Text and GUI must name these two actions distinctly.

Proposed narrow Command variants are SetAnalysisBase { property, binding }, SetAnalysisOverride { case, property, binding } and ClearAnalysisOverride { case, property }, using existing externally tagged command JSON and batch admission. The table's shorter names describe these operations. For example, the complete clear command is {"ClearAnalysisOverride":{"case":"99d3e09a-0ec3-4194-9dd4-9f3de6625cde","property":"63a931c2-675a-4fce-89e5-04361cb99450"}}. Ordinary record creation/deletion continues through the shared typed command boundary; source replacement must produce the same accepted result and revision behavior.

One AnalysisCheck ID identifies one predicate, optionally linked to one documented requirement, evaluated in any explicitly selected compatible context. Cases do not own checks or check lists. Evaluation targets explicitly identify the checks to run. To vary a threshold, use an ordinary typed threshold property and a case override; to express a different predicate, deliberately create/edit a different check. This avoids silently duplicating the same requirement predicate in every case. The example uses four properties (including the threshold), two cases and one shared check.

CalculationDefinition bodies are pure: they may use scoped Parameter nodes, literals, operators and calls to other definitions; they cannot read Property/Check/Case nodes or capture a project, UI state, file, clock or network. Every call supplies exactly one argument for every declared parameter, with no extra/missing keys or parameter default lookup. Source argument names resolve to stable ParameterIds. All arguments evaluate in the caller's effective context; after that the body sees parameter values only. Declared argument/result types are enforced at the boundary. A Boolean result can be called by a check.

Parameters have explicit stable IDs after admission. Renaming one changes the scoped declaration/use tokens, including named arguments at call sites, while preserving the ID. Reordering the parameter list preserves call meaning because arguments are keyed by ID; it may change presentation and the specified strict-argument evaluation order. Changing a parameter's type or deleting it must validate/repair all calls atomically. An Unbound definition body is admitted as an incomplete definition and produces a located Missing cause; it is not a silently uninterpreted foreign function.

3. Admission, deletion and outcomes

Admission validates the baseline dependency graph and the complete effective graph for every stored case in that layer. It cannot validate the baseline and override fragments independently. A baseline edit can create a cycle in an otherwise unchanged case, so every affected effective graph must be rechecked before the one candidate is accepted. An implementation may use sound incremental validation, but its answer must equal full validation.

All stored references and expression types are checked, including shadowed base expressions, unused branches and overrides outside the current target selection. Property edges come from typed Property nodes. Checks depend on properties; properties cannot read checks. Pure calculation call graphs must be acyclic. Cycles reject even if the cycle's branch would not execute for current values. This deliberately makes validity independent of a transient numeric input or chosen target. Unbound and an evaluated false predicate are both valid authored states; warnings may identify incomplete records.

Operation	Required invariant
Delete a property used by a formula, check or override map	Reject unless the same explicit batch repairs/removes the dependent references or records. Never silently prune a sum term, formula operand or override row.
Delete/reidentify a subject	Require explicit removal/rebinding of associated analysis links, or a valid typed identity remap in the same batch. Association is not automatic deletion ownership.
Delete a Case	Leaves properties, their bases and shared checks intact. Live references to that Case must be repaired; an external frozen capture remains historical.
Delete a unit/kind/calculation/parameter	Repair every live typed use, including display units, definition bodies and calls. An unused display unit is still a live reference.
Reidentify a property/case/check/local definition	Update only the corresponding live typed reference categories, including override keys; reject collisions. Do not rewrite UUID-shaped prose or immutable historical snapshots/package bytes.
Rename an alias or move an authored declaration between files	Preserve its explicit UUID and exact unaffected source bytes. Use the source index for typed reference tokens; alias text replacement is not an identity operation.
OA/SA transition or library export	Use the explicit analysis selection in section 7. Ordinary architectural containment/outgoing references cannot infer subjectless cases/checks.

Strict operators evaluate their operands left to right; calls evaluate arguments in parameter declaration order and lists in element order. For a strict node, collect nonvalue causes from its required children before producing a nonvalue; do not perform the numeric operation when a required child has no value. If a call's body is Unbound, add that missing-body cause as well. Boolean and conditional control flow is different: if/and/or evaluates only the branch selected by a known controlling Boolean. A missing/failed condition propagates without inventing a branch. Thus true || unknown is true, while unknown || true is Missing. Both branches remain statically checked.

enum ValueOutcome {
    Value(AnalysisValue),
    Missing { causes: NonEmpty<MissingCause> },
    Failed { causes: NonEmpty<EvaluationCause> }, // at least one supported-operation failure
}
enum CheckOutcome {
    Satisfied, Violated,
    Unresolved { causes: NonEmpty<EvaluationCause> },
}

Missing causes identify an Unbound property binding, check predicate or definition body. Supported-operation failures include division by zero, zero to a negative power, 0^0 and NumericLimit. These are evaluation failures, not false requirements. If a strict expression encounters both missing inputs and a failure, Failed retains both classified causes rather than losing the missing information. Causes are deduplicated by typed origin/location and ordered deterministically; a bounded dependency trace identifies consulted expressions and branches without enumerating exponentially many paths.

Only Boolean true/false produces Satisfied/Violated. Every nonvalue check is Unresolved with the original causes. An empty requested check list is allowed when properties are requested, and must be described as no checks; an entirely empty or duplicate target selection rejects. Invalid source/type/reference/cycle is an admission/request rejection, not an evaluated Failed value. Q1's closed AST contains only supported operations: an unknown function is a located rejection, while a request for an unavailable numeric profile/conversion is an explicit capability rejection. Do not fabricate an admitted unsupported Expr node to hide missing mathematics.

4. R6: closed internal dimension and operator algebra

This section is a complete candidate for the exact profile's internal scalar types. It does not infer physical quantity kinds from equal dimensions.

Symbol	Internal type
B	Boolean
N	Exact dimensionless Number
L(K,d)	Named linear quantity with verified nominal kind key K and dimension d
P(K,J,d)	Named affine point kind K with declared linear difference kind J and dimension d
A(d)	Anonymous linear intermediate with dimension d, permitted only inside expressions

Dimension d is the fixed seven-component integer vector (length, mass, time, electric current, temperature, amount, luminous intensity), each component in -32 through 32. A(0) is immediately normalized to N, so there are not two anonymous dimensionless types. A named dimensionless L(K,0) remains named and distinct from N.

For local kinds, K includes local identity within the captured private project. For imports, sameness uses the paired library contract's verified equivalence key: contract profile, nominal package/member/class origin and canonical rooted typed interpretation graph. Names, comments and archive revisions alone do not determine equivalence; different origins remain distinct even with identical dimensions. Coordinate basis, algebra and difference-kind closure must agree. Exact DefinitionRefs/pins remain provenance. This is the sibling's recommended R2 policy, still requiring root ratification and an executable conformance gate; do not substitute hash-only/name/dimension comparison.

Public property/call outputs retain their declared kind reference and its verified key. Internal arithmetic uses K; it does not arbitrarily choose the left operand's archive revision as a result identity. This makes same-origin compatible revisions usable without discarding exact pins. An incompatible coordinate basis requires explicit migration, never this equality relation.

In the table, “same” means identical normalized internal type, including the verified nominal key where present. Every unlisted combination rejects during typing; there are no coercions through JSON numbers, unit strings, Boolean truthiness or list broadcasting.

Operation	Permitted operands and result
Unary minus, abs	N, L(K,d), A(d); preserve type. P and B reject.
Logical not	B -> B.
Add/subtract, ordinary linear operands	N/N -> N; L(K,d)/same -> same L; A(d)/same -> same A, normalized at d=0. Named/anonymous mixtures and different named kinds reject.
Affine arithmetic	P(K,J,d) - same P -> L(J,d); P +/- L(J,d) -> same P; L(J,d) + P -> P. P+P, L-P and other point/interval combinations reject.
Multiply/divide, both N	N. Division's zero-domain check is at evaluation.
Multiply by N; divide by N	N times L or A, L or A times N, and L or A divided by N preserve the non-Number type.
N divided by L or A	A(-d), normalized; a named dimensionless denominator therefore yields N.
Product/quotient of two non-Number linear operands	Any L/L, L/A, A/L or A/A yields A(d1+d2) for product or A(d1-d2) for quotient, normalized. No named result is guessed.
Integer power	Exponent must be a syntactic integer in -16..16. N stays N. L/A power 0 -> N, power 1 preserves type, all other powers -> A(n*d), normalized. Every point power rejects, including exponent 1. Zero-domain failures are evaluated separately.
Numeric order and equality/inequality	N/N, same L, same P, same A -> B. Differently typed numerical values reject, even if their magnitudes happen to be equal.
Boolean equality/inequality	B/B -> B. Boolean ordering and list equality reject.
and/or	B/B -> B, with the conditional evaluation rule above.
if	B condition; both branch types must be the same normalized internal type. Result has that type. There is no inferred common named/anonymous supertype.
AsKind(K, value)	Target must be a linear kind. A(d) -> L(K,d) only for matching dimensions. N -> L(K,0) is allowed explicitly, closing the A(0) normalization case. A named operand or affine target rejects, even for a redundant same-name assertion.
List construction	Flat, homogeneous exact internal scalar type; no implicit element conversion. An empty list requires a type from its declared destination/call parameter or the explicit Sum initial value. Otherwise reject ambiguous empty type.
Sum(list, initial)	Both element type and initial must match N, L or A exactly. Returns that type; empty list returns initial. P/B lists cannot be summed.
Assignment, call parameter/result, public property output	Must match the declared Scalar/List(Boolean/Number/Quantity) type. A nonzero anonymous dimension requires AsKind before this boundary. No public anonymous quantity type is introduced.

Anonymous addition/comparison is intentional. For example L(Force)*L(Length) + L(Force)*L(Length) produces A(energy-dimension), and one outer AsKind(Energy, ...) is sufficient. A product followed by a quotient stays legal without intervening casts. A quotient of different named kinds with equal dimensions yields N; this is explicit dimensional algebra, not permission to add or directly compare those named kinds. An author can deliberately form Energy/Torque as a scalar ratio, but Energy + Torque and Energy == Torque remain invalid.

Unit coordinate conversion remains exact magnitude*scale+offset. Linear units require positive rational scale and zero offset. Affine point units use the point kind's coherent basis and declared difference kind; point subtraction yields an interval. Display units must be compatible with the declared quantity type, never choose input interpretation, and cannot alter authored literal magnitude/unit.

Q1 retains normalized exact rationals with 4096-bit reduced numerator/denominator, canonical decimal string wire components, 1234-digit literal-component maximum with actual bit checking, canonical integer/ratio source closure, finite expression/list/call limits, and no global epsilon. The R7 literal 10^300 and 1/(2^4095) must preserve literal AST identity through source and JSON. 0^0 is explicitly a runtime DomainError in this refinement, removing the earlier proposal's ambiguity about “rejected.” Dimension/exponent overflow is a typing rejection; numeric magnitude/intermediate budget failure is NumericLimit. These bounds need measured implementation review, not claims of performance.

One further AST distinction must be explicit: expression minus is Unary(Negate), not an implicit constant-folding rule. The ratio literal constructor accepts a signed integer numerator. Therefore a negative Number literal node canonically emits ratio(-n,d), including when d=1; a Unary(Negate, Number(n)) node emits unary minus. A negative Quantity literal similarly uses a signed ratio magnitude before its unit suffix. This preserves both admitted ASTs without requiring a context-sensitive signed-number lexer. The complete negative-boundary packet exercises the literal case; the implementation gate must also retain a distinct unary-negation node. Direct negative numbers remain concise authored expressions, but source formatting may not silently turn one AST category into the other.

This exact profile remains a foundation. Degree/radian conversion involving pi, trigonometry and other ordinary engineering approximations require a separately specified approximate profile and validation. The release's declared breadth is not satisfied by labeling those operations unsupported indefinitely. This contract does not ratify an exact-only whole release.

5. Complete examples, source contract and minimum authoring

The complete proposed source starts with a project and all required OA subjects, a local Duration kind, second/millisecond units, one pure calculation with two parameters, four properties, one shared check and two subjectless cases. All 17 identities are actual distinct UUIDs, including the two scoped parameters. There are no omitted imports, management snapshots, diagrams, externally created subjects or placeholder UUIDs.

It is 55 lines / 2678 UTF-8 bytes with all UUIDs present: four base bindings, two override bindings and one check predicate. These are fixture counts, not a usability result. The calculation definition is intentionally included to exercise parameter identity; replacing its call with inline addition is legal and removes that optional authoring overhead. A first property needs one property declaration with a visible base value, assuming its subject/type/unit already exist. It does not require a case or reusable calculation. A two-duration budget needs its input/result properties and one check; a separate threshold property is optional until threshold reuse/variation is wanted.

The complete candidate portable document includes every current Project collection, all proposed definition/import/mount/instance collections and exact source. Empty maps are explicit. The paired library catalog's final serde/schema details still require common ratification. A PowerShell constructor built these data fixtures and verified JSON transport, distinct UUID spellings, exact retained source bytes and freeze capsule equality. It did not parse the proposed grammar, evaluate quantities, verify Project/source equality, or run Studio tests. The expected observations are hand-derived and explicitly labeled.

Minimum source rules to add to the normative grammar:

• A property requires base followed by unbound or an expression. A case requires base ModelBaseline and an overrides block; duplicate property keys reject. A check requires predicate. A calculation requires body; an unfinished body is explicitly unbound. Optional explanatory fields have existing none spelling.
• Local @alias in expression value position resolves only a property; @alias(...) resolves only a calculation; [@alias] on a numeric literal resolves a unit. $name resolves only the current definition's parameter. Subject @alias resolves the unique typed Element/Relation category. Imports use the paired qualified-reference mechanism; no separate analysis-only resolver.
• Calls name parameter aliases, which resolve to IDs; serialized argument maps use those IDs. Keywords ratio(n,d), pow(expr, integer), abs(expr), as_kind(@kind, expr), sum(expr, initial: expr), and if condition then expr else expr lower to the already closed AST. ratio is one exact literal node; division is a distinct operator.
• Precedence from tightest to loosest is atom/call/literal-unit suffix, unary minus/not, multiply/divide, add/subtract, one non-associative comparison, and, or, conditional. Arithmetic is left associative; chained comparisons reject; parentheses preserve grouping. pow avoids an additional exponent associativity rule. Both sides of a conditional are expressions; nested conditionals associate through the grammar, not whitespace.
• A sparse dimension clause names only the seven fixed dimensions and lowers to the existing seven-entry vector; duplicate names/out-of-range exponents reject, omitted components mean zero. This is explicit dimension notation, not quantity-kind inference.
• Fresh initial declarations/parameters may omit IDs only through documented shared source admission that inserts and returns them. Established declarations retain IDs. A raw alias rename with unchanged UUID but unrepaired references rejects; typed rename updates declaration and typed uses atomically. Parameter IDs cannot be silently regenerated by renaming an argument.
• Additions, targeted edits and deletion use the same index/update/history boundary as current source. Preserve unaffected comments, quotes, whitespace, includes and authored decimal spelling. Dirty drafts retain their original context and are never silently evaluated/applied as accepted state.

Suggested minimal GUI transactions match that text. Add analysis value on a selected subject visibly enters Base, type, value and unit and creates one property in one undo transaction. A budget editor can create its complete properties/check in one batch. Create alternative visibly names Model baseline and records only entered overrides. The inspector/evaluation result names Model baseline or the actual case; a case row shows its effective value and whether its binding is Base or Override. Set unbound and Use baseline are separate controls. Evaluating uses the labeled accepted document and does not apply another pending editor.

These requirements are additive semantic authoring work, not a promise that a few keywords solve the entire large-model language. The separate text-only audit still owns namespace, declaration/metadata noise and CLI workflow decisions. No new CLI is claimed here. The production slice must provide the same actions via published API/source tooling without a GUI-generated seed.

6. REST, revision/provenance and explicit freeze

Candidate read-only routes are POST /api/v1/projects/{resource_id}/analysis/evaluate and POST /api/v1/projects/{resource_id}/analysis/freeze. Both require an exact If-Match for the accepted hosted document the caller selected. This deliberately makes the snapshot selection reviewable; no body field can forge the server revision. Capture the matching immutable document under the existing store boundary, then evaluate/export outside the lock. A concurrent later write does not mutate the capture; the response identifies its original revision/ETag. Missing/stale/malformed preconditions retain existing 428/412/400 behavior.

The complete evaluation bodies are in baseline, degraded and unmeasured. The degraded body, without omitted IDs:

{
  "context": {"Case": "38036c65-16d4-449c-837b-91eb141c1d93"},
  "targets": {
    "properties": ["bd5b68e8-65fc-4e35-9071-a73061316a4b"],
    "checks": ["bac0de99-9d2f-4e53-9158-d424ecac61bf"]
  },
  "numeric_profile": "Q1-exact-1"
}

The baseline context wire value is the unit variant "ModelBaseline"; a Case value is the single-key object shown. Context and numeric profile are mandatory, and target IDs must be unique/right-kind/current. A semantically invalid request returns 422; a false, Missing or failed supported evaluation returns a successful report with the typed outcome, not a save rejection or HTTP failure. Resource/body budgets and strict JSON handling follow the existing API contract.

Reports identify model.id; server resource/revision/ETag or local accepted document-instance/revision stamp; requested context, targets and numeric profile; exact definition environment capture; and every consulted binding's origin. Origin distinguishes ModelBaseline from CaseOverride(case), with property ID and source/AST location. A base-origin total formula can read an override-origin receive time; reporting only the formula's origin would conceal the assumptions. Public quantity outcomes use canonical exact coordinates and their declared type reference/key; display conversions are separate derived data.

One accepted model/source pair receives one document revision under the existing rules. There is no separately maintained mutable baseline revision or mandatory per-property revision. Comment-only edits can produce a different accepted document revision with the same numerical result. A cache key must include the accepted capture, context, targets, profile and exact definition environment, either separately or through one complete document identity. Reidentifying a live model cannot rewrite the origin of an earlier frozen capture. An asynchronous UI discards or visibly marks a result from a superseded capture.

Preferred first freeze is a whole immutable accepted PortableDocument capture, with explicit context/targets/profile and a validated complete effective-binding manifest. It is an exported artifact, not a new live baseline/case/check element or an automatically added project history record.

1. Atomically capture the complete accepted Project, exact SourceBundle, all local definitions, all immutable imports/pin closures and every required package archive's exact bytes. Validate that source/package compilation reproduces the captured Project and that each pin resolves to the supplied bytes. Reject missing/corrupt/incompatible content; do not fetch or consult another project's cache.
2. Include all applicable properties in the effective-binding manifest: all in the selected Case's layer, or both layers for ModelBaseline. Capture each effective Binding, including Unbound, and its Base/Override origin. Include every shared check predicate in those layers; target lists still explicitly determine which outputs were requested. These manifests are derived, validated against the capture, and cannot override it.
3. Retain the entire local pure-definition environment and every imported package in the captured document, including nonselected branches and unused imported declarations. No local definition reference can resolve against a later ambient project. Package bytes/pins and the verified compatibility-profile version travel together; a digest without content is incomplete.
4. Emit a versioned envelope with the exact portable document bytes and their SHA256, originating document stamp, model ID, context/targets/profile, manifests and definition-capture inventory. The concrete fixture uses a base64 UTF-8 JSON byte capsule plus a decoded companion file for inspection. The hash commits the exact captured bytes; it is not claimed as a semantic equivalence hash or a publisher trust proof. Decoding is bounded and strict.
5. Reopen/replay by decoding, checking the digest, admitting the captured PortableDocument through the common validator, and verifying the redundant manifests. Evaluate only that private capture. The same IDs denote historical objects in that private namespace; they are not inserted into the current live Project ID map. Exported descriptions/origin stamps are provenance assertions, not authentication.

The complete frozen degraded fixture contains the exact full portable document, four effective bindings and the shared check, explicit local-definition inventory, and an explicitly empty import/package set. Empty is correct for this fully local example, not a missing imported environment. Its decoded companion exposes every captured field; there are no management placeholders. The local origin UUID/revision in the fixture is an illustrative accepted stamp, not a claim of a real Studio session.

The nonempty pinned-package freeze gate remains mandatory with the sibling's complete library fixture: capture both selected and unselected imported content, remove the ambient source/package files, reopen offline, mutate a byte under an unchanged pin and require rejection, then publish a cosmetic revision and show the frozen original remains unchanged. Experimental package bytes may exercise transport but must not be labeled production archive grammar. Exact archive/pin fields and compatibility proof validation use the paired library contract; the analysis subsystem must not invent a second package format.

The sibling's final full-prototype D1 experimental archive has raw SHA256 28df5ea3447918dfee3c6ed4243d8f986c689f93a54d89c6181b47d6c2f39b33; its cosmetic D2 archive is a35102e04b9f6822ab409ab43f83eded33edd0a3a3c1f589245bb7b123ce4779. These are concrete nonempty bytes for the paired capture test, not a production archive schema, normative UUID example, or a claim that this report's local fixture imports them. A frozen D1 environment must retain D1 even where verified typed compatibility also permits D2 for a later live use.

This whole-capture choice costs space and retains unrelated captured architecture/cases. It deliberately avoids guessing a minimal architectural/analysis closure and prevents incomplete freezing of factored definitions. Deduplication may share immutable bytes internally, but every standalone export/recovery must contain them. A smaller closed independent document is a worthwhile later alternative; it must demonstrate exact subject/definition/history closure and unchanged semantics before replacing this contract. A result-only report and a shallow copied Case are different operations and must not be called a reproducible frozen study.

The artifact can be created and replayed by text/API clients. Creating a local editable independent study from it is an explicit open/fork/import operation with its own identity policy; replay does not silently adopt the snapshot into another project. No new third live evaluation context variant is needed: the private document still evaluates ModelBaseline or Case(id).

7. Integration with libraries, transitions and current boundaries

The selected-case closure is an explicit AnalysisSelection of property IDs, check IDs and whole case IDs, separate from architectural selection. It follows required typed property/definition dependencies, all bindings of every selected whole case and declared external subject/property roles. It never inverse-pulls every case mentioning a selected property, and never silently slices a case's override map. Missing dependencies require explicit inclusion or an external role decision. A subjectless case/check is valid and cannot be inferred from architectural parentage.

The sibling library contract uses this selection for patterns. Instance materialization allocates new property/check/case IDs and remaps their live typed architectural/property references. ModelBaseline has no UUID to remap; it means the property-owned bases of the resulting instance/project. Imported neutral definitions retain exact qualified pins or become explicit local copies with captured private definitions; they are not accidentally routed through the architectural Element remapper. An unrelated project-wide case sharing a property remains untouched unless explicitly selected.

OA/SA transition must expose the same analysis inclusion/omission choices and same-layer subject/property remapping. Root's combined transition/library contract owns mounted definitions, exact opposite-layer exports or explicit local derivatives. New analysis Kind mappings alone cannot recover the required associations. No transition should silently create a case, take current evaluated numbers as new baseline literals or claim preserved frozen provenance after remapping.

Inspected current boundary	Required integration
model.rs:13, :229, :1621	Existing OA/SA layer and Element fields remain authoritative; add closed body variants, definition catalog and identity reservation. No mandatory baseline record.
session.rs:11, :170; references.rs:392	New narrow base/override/parameter edits lower into one clone/validate/admit batch. Existing deletion cleanup must not erase semantic analysis dependencies silently.
references.rs:17, :154	Add typed Expr/subject/check/override-key visitors; distinguish local live IDs, scoped parameters, imported members and frozen historical IDs.
source_project.rs:286, :780; source_project/source_migration.rs:4	Shared compile/stabilize/update/migrate path must cover every new field, ID/ref token and exact source file; new schema must reject old parser claims honestly.
semantic/types.rs:88	History/snapshot closed vocabulary needs deliberate additions; frozen/private captures are not live reference graphs. No UUID-shaped string rewriting.
transitions.rs:203, :447	Explicit analysis selection and inspected same-layer materialization, not only a mapping for new Kind names.
docs/api.rst:13, :188, :288	Preserve accepted model/source revision, ETag and atomic command/source behavior; add pure capture endpoints and full source/JSON/OpenAPI parity.

The API already distinguishes service resource identity from model identity and increments revision for source-only changes. It does not retain arbitrary past server revisions. Therefore an origin ETag alone cannot reopen a frozen study; retained exact source/model/package content is essential. No new external standards assertion is needed to derive these rules from the experiment and current code. The earlier primary standards research remains context, not an automatic resolution of Studio's architecture.

8. Falsifiers and exact first implementation slice

These expected observations are not runtime results from the proposed model. The executable 218-assertion experiment establishes the analogous context behavior; the new UUID/source/quantity/library integration still needs implementation.

Complete fixture/change	Required observation or rejection
Baseline total/check	750 ms + 1 s = 7/4 canonical seconds; Satisfied against 2 s.
Degraded Case total/check	Base-origin formula reads overridden receive time: 1250 ms + 1 s = 9/4 seconds; Violated. Returning 7/4 falsifies effective-case resolution.
Unmeasured Case	Explicit Unbound receive override gives Missing input 63a931c2-675a-4fce-89e5-04361cb99450 and Unresolved check; no zero/fallback.
Clear that override	Exact removal restores 7/4 seconds and Satisfied. Setting the property base to Unbound then clearing remains Missing.
Set degraded receive formula to total	Effective dependency cycle rejects the complete batch. Also test a later baseline formula edit that creates a cycle only in an existing case.
Change shared limit base to 5/2 seconds	Same check ID now satisfies baseline/degraded; no copied predicates are changed. Override limit only in one case and only that case differs.
Change dispatch base from 1 to 2 seconds after freeze	Active degraded total becomes 13/4; frozen degraded stays 9/4 with old inputs/formula/environment. Case source may be unchanged.
Change combine body from a+b to a+b+b after freeze	Active degraded becomes 13/4 from the original input bases; frozen stays 9/4. A full binding list retaining a live local definition fails this test.
Delete receive, a referenced property, or a used calculation	Reject unless explicit same-batch repair is supplied. Case deletion alone retains all bases/checks.
as_kind(Energy, (2 N_force * 3 m) + (4 N_force * 5 m))	Two A(energy-dimension) intermediates add; explicit result is 26 J with the declared Energy kind. Symbols here denote explicitly defined units in the future R6 fixture.
(2 kg * 3 m) / 2 s	Anonymous momentum intermediate with canonical coordinate 3; assign to Momentum only with AsKind.
(2 N_force * 3 m) < (4 N_force * 5 m)	True; comparison of same-dimensional anonymous products is permitted.
Energy / Torque with equal canonical coordinates	N equal to 1 is permitted; Energy + Torque and direct equality reject. Equal dimensions do not erase named kind identity.
anonymous result / same-dimensional anonymous result	N; explicit AsKind of a named dimensionless kind is possible. Implicit named dimensionless -> Number assignment rejects.
20 degrees C - 10 degrees C; 20 degrees C + 5 K_interval	10 K_interval and 25 degrees C under declared affine definitions. Point+point, point scaling and point power reject.
If branches named Energy versus anonymous energy dimension	Reject; explicit AsKind in the anonymous branch repairs it.
1/0, 0^0, false predicate, Unbound input	Failed, Failed, Violated, Missing respectively. No common “false/error” bucket.
Literal AST 10^300 and the rational with numerator 1/denominator 2^4095 constructed via JSON	Canonical source spells the full integer/ratio denominator and returns exactly the same literal AST; exponent notation here describes the mathematical fixture, not accepted ratio-argument syntax. Complete literal packets include the negative 4096-bit boundary as well.
Subjectless selected case/check plus an unrelated case sharing p	Explicit pattern/transition selection preserves selected complete analysis and leaves the outside case untouched.

The next production slice should be one complete vertical implementation, with independently constructed expected Project/source/REST results:

1. Admit the complete local fixture through source and JSON using shared core types, then show exactly equal model identity/ASTs. Add base/override/check/definition visitors and transaction validation before desktop forms. Cover Unbound, Clear, shared checks, inherited formula context and baseline-induced case cycles.
2. Implement the closed exact evaluator and R6/R7 boundaries with independent rational/dimension expectations, plus false/Missing/Failed classification and provenance. Include nested anonymous sums/products/quotients, empty Sum typing, compatible mixed-revision kinds, affine operations and literal serialization boundaries.
3. Expose explicit accepted-context evaluation and whole-document freeze/replay through the published REST/source workflow. Verify ETag races, source comments/file layout, complete local definitions, exact nonempty package pins/bytes, private offline resolution and tampered-manifest/package rejection. No hidden cache or GUI initialization may be needed.
4. Add the minimal native property/base/case/check authoring path using the same operations; verify explicit context/origin display, Use baseline versus Unbound, single undo/redo, exact save/reopen and stale result handling. A pending draft must not be applied by Evaluate.
5. Integrate the sibling's two-instance/selective-update/outside-consumer and OA/SA analysis-selection fixture before claiming reusable analysis or transition parity. Keep approximate numeric capability, dense text/source authoring and the rest of the user's release objective open until their own accepted slices exist.

Root's consequential ratification points are limited and explicit: shared root checks with threshold properties; same-layer analysis plus explicit cross-layer work later; all effective graphs statically valid even for unused branches; strict argument/Boolean evaluation policy; whole capture rather than minimum closure; declared-output kind anchoring with verified same-origin compatibility; and the exact-versus-approximate capability boundary. The B direction is already selected. None of these refinements should silently become production defaults merely because this paper fixture is complete.