ifc-0129

9.4.1 Transforming a factor, interchange, or domain theory

9.4.1 Transforming a factor, interchange, or domain theory

When the selected enriched-sketch doctrine admits the required tensor product, its semantics identifies several distinct transformational targets. If \(\mathbb A\otimes \mathbb B\) presents the current repair calculus, a proposal may:

  1. extend or revise the assimilatory factor \(\mathbb A\);

  2. extend or revise the proto-accommodative factor \(\mathbb B\);

  3. change the interchange generators or equations relating the factors;

  4. change the domain sketch \(\mathbb S\) on which the calculus acts; or

  5. change the enrichment, tangent doctrine, observers, or integration semantics needed to interpret the preceding structures.

These interventions have different empirical signatures. A side failure motivates repair of one factor. Two coherent sides with a persistent mixed defect motivate an interchange change. A coherent and integrable repair calculus, together with a registered expressivity argument ruling out the required scientific object, motivates a domain-theory extension. Experiments should not pool these diagnoses into one generic “schema change” label.

Integrability provides a gate between local diagnosis and declaration surgery. When the proposed infinitesimal repair integrates within the existing theory, no declaration change is yet warranted; the resulting work may be ordinary repair, combination, or exploration. When a registered finite-realization observer rejects it after the relevant controls, that failure is evidence for transformation but remains underdetermining: it does not say which factor, interchange law, or domain object should be added. Candidate extensions must still be generated, transported, and independently admitted.

. A transformational DIAL trace must name the edited level, provide a counter-witness against adequate realization inside the old declaration— including finite integration when that is the relevant control—specify the new presentation and its model semantics, and test a finite consequence not used to choose the edit.