PaperlayerView exact revision on arXiv

Source-linked AI summary

Foundations of Algebraic Architecture Theory: A Rising Sea of Geometry, Transport, Comparison, and Reconstruction

Hiroyuki Nakahata

arXiv:2609.27638v1cs.SEcs.PL

TL;DR

AI-generated changes make it important to determine what they preserve and when local descriptions determine a whole. The paper specifies structure and preservation through readings and encodes lens and protocol semantics with typed facts and laws; its examples show operation constraints narrowing the compatible changes.

Abstract

from arXiv · show

AI-generated software changes make it increasingly important to determine what a change preserves, where local consistency fails to extend globally, and which alternatives remain. We develop the foundations of Algebraic Architecture Theory (AAT) from Atoms, typed primitive facts, and Laws, equations that objects must satisfy. A reading specifies what counts as structure and which operations and laws to preserve. The main reconstruction theorem identifies the category of full geometries and all their structure-preserving morphisms with an independently defined category of local models, up to equivalence. Objects are recovered up to isomorphism and morphisms between fixed endpoints uniquely. The theory addresses gluing, diagnosis, transport, classification of changes, and reconstruction. From finite Atom families we construct cores closed under operations and geometries with sites and coefficients. We give conditions under which a Cech obstruction detects the existence of a global state and, through comparison with repair semantics, a global repair. We compare diagnoses and give a finite criterion for uniform invariance given computable finite data. Transport along exact changes has a universal property and commutes with base change on exact pointed pullback squares. Comparisons of routes generated from the same square, finite comparison diagram, and geometry factor into an invertible comparison and an idempotent normalization. We characterize when observations determine comparison preservation and classify compatible lifts. Encodings of lens and protocol semantics preserve and reflect laws and recover semantics-preserving morphisms. Applications classify and count operation-preserving changes and extend morphisms uniquely from finite tables. Corresponding Lean declarations are listed in the appendix.

6 Idempotent Normalization and Realization

Chapter 6 covers idempotent normalization, generated comparisons, and how normalization interacts with changes.

6 Idempotent Normalization and Realization

  • The chapter covers selecting representations, lifting normalization to a structure-preserving idempotent, and completing objects.Source: §6 · p. 5
  • It classifies generated comparisons of full geometries and collects normalized objects and changes into a category.Source: §6 · p. 5
  • It treats when normalization and change can be interchanged, the category of comparisons, and what remains for lenses and protocols.Source: §6 · p. 5

7 Comparison-Preserving Changes and Information

Chapter 7 addresses changes that preserve comparisons, what observations reveal about them, and how compatible changes are classified.

7 Comparison-Preserving Changes and Information

  • The chapter considers changes preserving one comparison and changes carried from the same generator.Source: §7 · p. 5
  • It examines when observations distinguish changes and how restriction, reflection, and lifting relate to normalization.Source: §7 · p. 5
  • It constructs lifts for full geometries and classifies the information and lifts retained by generated comparisons.Source: §7 · p. 5
  • The chapter classifies changes through connections among operations and considers consequences for lenses and protocols.Source: §7 · p. 5

8 Presentation and Local Reconstruction

Software changes raise questions about what structure is preserved, how local descriptions assemble, and when those descriptions determine a whole. The paper calls its mathematical foundations Algebraic Architecture Theory and makes a reading specify the structure and preservation requirements.

8 Presentation and Local Reconstruction

  • Chapter 8 is organized around finite presentation, compatibility and gluing, reconstruction, applications, and finite and infinite models.Source: §8 · p. 5

Introduction

  • AI-generated changes motivate the need to decide what structure changes preserve, where local consistency fails globally, and what alternatives remain.Source: Introduction · p. 7
  • A reading specifies what counts as structure and which operations and laws a change must preserve.Source: Introduction · p. 7

Five questions

The section frames five questions about fitting local states together, preserving diagnoses and comparisons, and assembling local descriptions. Together, they ask what information and compatibility conditions are needed to reason about changes across a whole system.

Five questions

  • Clock conversions that fail around a cycle prevent a global assignment satisfying every specified relation, raising whether timestamps can be corrected consistently.Source: Five questions · p. 7
  • Diagnosis requires retaining connection and conversion data across grouped regions to detect discrepancies that individual inspection misses.Source: Five questions · pp. 7–8
  • Route agreement requires corresponding data and operations that satisfy the same conditions; invertible conversions alone do not ensure agreement.Source: Five questions · p. 8
  • Comparison-preserving changes must keep the full order state, including payment data, consistent across migration and update routes.Source: Five questions · p. 8
  • Local descriptions assemble into one design and migration only when teams agree on shared transaction data, completion conditions, and correspondences.Source: Five questions · p. 8

Architecture relative to a reading

A reading specifies what counts as structure and what changes must preserve; Atoms, operations, Laws, and locality determine the resulting architecture objects and geometries.

Architecture relative to a reading

  • Atoms are typed primitive facts; configurations combine finite Atom families with relations, while Laws state equations that architecture objects must satisfy.One example is a required relationship between reading and updating a state.Source: Architecture relative to a reading · p. 9
  • The core generated from an extracted Atom family is the smallest family of objects closed under the permitted operations.It keeps object formation, operations, and equations together.Source: Architecture relative to a reading · p. 9
  • A full geometry equips a core with local contexts, covers, overlaps, coefficients, and local data for later comparison and reconstruction.The title's “Rising Sea” metaphor points to common objects supporting different software questions through the same mathematical constructions.Source: Architecture relative to a reading · p. 9
  • A reading fixes the vocabulary, extraction rules, object formation, equations, operations, and locality that determine which maps are admitted.Retaining updates as well as displayed values changes which maps preserve the structure.Source: Architecture relative to a reading · p. 9

Correspondence with the semantics of CS

The paper encodes lens and protocol semantics in Algebraic Architecture Theory, relating their laws and semantics-preserving maps to typed constructions and applying common results to classify changes and extend morphisms.

Correspondence with the semantics of CS

  • The lens encoding preserves and reflects the original laws, and typed morphisms recover the original semantics-preserving morphisms.For protocols, finite operation tables satisfying path relations and observation conditions determine realizations, while suitable vertex maps recover semantics-preserving morphisms.Source: Correspondence with the semantics of CS · pp. 9–10
  • The correspondences provide a route from a software question to an AAT theorem and back, with each stating whether it gives equivalence, implication, or one-way preservation.This describes how the paper uses the independent semantics and their typed constructions together.Source: Correspondence with the semantics of CS · p. 10
  • In the product-lens example, preserving displayed address and unset payment leaves four candidate changes, but preserving updates leaves two; in the worker protocol, the counts are sixteen and four.The common classification theorem says changes are one permutation per connected component of the operation graph, because preserving an operation that leaves internal state unchanged forces its endpoint state changes to agree.Source: Correspondence with the semantics of CS · p. 10
  • The correspondence identifies comparison-preserving changes by group isomorphism and supports restrictions of lens views and protocol realizations to selected data.The reconstruction principle also yields unique extensions of lens and protocol morphisms from compatible finite tables.Source: Correspondence with the semantics of CS · p. 10

Main constructions and their consequences

The section is introduced as a reading guide to the paper's parts, chapters, questions, and results developed.

Main constructions and their consequences

I: Geometry and Local Consistency

This section concerns the construction of objects and geometries, and the obstruction to gluing local consistency into a global state or repair.

I: Geometry and Local Consistency

  • The central question is when local states fit together.Source: §I · p. 10
  • The section's stated scope includes constructing objects and geometry.Source: §I · p. 10
  • It also addresses obstructions to gluing and their relation to repair.Source: §I · p. 10

II: Diagnosis and Transport

The section asks whether diagnoses survive changes of reading and presents diagnostic invariance alongside universal transport and coherent comparisons.

Diagnosis and Transport

  • The section asks when a diagnosis survives a change of reading.It also asks when structure can be carried along a change.Source: §II · p. 10
  • Diagnostic invariance is a central result of this section.Source: §II · p. 10
  • The section also develops universal transport and coherence of comparisons.Source: §II · p. 10

III: Comparison and Normalization

This section asks when two construction routes agree and what normalization retains, then develops base-change comparisons and classifies comparison invertibility.

Comparison and Normalization

  • The section asks when two construction routes agree and what normalization retains.Source: §III · p. 10
  • Base-change comparisons are developed as a result of the section.Source: §III · p. 10
  • The section classifies comparison invertibility and compatible changes, and addresses recovery of objects and morphisms.Source: §III · pp. 10–11

IV: Classification and Reconstruction

The section develops methods for diagnosis, transport, comparison, classification, and reconstruction. Its reconstruction theorem identifies full geometries with independently defined local models up to equivalence.

Chapter 1: Geometry and local consistency

  • Finite Atom families generate cores containing exactly the objects reachable by finite sequences of permitted operations.Contexts and covers define a site, while compatible restriction maps give a presheaf of rings and its sheafification.Source: §IV · p. 11

Chapter 2: Geometry and local consistency

  • Under stated torsor, restriction, and sheaf conditions, a degree-one Čech obstruction vanishes exactly when local states admit a global state.Under correspondence and completeness conditions, repair semantics' obstruction class is identified with the equations' class, connecting vanishing to global repair.Source: §IV · p. 11

Chapter 3: Diagnosis and transport

  • Under Condition C, diagnostic comparison induces an isomorphism on first cohomology; uniform invariance has a decidable finite criterion when the required data are computable.The criterion reduces to vanishing of kernels and cokernels indexed by nonempty subsets of values.Source: §IV · p. 11

Chapter 4: Diagnosis and transport

  • Exact changes reindex extracted Atoms bijectively, and transported cores are characterized by unique factorization of further changes.For finite comparison diagrams, edge reselection can make every face commute exactly when the obstruction to removing discrepancies vanishes.Source: §IV · p. 11

Chapter 5: Comparison and normalization

  • On exact pointed pullback squares, transport and pullback are related by an invertible Beck–Chevalley comparison; backward transport along refinements requires reflection of extraction on the realized locus.Source: §IV · p. 12

Chapters 5–6: Comparison and normalization

  • Generated comparisons factor into an invertible comparison and an idempotent normalization, and are invertible exactly when the normalization factor is the identity.Otherwise they give an isomorphism between retained images in the idempotent completion, distinguishing normalized agreement from recovery of the original structure.Source: §IV · p. 12

Chapter 7: Classification and reconstruction

  • Observations determine comparison preservation exactly when their kernel lies in the comparison-preserving group; compatible lifts of each fixed normalized change form a torsor under its kernel.Lifts can exist even when normalized information does not determine whether a given change is compatible.Source: §IV · p. 12

Chapter 8: Reconstruction

  • Full geometries and independently defined local models are equivalent, recovering objects up to isomorphism and morphisms between fixed endpoints uniquely.The reconstruction uses compatible primitive data over finite fragments; lens and protocol cases explain when a finite table suffices.Source: §IV · pp. 12–13

Organization and reading guide

This section develops Algebraic Architecture Theory from readings that specify structure and preservation, through finite cores, local contexts, sites, sheaves, coefficients, and lens and protocol semantics. It then connects local law failures and Čech obstruction classes to global gluing and repair, and introduces the question of how diagnoses persist as Laws, resolutions, or local structure change.

Organization and reading guide

  • The guide assumes basic algebra and category theory, routes readers by topic across Chapters 2–8, and points to appendices for Lean declarations and proof-build instructions.Preliminaries fix notation; Appendix A lists declarations with assumptions and source versions, while Appendix B gives source locations and build instructions.Source: Organization and reading guide · p. 13, Preliminaries and Notation · p. 14

Overview of the Chapter

  • Finite Atom families generate cores closed under operations and geometries equipped with sites and context-specific coefficient rings.The chapter also sets up local reading and gluing as part of the reading-dependent construction.Source: Overview of the Chapter · pp. 18–19
  • A three-level projection tower connects extraction, core, and geometry; lens and protocol encodings preserve and reflect laws and recover semantics-preserving morphisms.The cited propositions cover the tower and the validity of laws under the encodings.Source: Overview of the Chapter · p. 19

1.1 Atoms and relative extraction

  • For each source and extraction doctrine, a unique Atom family is determined, while readout is separate and may fail to distinguish distinct Atoms.The family records adopted facts; a separate map specifies what information is read from them.Source: §1.1 · p. 20

1.2 Configurations, objects, and operations

  • Configurations pair Atom families with relations and identifications; architecture objects add typed structure and quantities, and operations form a category when unit and associativity laws hold.Operations act on configurations, and the action is required to preserve identity and composition.Source: §1.2 · pp. 21–22
  • A reading selects structure and operations to track, including functional or predicate invariants and finite multi-axis signatures.An invariant reading assigns an invariant to each index; a signature reading selects axes and their values for each object.Source: §1.2 · p. 22

1.3 Local contexts and Laws

  • Contexts specify readable positions, axes, and observables, while Laws are equations evaluated locally through residuals that vanish when the equations hold.Required equations must have vanishing residuals on every context and Atom for an object to be lawful.Source: §1.3 · pp. 22, 24

1.4 Finite detection and generation of the core

  • Sound and complete finite detectors characterize lawfulness: required circuits are empty exactly when all required equations hold.Circuits are finite structural patterns; soundness links a detected pattern to equation failure, while completeness ensures failures have such a pattern.Source: §1.4 · p. 25
  • The relative core is the smallest family containing the base object and closed under operations, equivalently the objects reachable by finite operation sequences.The construction also retains the initial configuration, context category, equation system, circuits, operations, invariants, and signature.Source: §1.4 · pp. 25–26

1.5 From covers to sites

  • Coverage requirements and chosen overlaps generate a smallest Grothendieck topology, whose adequate covers provide the information needed to connect local equation validity with gluing consistency.The AAT site retains its construction data; adequacy requires that the specified visibility and interaction information is available on the cover.Source: §1.5 · p. 28

1.6 Presheaves, sheaves, and geometries with coefficients

  • A sheaf uniquely glues matching local sections, and every presheaf has a universal map to a sheafification.The sheafification receives a natural transformation from the presheaf, and every map from that presheaf to a sheaf factors uniquely through it.Source: §1.6 · pp. 28–29
  • Sheafification extends matching local presentations uniquely, and an input that is already a sheaf is unchanged up to isomorphism.The two-point example illustrates how sheafification can add locally compatible sections.Source: §1.6 · pp. 29–30
  • Context coordinates and structural equations define quotient rings whose restriction maps make the local data a presheaf of commutative k-algebras.Source: §1.6 · p. 30
  • Changing coefficients induces a raw-system change that respects identity maps and composition of coefficient homomorphisms.Source: §1.6 · pp. 30–31

1.7 Morphisms of readings and the three-level projections

  • An exact change preserves and reflects extraction and equation validity, while the three reading levels form categories B, Ecore, and Egeom linked by projections.The projections forget geometry to extract the core, then extract the extraction doctrine, selected source, and their maps.Source: §1.7 · pp. 31, 34

1.8 Model synchronization: the semantics of reads and updates

  • The lens and protocol constructions preserve and reflect their original laws, and their typed morphisms correspond one-to-one to semantics-preserving morphisms.This correspondence transfers later classification and local-reconstruction results back to the original semantics.Source: §1.8 · p. 35
  • A total lens decomposes its states into displayed values and a reference fiber, and its morphisms correspond bijectively to maps between reference fibers.Under this decomposition, updates replace the displayed value while leaving the reference-fiber component unchanged.Source: §1.8 · pp. 36–37
  • For product lenses, preserving updates forces the same fiber change across views; the example has four read-preserving changes but only two that also preserve updates.Each fiber can independently use the identity or swap when only reads are preserved; update preservation ties those choices together.Source: §1.8 · p. 37

1.9 Protocols: named operations and all executions

  • Finite state sets, edge maps, and observations satisfying the declared path relations and observation naturality determine exactly one protocol realization.The conditions are checked on the finite input tables, rather than by enumerating paths.Source: §1.9 · p. 38
  • Vertex maps satisfying edge and observation commutativity uniquely extend to protocol morphisms, covering all executions through path induction rather than enumeration.Finite protocol data can govern paths of arbitrary length, including those repeating cycles.Source: §1.9 · p. 39

1.10 Constructing Atoms, operations, and Laws from semantics

  • An equation system makes an architecture object Lawful exactly when its lens or protocol operation data satisfy the corresponding semantic laws.For protocols, these equations are the path-relation and observation-naturality conditions.Source: §1.10 · pp. 42–43
  • Semantics-preserving lens and protocol morphisms correspond naturally to typed morphisms, with protocol morphisms uniquely determined by their vertex maps.The source-map correspondence is faithful and retains non-injective semantics-preserving maps.Source: §1.10 · pp. 42–44

Summary of the Chapter

  • The smallest family containing an extracted finite Atom family and closed under permitted operations consists exactly of objects reachable by finite operation sequences.With a sound detector and completeness for the required equations, Laws hold exactly when required circuits are absent.Source: Summary of the Chapter · p. 44
  • The chapter builds sites and sheafified local structure, relates extraction, core, and geometry by projection functors, and recovers lens/protocol Laws and semantics-preserving morphisms.The constructed Laws hold exactly when the original laws hold, and typed morphisms correspond one-to-one to the original semantics-preserving morphisms.Source: Summary of the Chapter · p. 44

Overview of the Chapter

  • Locally lawful states may fail to glue; the chapter studies overlap discrepancies modulo local corrections, with vanishing yielding a global repair under evaluation and repair-sheaf conditions.The overview identifies the obstruction class of specified local data and states that the repair conclusion requires maps connecting symbolic equations to evaluations, plus local correction actions and gluing.Source: Overview of the Chapter · pp. 45–46

2.2 Spaces satisfying the Laws and evaluation

  • Closed subschemes represent points satisfying equations through vanishing evaluation, providing a geometric locus for lawful states.The overview frames this as the equivalence between Laws holding and factorization through the lawful locus.Source: Overview of the Chapter · p. 45

Why we connect to the semantics of repair

  • The chapter connects computed obstructions to permitted repairs by identifying equivalent local changes and residuals, then carries obstruction zero and nonzero verdicts back to repairability [SAGA, §§4–5].It constructs the coefficients, local states, and comparison maps needed to prove the correspondence of obstruction classes and the existence of repairs.Source: Why we connect to the semantics of… · p. 46

2.1 Local algebras and ideals of equations

  • Local configurations are presented as coordinate families satisfying structural relations, while required Laws generate sheaf ideals whose enlargement strengthens their zero-locus conditions.The chapter also defines witness and obstruction ideals for individual and required Laws.Source: §2.1 · pp. 47–48

Evaluating symbolic equations into residuals

  • Under Construction 2.6’s realization conditions, required residuals vanish exactly when a test map factors through the lawful locus; compatible object realizations make this equivalent to lawfulness.The conditions connect symbolic equation evaluations to residual evaluations before imposing that required residuals vanish.Source: Evaluating symbolic equations into… · pp. 49–51

2.3 Coefficients representing obstructions

  • Obstruction discrepancies require abelian-group coefficients; quotient groups and maps from finite failure patterns encode differences, with the coefficient choice determining which differences count as equivalent.Source: §2.3 · p. 51
  • Under local soundness and completeness, required Laws fail on a context exactly when some local circuit has a nonzero coefficient image, provided every circuit image is nonzero.If images are aggregated, nonzero images must not cancel; independent direct-sum coordinates ensure this condition.Source: §2.3 · pp. 52–53

2.4 Comparison on overlaps and Čech obstruction classes

  • On a fixed cover, overlap differences form Čech cochains, and a 1-cocycle class is zero exactly when the differences can be removed by local corrections.For three charts with empty triple overlap, the cycle period identifies the obstruction class; with coefficients M, the first Čech cohomology is isomorphic to M.Source: §2.4 · pp. 53–54

2.5 From vanishing of the obstruction class to gluing

  • For a local atlas of torsor states, overlap differences define a Čech 1-cocycle, and its class vanishes exactly when corrections yield a global state, uniquely for that corrected family.The equivalence requires the state presheaf to be a sheaf; conversely, a global state supplies corrections making the cocycle a coboundary.Source: §2.5 · p. 55

Application to local states satisfying the Laws

  • For lawful local states, the obstruction class vanishes exactly when a global lawful state exists, assuming the lawful-state torsor action and sheaf conditions hold.Finite-check applications must connect readable information and detected failures to residual vanishing, with nonzero circuit images that do not cancel when aggregated.Source: Application to local states satisfying… · pp. 55–56

2.6 Shape of covers, capacity of obstructions, and detection by cycles

  • Obstruction capacity depends on cochain dimensions, constant coefficients identify Čech cohomology with the cover nerve’s cohomology, and forest-shaped covers have vanishing first cohomology under surjective edge restrictions.Preserving cochain dimensions preserves the Euler characteristic, but individual cohomology groups and specified obstruction classes also depend on the differentials and class.Source: §2.6 · pp. 56–57
  • A cover with no triple overlaps and a forest overlap graph admits correction of every 1-cochain under the stated surjectivity condition, whereas adding a cycle can leave a nonzero period.A triple overlap can force that period to vanish through the cocycle condition.Source: §2.6 · p. 57

Sums along cycles and differences on the boundary

  • Pairing a cocycle with a cycle is unchanged by adding a coboundary, while a nonzero boundary difference induces a cohomology class whose cycle pairing records that difference.For a split complex, the connecting class from a difference on the shared boundary is choice-independent.Source: Sums along cycles and differences on… · p. 58

2.7 Comparison of the structural and semantic phases

  • The structural-versus-semantic split classifies source–Atom pairs by invariance across semantic readings, and Condition S requires restrictions and differentials to preserve the structural subspace.The readings vary semantic interpretation and admissible predicates while preserving vocabulary, normalization, resolution, and source structure.Source: §2.7 · pp. 58–59
  • If Condition S holds and structural H1 vanishes, the semantic obstruction map is injective; examples show that Condition S alone is insufficient and its failure can prevent the quotient differential from descending.The structural forest condition supplies the required H1 vanishing.Source: §2.7 · pp. 59–60

2.8 Concrete integer-coefficient obstructions built from Atoms

  • The concrete construction uses generators pairing Laws with sources and geometry points for local ranges, placing both in one Atom family to compute obstruction classes from local states and transitions.Source: §2.8 · p. 60

Building coefficients from generator relations

  • Quotienting the free abelian group on Law-source generators by label-preserving primitive relations yields coefficients isomorphic to the free abelian group on relation components.Generators with different Law values remain distinct even when other source coordinates are identified.Source: Building coefficients from generator… · p. 60

The eight-point space and two covers

  • The eight-point space admits three-chart and four-chart covers with connected charts and nonempty pairwise overlaps but no triple intersections, so their Čech complexes have zero degree 2.The locally constant coefficient groups form a sheaf on the chosen context site.Source: The eight-point space and two covers · pp. 61–62

Computing obstructions from local states and affine transitions

  • For lawful chart states and affine transitions, overlap differences define a Čech obstruction class that is unchanged by changing local states, while changing transitions can change the class.In the three-chart example, a nonzero class prevents gluing; setting one transition to zero removes that obstruction.Source: Computing obstructions from local… · p. 63

2.9 Semantic local repair and obstruction classes of equations

  • Semantic repair coefficients quotient repair words by relations for equal local effects, and compatible repair actions make each nonempty local state set a torsor; atlas choices yield well-defined obstruction classes.Source: §2.9 · pp. 64–65

2.10 The SAGA comparison and global repair

  • Under the local-state correspondence and completeness conditions, repair and equation coefficients and obstruction classes agree; if repair states form a sheaf, a global repair exists exactly when either class vanishes.The coefficient isomorphism induces isomorphisms of the Čech complexes in degrees 0–2 and of first cohomology.Source: §2.10 · pp. 66–67
  • With fixed parity transitions, the semantic and equation-side obstruction classes are both nonzero and no global repair exists; changing the first transition to zero makes both classes vanish.The comparison matches the classes, and the sheaf condition on repair states connects vanishing to a global repair.Source: §2.10 · p. 68, Summary of the Chapter · p. 69

Summary of the Chapter

  • The chapter builds local algebras and equation ideals, relates simultaneous residual vanishing to factorization through the lawful locus, and constructs affine-transition chart data from Atom families.The lawful-locus result assumes an algebraic presentation of the evaluation data and a localization condition.Source: Summary of the Chapter · p. 68
  • Overlap differences define a cocycle, and changing local states adds a coboundary; under a torsor action and sheaf condition, a zero class is equivalent to a global state.Obstructions vanish on forests under surjective restrictions, while a nonzero cycle period detects an obstruction.Source: Summary of the Chapter · p. 68
  • Repair-word and equation-quotient coefficients become isomorphic under local-state correspondence and completeness conditions, matching obstruction classes and characterizing global repair with the sheaf condition.The connection is stated as Theorem 2.49 and Corollary 2.50.Source: Summary of the Chapter · p. 69

Overview of the Chapter

  • The chapter constructs a coarsest resolution preserving Law evaluations, diagnostic complexes, and cochain maps between cover comparisons, with a sufficient condition for first-cohomology isomorphism.The overview identifies Condition C as the condition for that isomorphism.Source: Overview of the Chapter · pp. 71–72
  • Uniform invariance across adequate resolutions has a necessary-and-sufficient condition reducible to finite computation, and local observation alone can fail.The overview also points to a counterexample for local observation.Source: Overview of the Chapter · p. 72
  • Structural-nerve invariance and vanishing for per-source coefficients are treated separately from the correspondence of specified obstruction classes and equivalence of vanishing.The overview also connects Chapter 2's integer-coefficient obstructions with this chapter's rational-valued diagnoses.Source: Overview of the Chapter · pp. 71–72

Why compare diagnoses

The section develops how diagnoses and their underlying cores and geometries can be compared across changes in semantic reading and resolution, including conditions for invariance, correction, transport, and coherence. It also relates shared-operation preservation and semantics-preserving comparisons to lenses, protocols, and typed constructions.

Why compare diagnoses

  • Comparing diagnoses is necessary because state readings and the regions used to test local consistency can vary, so comparisons need maps preserving diagnostic-value meaning.The section introduces the comparison square and points to obstruction-verdict invariance and concrete zero and nonzero examples in §3.11.Source: Why compare diagnoses · p. 72

3.1 The canonical resolution preserving Law evaluations

  • The canonical resolution is the coarsest resolution that retains the chosen Law values, and every L-adequate resolution maps uniquely to it.It is unique up to a unique bijection commuting with the maps from the sources.Source: §3.1 · p. 73

3.2 Finite computation and presentation by extraction methods

  • For finite sources with decidable evaluation equality, the canonical resolution is computable by grouping sources with identical Law-value tuples.Presentability by a finite family of extraction methods with decidable equality can be checked by comparing the induced equivalence relations; adequate methods alone need not present it.Source: §3.2 · pp. 74–75

3.3 The diagnostic complex from Law values

  • The Law-value diagnostic groups coordinates by Law-value labels, has d1d0 = 0, and decomposes into separate diagnoses for each label.Thus comparisons split into comparisons over the regions where each individual Law value is visible.Source: §3.3 · p. 76

3.4 From comparisons of resolutions to cochain maps

  • Local comparison data between resolutions induce cochain maps that preserve cocycles and coboundaries, and hence induce maps on diagnostic classes.These maps split into comparisons for individual Law-value labels.Source: §3.4 · p. 77

3.5 Diagnostic invariance under Condition C

  • Condition C makes the diagnostic comparison an isomorphism when both resolutions are L-adequate.Within each fiber, connectedness and the cycle-boundary condition allow cocycles to be corrected to vanish on internal edges.Source: §3.5 · p. 79
  • Condition C enables correction of locally removable differences within fibers and unique recovery of the remaining differences on the coarse side.In the three-chart-to-four-chart example, the comparison preserves nonzero diagnostic classes, mapping the coarse edge values to (0, zab, zbc, zac).Source: §3.5 · p. 80
  • Preserving Laws does not by itself ensure that diagnoses correspond, and adding a Law may make it unreadable on the coarse resolution.For diagnoses built from Laws that descend through a resolution, correspondence still requires checking both the retained Laws and the comparison conditions on the covers.Source: §3.5 · pp. 80–81

3.6 Deciding invariance for all Laws

  • Uniform invariance is equivalent to each comparison T_A being an isomorphism for every nonempty subset A of coarse values.With finite computable presentations, the property is decidable by constructing the comparison maps and checking their ranks, rather than comparing group dimensions alone.Source: §3.6 · pp. 81–82
  • The geometric conditions of Corollary 3.24 guarantee uniform invariance and are decidable from finite data, but they are stronger than necessary.Finite examples show uniform invariance even when individual clauses fail.Source: §3.6 · pp. 82, 84

3.7 An example undecidable from local incidence information alone

  • The same local observation can describe one uniformly invariant comparison and another that is not, so local incidence data alone cannot decide invariance.The examples have identical local observations, but their global face relations yield different H1 dimensions; the period around the full face-relation cycle explains the difference.Source: §3.7 · pp. 85–86

3.8 Structural supports and the role of coefficients

  • The structural nerve has ordered Atom tuples as cells, and its cells and incidence relations remain unchanged when the reference semantic reading changes within the family.Tuples consist of Atoms holding simultaneously at a common source; repeated Atoms are allowed.Source: §3.8 · pp. 86–87
  • Structural support can remain invariant while the all-Atom nerve changes; with coefficients separated by source, the diagnostic H1 vanishes by an explicit correction.Thus structural invariance alone does not imply equality of the whole nerves or determine which coefficients read differences.Source: §3.8 · p. 87, Summary of the Chapter · p. 94

3.9 Mapping integer obstruction coefficients to the Law-value diagnosis

  • The coefficient comparison maps integer generator relations to Law-value coordinates and is injective when generators with the same label are connected by primitive relations.For the same local data, the resulting map sends obstruction classes to diagnostic classes.Source: §3.9 · pp. 88–89

3.10 From vanishing diagnoses to integer corrections

  • Under relation-component identification and common representatives, vanishing diagnoses yield integral corrections, so the original obstruction vanishes and the local states glue to a global state.The reflection can fail if either condition is absent: relation components may be merged or diagnostic coordinates may be locally missing.Source: §3.10 · pp. 90–91

3.11 Refinement of covers and invariance of the obstruction verdict

  • Under the stated conditions, refinement from three charts to four preserves obstruction verdicts even though the comparison map between readings is non-injective.The constructed comparison commutes, and the example carries both removable nonzero differences and surviving nonzero obstruction periods across the refinement.Source: §3.11 · pp. 92–93

Transporting coefficients and local contexts by isomorphisms

  • Isomorphisms of local contexts and coefficients preserve obstruction verdicts, while refinement comparisons extend beyond degreewise isomorphisms through Condition C and integer correction.The coefficient isomorphisms must commute with restrictions; the broader comparison can also place classes from specified residuals into the same comparison.Source: Transporting coefficients and local… · pp. 93–94

Summary of the Chapter

  • The chapter summary gives a finite criterion for uniform invariance across adequate resolutions and states that canonical resolution is uniquely readable through every adequate resolution.It also summarizes that Condition C yields an isomorphism on H1 for diagnosis comparisons.Source: Summary of the Chapter · p. 94
  • A comparison map is needed when local regions are repartitioned; the chapter gives conditions for preserving obstruction classes and vanishing, and delimits when verdicts can be shared.Source: Summary of the Chapter · p. 94

Potential applications to code review

  • Code-review summaries can preserve diagnostic classes across splits and mergers when the code-to-model correspondence and comparison hypotheses hold; a vanishing diagnosis yields a correction under the chosen Laws and coefficients.Realizing that correction as an actual code change remains an application-time task.Source: Potential applications to code review · p. 95

Overview of the Chapter

  • Transport carries data, operations, and conditions across a change of reading; its universal property makes canonical unit and composition comparisons coherent, while edge reselection removes specified discrepancies exactly when all comparison diagrams can be made commutative.Source: Overview of the Chapter · p. 96

4.1 Characterizing transport by unique factorization

  • A transport morphism uniquely factors every further change; transports over the same base change are uniquely isomorphic, and identities and composites are strongly opcartesian.Source: §4.1 · p. 98

4.2 Constructing the core along an exact change

  • Under an exact change, the canonical core transport is strongly opcartesian and carries the extracted family, base object, and generated objects along the Atom bijection.For a change that enlarges extraction, additional operation, equation-system, and detector-soundness data yield a comparison with forward preservation on images of original objects.Source: §4.2 · pp. 99–100

4.3 Lifting the transport of the core to the geometry

  • For a geometry and core morphism, the local-realization comparison data exist exactly when a geometry morphism over that core morphism exists.Source: §4.3 · p. 101
  • The canonical core transport lifts to a strongly opcartesian geometry transport.Source: §4.3 · p. 102
  • For canonical core transport, the existence condition and universal property are constructed, and uniqueness of the factor follows from bijective comparisons and the identity coefficient map.For a general core morphism, Proposition 4.10 supplies the existence condition.Source: §4.3 · p. 102

4.4 Units, composition, and projections of transport

  • Transport induces functors between fibers, with coherent composition and unit comparisons, and is compatible with projection from geometries to cores.The comparison is a natural isomorphism, and the compatibility includes objects, morphisms, and composition comparisons.Source: §4.4 · pp. 102–104

4.5 The difference between specified and canonical comparisons

  • Finite comparison data assigns lifts to graph edges and specified fiber automorphisms to faces; the raw defect measures their difference from canonical comparisons.A raw defect is the identity exactly when the specified comparison agrees with the canonical one.Source: §4.5 · pp. 104–105

4.6 Removing discrepancies by reselecting edges

  • The obstruction orbit vanishes exactly when one edge reselection makes the specified comparisons canonical on all faces simultaneously.Changes at path ends depend on the current edge selection, so the criterion accounts for interactions among paths and faces.Source: §4.6 · pp. 106–107

4.7 Additional conditions for pasting faces

  • Coherent pastings require specified comparisons to agree along each chosen syzygy; otherwise a mismatch can obstruct overall coherence even when face comparisons are coherent.A later comparison conjugates an earlier defect, so pasted defects are not generally simple products of face defects.Source: §4.7 · p. 108

4.8 Removable and irremovable discrepancies

  • In S3, three specified comparisons can fail to cohere because the indirect route composes in the opposite order from the direct route, regardless of edge selection.Likewise, two faces sharing edges may each be coherent alone but not under one common selection.Source: §4.8 · p. 109

4.9 Achieving coherence of the core and the geometry with the same selection

  • The geometry-to-core setup lifts selected core changes to the geometry, then examines remaining geometric coherence conditions using that same selection.The specified comparisons in the geometry project to the specified comparisons of cores.Source: §4.9 · pp. 109–110
  • For an aligned edge section, the original defect factors into a core-visible lift followed by a core-invisible factor, and this order generally cannot be reversed.The geometry-side factor lifts the defect visible at the core; the remaining factor is invisible to the core.Source: §4.9 · pp. 110–111
  • Overall coherence requires lifting a core selection and correcting its lifted defect with kernel changes; independently coherent levels may still fail without a lift.The obstruction vanishes exactly when an aligned edge section permits the required kernel adjustments.Source: §4.9 · pp. 111–112

4.10 Carrying the reads and updates of a lens by the same map

  • For lenses, the same state map preserves reads and updates, and update preservation implies read preservation; invertible changes form a subgroup, while general morphisms can merge information.The example permits a non-injective semantics-preserving map that collapses a two-element complement to a singleton.Source: §4.10 · pp. 112–113

4.11 Carrying protocol operations and adapters

  • For protocols, preservation on each named operation determines a unique semantics-preserving morphism, and adapter preservation is expressed by commuting squares.Operations with different names remain distinct generating edges even when their actions coincide.Source: §4.11 · p. 114

4.12 Comparison of semantics and typed constructions

  • A fully faithful functor induces a group isomorphism on changes preserving a comparison, so invertible semantics-preserving changes of lenses and protocols are recovered exactly from their typed constructions.The result also applies to lenses whose views change, using the view map and the write map built from the state and view maps.Source: §4.12 · pp. 114–115

Summary of the Chapter

  • When an edge is shared across faces, a discrepancy absorbable on one independent edge must still be made coherent simultaneously across every face.The chapter summary connects this condition to vanishing of the obstruction for a family of transformations realizing the specified comparisons.Source: Summary of the Chapter · p. 116

Overview of the Chapter

The chapter develops normalization and comparison methods for transporting changes, diagnoses, and geometry across routes, and characterizes when changes preserve comparisons or can be lifted and restricted. It also classifies operation-preserving changes and develops a local reconstruction method that establishes an equivalence between full geometries and local models.

Overview of the Chapter

  • The chapter constructs the canonical comparison by matching original inputs to a selected target scope and pulling back objects, operations, and Laws along that correspondence.This recovers dependencies needed to check conditions that could be lost by extracting only the processing within one service.Source: Overview of the Chapter · p. 119

5.1 Constructing corresponding inputs by fiber products

  • A fiber product of exact doctrines gives corresponding inputs and is universal among exact cones; compatible selected sources make the same construction a fiber product in B.When distinct original sources map to the same target source, both remain as corresponding inputs.Source: §5.1 · pp. 120–121

5.2 Pulling back cores from the target

  • For any exact base morphism, backward reindexing gives a strongly cartesian lift, and the resulting pullback functor is coherent under identities and composition.Pullback is adjoint-equivalent to transport, with invertible unit and counit; even a non-invertible base map can induce equivalent fibers over selected sources.Source: §5.2 · p. 122

5.3 The canonical comparison exchanging transport and pullback

  • The canonical Beck–Chevalley mate is a natural isomorphism between the route that pulls back then transports and the route that transports then pulls back.It is choice-independent after aligning different pullback choices by unique lift comparisons; its invertibility follows from the invertible unit and counit of transport and pullback.Source: §5.3 · pp. 124–125
  • A specified comparison satisfies the canonical comparison equation exactly when it equals the canonical comparison; invertibility alone does not verify that the two routes are correctly matched.A mismatch may be an invertible automorphism, so route agreement and invertibility require separate checks.Source: §5.3 · p. 125

5.4 Existence of the constructions and the scope of finite presentation

  • With decidable Atom equality, an exact morphism is presentable by finite exception tables exactly when both endpoint source sets are finite and every target extraction set is finite or cofinite.The theorem permits rechoosing endpoint presentations; fullness for fixed codes is a separate question, and finite sources alone do not suffice.Source: §5.4 · pp. 126–127

5.5 Assembling commutative squares into whole diagrams

  • For a specified diagram, epis at the starts of its faces ensure that edge squares induce target path relations, but individual coherence does not require every vertex map to be epi.Agreement on the image of a non-epi map need not imply agreement elsewhere, although some diagrams remain coherent without epis.Source: §5.5 · p. 128

5.6 Carrying diagnoses and edge reselections back and forth

  • When the target diagram satisfies its path relations, transport preserves and reflects face coherence, the existence of a coherent edge reselection, and reselection-orbit membership.The correspondence also carries specified comparisons and reselections through vertexwise automorphism-group isomorphisms; the diagnosis concerns the fixed diagram and coefficient ring.Source: §5.6 · pp. 129–130

5.7 Conditions for backward transport along refinements

  • A pointed refinement admits a strongly cartesian lift for every target core exactly when it reflects extraction on the realized locus; this condition transfers across compatible base-change pairs and is closed under identities and composition.The realized-locus condition applies where a target core exists; if none exists, the lift criterion holds vacuously.Source: §5.7 · pp. 130–131
  • Backward transport can fail when a partial extraction omits a target Atom, but becomes possible when matched inputs are narrowed to all; an infinite selected family may preclude cores altogether.The infinite-family example satisfies the theorem’s conditions but has no cores, so it does not exhibit cores traveling back and forth.Source: §5.7 · p. 132

5.8 Comparisons including covers and local data

  • Pulling a geometry back along generated backward core transport yields a strongly cartesian morphism with respect to pref.The construction reindexes coverage, overlaps, coefficients, raw systems, support, axes, and observables; uniqueness follows from the generated inverses.Source: §5.8 · pp. 132–133
  • Two backward routes from the same geometry admit an invertible natural comparison whose coefficient component is the identity, and finite rooted diagrams inherit compatibility across edges and specified face comparisons.Under endpoint isomorphisms preserving components, comparison solutions transfer in both directions; arbitrary geometry morphisms need not support backward transfer.Source: §5.8 · pp. 134–135

5.9 Reading the exchange of order in lenses and protocols

  • Lens restrictions to a selected view remain total and preserve lens isomorphisms, while protocol restrictions preserve semantics-preserving adapters, comparison triangles, and commutative adapter squares.Lens semantics alone do not determine covers or local data, and coherence involving operations outside a protocol selection must be checked separately.Source: §5.9 · pp. 135–137

5.10 The generated comparison including the two routes and normalization

  • A diagnosis-selected normalization can be incorporated into the route comparison when it preserves core structure, producing a generated comparison that may discard distinctions among representations.The normalization is idempotent and preserves configurations; its conditions include unchanged residuals, operation types, invariants, and signature-axis coordinates.Source: §5.10 · pp. 137–138
  • For the two geometry routes, the canonical comparison is invertible and projects compatibly to the comparison of cores.The construction uses an exact pointed pullback square, a finite comparison diagram, a cochain, coefficients, and an original geometry; its geometry-level units and counits are invertible.Source: §5.10 · p. 137

Summary of the Chapter

  • Chapter 5 establishes exact-base transport and pullback equivalence, diagram-level preservation and reflection of defects and reselection, a realized-locus criterion for backward transport, and route comparisons for geometries, lenses, and protocols.Along exact base morphisms the Beck–Chevalley mate is invertible; aligned diagrams also distinguish relations cancellable by epis from individually imposed relations.Source: Summary of the Chapter · p. 140

5.10 The generated comparison including the two routes and normalization

  • The generated comparison β = Eα composes the canonical route comparison with diagnosis-selected normalization and is compatible with projection when the same normalization is used for geometries and cores.The following chapter studies idempotence of the normalization morphisms and the generated comparison’s invertibility and image.Source: §5.10 · p. 140, Summary of the Chapter · p. 141

Overview of the Chapter

  • This chapter asks what a comparison retains after diagnosis-selected normalization and whether the original can be recovered, distinguishing idempotence from invertibility.The generated comparison is β = Eα, where E is the selected normalization and α is the canonical comparison between the two routes.Source: Overview of the Chapter · p. 142

6.1 Selecting one representation for each configuration

  • For any readout unchanged by normalization, there is a unique factorization through configurations, and the normalization’s fixed points correspond bijectively to configurations.The quotient of architecture objects by having the same configuration is also isomorphic to the collection of configurations.Source: §6.1 · p. 144

6.2 Lifting object normalization to a structure-preserving idempotent

  • If Ad(P) holds, normalization lifts to an idempotent structure-preserving endomorphism of a core, but it is noninvertible and does not split within the category of cores.Distinct architecture objects can represent the same configuration, so object normalization is not injective; the core contains more than the configurations alone.Source: §6.2 · pp. 145–146

6.3 Making the remaining information into objects by idempotent completion

  • In the idempotent completion, a normalized comparison is an isomorphism between the images, while it is invertible in the original category exactly when the normalization is the identity.Conjugating the target idempotent along the canonical isomorphism gives the source idempotent; the same generated comparison induces the isomorphism of images.Source: §6.3 · p. 147
  • A morphism that is not invertible between original objects can induce an isomorphism between their normalized images using that same morphism.The objects and their identity morphisms change under normalization; the comparison morphism does not.Source: §6.3 · p. 148

6.4 Classifying the generated comparisons of full geometries

  • For full geometries with admissible cores, normalization is idempotent, and generated transport and pullback along exact base morphisms preserve admissibility and commute with normalization.The commutation applies to transports and pullbacks generated from the same reindexing.Source: §6.4 · pp. 148–149

Then d

  • The generated comparison is invertible exactly when d is the identity, equivalently when χ does not hold; when normalization is selected, it is an isomorphism between the normalized images.Projecting that isomorphism of geometry images to cores yields the corresponding isomorphism of core images.Source: Then d · pp. 150–151

6.5 Collecting normalized objects and changes into a single category

  • Normalized cores form a category fully faithfully embedded in the Karoubi completion, and the normalization functor from admissible cores is full.Its morphisms are the original morphisms satisfying the normalization compatibility condition.Source: §6.5 · p. 153
  • Normalization extends to full geometries via a full functor compatible with projection to cores, while leaving a morphism’s base and coefficient homomorphism unchanged.The normalized geometry morphisms satisfy the corresponding compatibility condition with the endpoint normalizations.Source: §6.5 · p. 153

6.6 Conditions for interchanging the order of a normalization and a change

  • For admissible cores, interchanging a change and normalization is equivalent to agreement of their operation components after normalization.The criterion compares operations themselves, not only their actions on configurations.Source: §6.6 · pp. 154–155
  • An operation tag can make the order matter even when configuration actions agree, and normalization can send distinct morphisms to the same morphism, so it need not be faithful.In the example, normalizing then applying the change yields tag 0, whereas applying the change then normalizing yields tag 1.Source: §6.6 · pp. 155–156
  • Interchanging a change with normalization requires checking the correspondence of operations, since original-representation-dependent operation specifications can differ despite matching normalized operations.The design review must check condition (6.36) in addition to correspondence of objects.Source: §6.6 · p. 156, Summary of the Chapter · p. 160

6.7 The category of comparisons themselves and the three-level projections

  • Idempotent completion commutes up to natural equivalence with forming the category of comparisons, compatibly with projections to extraction, core, and geometry.A comparison between idempotent images is formed by applying the endpoint idempotents to the original comparison; it need not equal that original comparison.Source: §6.7 · pp. 156–157, Figure 6.1 · p. 157, Summary of the Chapter · p. 161

6.8 What remains in the image for lenses and protocols

  • Fixed-view lens idempotents split within the same category, while protocol images retain executions and observations when the idempotent adapter preserves both.An idempotent state map alone is insufficient for protocols: it must commute with executions so that fixed points remain closed under them.Source: §6.8 · pp. 158, 160, Summary of the Chapter · p. 161

Summary of the Chapter

  • A generated comparison is invertible exactly when its normalization factor is the identity, although it still induces an isomorphism between the images when normalization is nontrivial.The normalization map retains fixed-point configurations, and readouts unchanged by normalization factor through them; normalized objects and morphisms form a category with a full normalization functor.Source: Summary of the Chapter · p. 160

Overview of the Chapter

  • The chapter distinguishes testing whether a change preserves a comparison from constructing a compatible detailed change, and classifies compatible options by a group action.For AAT normalization, compatible changes can sometimes be constructed even when deciding whether a given change is compatible requires information lost during normalization.Source: Overview of the Chapter · p. 163

7.1 Changes preserving a single comparison

  • Matching call relations and visible behavior can conceal broken data preservation; compatible changes form a group identified, with full endpoint automorphisms, as comparison automorphisms.The shipping-address refactoring example shows that the payment category can change despite matching operation structure, so the carried-over data conditions must also be checked.Source: §7.1 · pp. 164–165
  • For a comparison c, the projection kernels are the changes fixing c at either endpoint, and following candidates exist exactly over the projection image; an isomorphism comparison identifies both endpoints by conjugation.When a following candidate exists, all candidates at that endpoint are obtained by composing it with the corresponding kernel subgroup.Source: §7.1 · p. 166

7.2 Carrying changes from the same generator

  • Changes carried from the same generator are compatible, while differences between independently chosen changes must lie in J; regeneration from an isomorphic input presentation preserves the comparison-preserving groups and candidate changes.Once a change on one side is fixed, the usable source changes on the other side are Ja.Source: §7.2 · p. 167

7.3 Conditions for distinguishing by observation

  • Compatibility is determined by observation exactly when every observation-invisible change is compatible (K⊆Γ); for coefficient-only observation across an isomorphism, this reduces to KY={1}.The remaining ambiguity is represented by the pointed coset set K/L, which is a single point precisely under the determination condition.Source: §7.3 · pp. 168–169

7.4 Restriction to the normalization, reflection, and lifting

  • Core normalization preserves arbitrary comparisons; for r(Γ0)⊆∆, a compatible lift of δ∈∆ exists exactly when δ∈r(Γ0), and all such lifts form a right-multiplication torsor under L=ker(r restricted to Γ0).Examples show lifts can exist even when reflection fails, while an image exchange can have no lift inside the centralizer group.Source: §7.4 · pp. 170–172

7.5 Constructing lifts for full geometries

  • For full geometries satisfying Ad(P), normalization preserves residual equation and invariant/signature coordinates and operation configuration maps; changes on the normalized image can extend consistently to the original objects.The stated assumption requires the core to satisfy Ad(P).Source: §7.5 · p. 172

Carrying the data accompanying an object

  • The extension represents objects as configurations paired with accompanying data and combines exchanges before and after configuration transport so selected objects map to selected targets.The construction uses the Atom component of the normalized-image automorphism to transport the configuration.Source: Carrying the data accompanying an object · p. 173
  • Changes carrying an object’s accompanying data preserve object formation, and the induced action on all such data preserves identities and composition.This yields a group-homomorphism lift for self-maps of Atoms.Source: Carrying the data accompanying an object · p. 173

Extending the components of the operations and of the geometry

  • For each full geometry, automorphisms of its normalized image admit a group-homomorphic lift that preserves base and coefficients and commutes with normalization.The lift satisfies SG(NG) = 1G and SG(f)NG = NGSG(f) = f.Source: Extending the components of the… · pp. 173–174

Combining the two endpoints so as to preserve the comparison

  • An isomorphism comparison admits a section built by lifting one endpoint and defining the other by conjugation, preserving the comparison and endpoint base and coefficient components.The section is a group homomorphism.Source: Combining the two endpoints so as to… · pp. 174–175

7.6 Information remaining in a generated comparison, and all the lifts

  • For a generated comparison, normalization has a section, compatible lifts form a right torsor under the kernel, and incompatible changes can share the same normalized value.This also holds for base-fixing groups; on centralizer groups, preserving the normalized comparison is equivalent to preserving it before normalization, though normalization forgets some compatibility information. For the diagnosis-selected normalization, a section exists, but preservation need not be reflected.Source: §7.6 · pp. 176–177

7.7 Classification of changes by the connections of operations

  • Operation-preserving changes following a fixed visible change correspond to one permutation per connected component of the operation graph, with the same permutation required at both ends of every edge.Their projection to visible changes splits, and each fiber is a right torsor under the kernel; fixing selected states restricts the permutations to those fixing the selected value.Source: §7.7 · pp. 178–179

7.8 Consequences for lenses and protocols

  • A state correspondence between refactored systems must preserve reads and commute with named operations; relative to one compatible correspondence, alternatives are classified by automorphisms preserving those structures.The correspondence satisfies g′h = g and hTe = T′eh.Source: §7.8 · p. 180

Lenses: the total update ties all the views together

  • For a total lens, the view-update graph is connected, so every visible change has |KL|! invertible lens changes following it, forming a direct-product classification.Preserving a selected section corresponds to the selected-state version of the classification.Source: Lenses: the total update ties all the… · pp. 180–181
  • Lens updates force correspondence choices across views to agree, while protocol changes remain independent across disconnected operation components.In the shipping-address example, four correspondences preserve display and the unset payment value, but only two preserve updates; in the worker example, the 16 control-point correspondences narrow to four that preserve context handoff.Source: Lenses: the total update ties all the… · p. 181, Summary of the Chapter · pp. 184–185

Protocols: independent changes remain on independent components

  • With identity transitions on a finite protocol graph, realizations satisfy the path equations, and operation-preserving changes follow the split short exact sequence, section, and kernel torsor classification.When two same-role workers are exchanged, their component kernel is S2 × S2 and the full change group is (S2 × S2) ⋊ S2, of order 8.Source: Protocols: independent changes remain… · pp. 181–183

Connection with the comparison-preserving group

  • Typed operation and observation equations identify semantics-preserving automorphisms and comparison-preserving endpoint pairs with their typed counterparts, including projections, kernels, and lift torsors.The total update links lens views, whereas independent workers retain separate changes; both cases arise from the same connected-component theorem with different operation inputs.Source: Connection with the… · p. 183

Summary of the Chapter

  • For a single comparison, compatible endpoint changes satisfy vc = cu; a section, kernel, and kernel torsors describe compatible lifts and their freedom.Compatibility is determinable from observation alone exactly when ker O ⊆ Γ; canonical normalization can construct a section, though normalized values need not determine compatibility of a given change.Source: Summary of the Chapter · pp. 183–184

Overview of the Chapter

  • The main theorem makes the category of full geometries and all structure-preserving morphisms equivalent to local models reconstructed from primitive data and compatibility conditions.The chapter frames reconstruction as separation, assembly of morphisms, and assembly of objects; local readouts include types, operations, Laws, geometry, and realization.Source: Overview of the Chapter · pp. 186–187
  • For finite descriptions, operation Laws can uniquely extend an overall morphism from a finite table; finite-model checking separates sufficient readout information from computational cost.The chapter also constructs models and changes from divided descriptions, illustrated by teams aligning shared transactions, amounts, completion conditions, operations, and Laws.Source: Overview of the Chapter · pp. 186–187

8.1 Recovery of objects and morphisms by finite presentation

  • For fixed endpoint presentations, finite exception codes make explicit that not every semantic morphism is presentable between those endpoints.The code records a default value in {0, 1} and a finite exception set; its default distinguishes finite-set from cofinite-set characteristic functions.Source: §8.1 · p. 188, Finite exception tables and the… · p. 188

Finite exception tables and the one-point compactification

  • Finite exception codes represent continuous {0, 1}-valued functions on the one-point compactification D+; on infinite D codes are unique from their evaluations, while finite D admits two codes per function.The chapter’s finite-presentation characterization requires finite sources at both ends and continuous extensions of target extraction predicates; finite discrete sources are exactly compact ones.Source: Finite exception tables and the… · pp. 188–189

Morphisms between fixed presentations

  • A semantic morphism between fixed presentations is presentable only when its normalized default values agree at corresponding sources.For finite Atom sets, zero-default normalization makes D0 fully faithful, and D0Rfin is isomorphic to D0 while preserving semantic objects and morphisms. A finite example shows that equal meanings alone do not ensure presentability.Source: Morphisms between fixed presentations · pp. 189–190

8.2 Compatibility of finite fragments and gluing

Indices and restrictions of the readout

  • A table over finite subsets is equivalent to a compatible family of fragments, since each item’s value is fixed by its single-point fragment.Restriction and reconstruction from single-point fragments are inverse operations.Source: Indices and restrictions of the readout · p. 191

Representation by graphs of typed functions

  • Typed functions correspond one-to-one with Boolean graphs having exactly one output per input, and this correspondence preserves identities and composition.Finite-support evaluation formulas express local conditions, but requirements such as totality quantify over inputs and need not be finitely checkable.Source: Representation by graphs of typed… · pp. 191–192

8.3 Reconstruction principle by separation and assembly

  • Separation and assembly of morphisms and objects make the local readout functor an equivalence of categories, with exactly one overall morphism for each local morphism.The conditions are injectivity on morphisms with fixed endpoints, construction of a morphism from every local morphism, and construction of an overall object isomorphic under readout to every local object.Source: §8.3 · p. 192

The category of realizations and the variants of morphisms

  • Full-geometry morphisms have representative and explicit-map variants, both allowing noninvertible maps on the base, architecture objects, and coefficients.The representative variant requires equality after transport; the explicit-map variant instead records concrete bijections and preservation of evaluations, relations, restrictions, and readouts.Source: The category of realizations and the… · pp. 193–194

Primitive data and local compatibility conditions

  • Local objects and morphisms read primitive data as values or function-graph entries, then require compatible fragments satisfying structural laws and preservation conditions.The object conditions include finite selected Atom families; morphism conditions include totality and uniqueness, endpoint agreement, ring-homomorphism laws, preservation of Law evaluations, and naturality.Source: Primitive data and local compatibility… · pp. 194–195
  • The local objects and morphisms form a category MΘ, and reading primitive data defines a functor.Source: Primitive data and local compatibility… · p. 196

8.5 The local reconstruction theorem for full geometries

Assembly of full geometries

  • Assembly builds full geometries in dependency order, recovering each structure and yielding a canonical isomorphism, while morphisms are recovered exactly.The readout and assembly between local morphisms and full-geometry morphisms are mutually inverse.Source: Assembly of full geometries · pp. 197–198

The main theorem

This section reconstructs geometries and their structure-preserving morphisms from local descriptions, identifying full geometries with their local models up to categorical equivalence. It also treats unique extension of morphisms from selected finite tables and distinguishes finite-model reconstruction and checking from limitations involving infinite objects or readouts.

The main theorem

  • The primitive readout gives an equivalence between full geometries and local models, recovering objects up to isomorphism and all structure-preserving morphisms between fixed endpoints uniquely.The Hom-sets include the noninvertible morphisms permitted by the chosen variant.Source: The main theorem · p. 198

Modernization of an intrabank transfer system

  • In the transfer example, a design change is compatible when team correspondences form an overall structure-preserving morphism; Theorem 8.18 reconstructs that morphism uniquely.A completed transfer must have corresponding debit, credit, and journal entries; proposals can be compared by checking whether their local correspondences satisfy preservation conditions.Source: Modernization of an intrabank transfer… · pp. 200–202

Application to normalization and generated comparisons

  • Theorem 8.18 reconstructs tagged-operation automorphisms and generated route comparisons, including nontrivial idempotent normalization with noninvertible β, while an identity cochain gives β = α.Reading the tag distinguishes morphisms with equal configuration actions.Source: Application to normalization and… · p. 202

8.7 Application of the reconstruction principle to the semantics of CS

  • The reconstruction principle is applied to lenses and protocols with observations, recovering objects and general morphisms from primitive data, preservation conditions, and their respective laws.The constructions use a finite reference fiber for lenses or a table of generating edges for protocols.Source: §8.7 · p. 203

Local models and assembly

  • Local assembly reconstructs lenses and protocols with observations, yielding categorical equivalences that recover objects up to isomorphism and morphisms, including noninvertible ones.Lens models impose the three lens laws and a finite reference fiber; protocol models require finite state sets, path relations, and natural observations.Source: Local models and assembly · pp. 204–205

Reconstruction of lenses from the reference fiber

Reconstruction of protocols from the generating edges

  • For protocols, vertex tables extend uniquely to a general morphism exactly when they preserve observations and satisfy naturality at generating edges.Observation preservation is required even at isolated vertices; observations alone do not detect every difference in edge actions.Source: Reconstruction of protocols from the… · pp. 206–207

Compatibility of finite presentations with the primitive readout

  • For lenses and protocols, finite decoding presentations are equivalent to their realization categories and compatible with the primitive readout; these equivalences extend to idempotent completions, arrows, and comparison squares.The decoded presentations agree with direct readout up to natural isomorphism, including on general morphisms.Source: Compatibility of finite presentations… · pp. 207–208

Resource constraints of implementations and finiteness of models

  • Fixed storage bounds the number of storable states, but reconstruction from finite tables also requires specifying the model’s types, coefficients, contexts, and readout range.The account distinguishes tabulating all required items from recovering omitted components by laws.Source: Resource constraints of… · p. 209

The overall table and partial readouts

  • When all required readout items are indexed by a finite set and finitely encodable, compatible fragments recover the overall table; partial readouts may leave candidates indistinguishable.In the transfer example, reading only completion and journal-entry indicators leaves two candidates indistinguishable, while debit and credit records distinguish them.Source: The overall table and partial readouts · p. 209

Finite checking procedures and computational cost

  • Finite checking is decidable when tables and conditions are finitely enumerable and evaluation and equality decisions are computable, but reconstruction gives no resource-cost bounds.Termination in finitely many steps does not establish execution within given time or memory limits.Source: Finite checking procedures and… · p. 210

Limits of presentation by a countable syntax

Summary of the Chapter

  • The main theorem gives an equivalence recovering geometries up to isomorphism and all structure-preserving morphisms, including noninvertible ones, while preserving identities and composition.It applies to the chosen variant of the primitive data, Laws, local geometry, and realization.Source: Summary of the Chapter · p. 212

R.1 Semantics of specifications and architecture

This section presents AAT’s common framework for readings of Atoms and Laws, connecting geometry with local consistency, diagnosis, transport, comparison, reconstruction, and structure-preserving changes. It also frames development-practice questions through change classification and reconstruction, and records the correspondence of the paper’s definitions, constructions, and results to Lean declarations and the versions used for formalization.

R.1 Semantics of specifications and architecture

  • AAT turns a reading of Atoms and Laws into a geometry whose lawful locus expresses satisfaction, and encodes lens and protocol semantics with corresponding laws and semantics-preserving morphisms.The construction proceeds through cores closed under operations, then geometries equipped with sites and coefficients.Source: §R.1 · pp. 214–215, Conclusions · p. 220

R.2 Local consistency and cohomological obstructions

  • Under torsor, equivariance, and sheaf conditions, vanishing of the specified obstruction yields a global repair; comparison of coefficients links equation-based obstructions with semantic repairs.The conclusions state that vanishing of the first obstruction class is equivalent to a global state under the stated torsor and sheaf conditions.Source: §R.2 · p. 215, Conclusions · p. 220

R.3 Abstraction and preservation of information

  • AAT characterizes the coarsest reading preserving Law values exactly and gives conditions for diagnosis invariance, including a finite test for uniform invariance and an observation-kernel criterion for judging comparison preservation.Under Condition C, the comparison map is an isomorphism on first cohomology; membership in the comparison-preserving subgroup is determined by observations exactly when ker O is contained in that subgroup.Source: §R.3 · p. 216, Conclusions · p. 220

R.4 Transport and base change

  • Exact changes of reading induce transport and core pullback by adjoint equivalence, while generated comparisons factor into an invertible map and an idempotent normalization.For exact pointed pullback squares, transport and base change commute up to an invertible canonical comparison.Source: §R.4 · p. 217, Conclusions · p. 221

R.5 Lenses, updates, and comparison-preserving changes

  • AAT describes get-and-put-preserving lens morphisms through maps of reference fibers and classifies comparison-preserving changes by how operations connect hidden states.For operations that keep hidden states unchanged, the changes are indexed by connected components and related to visible changes by a split short exact sequence; protocol components can be changed independently.Source: §R.5 · p. 218, Conclusions · p. 221

R.6 Presentation and local reconstruction

  • AAT proves an equivalence between full geometries and local models, recovering objects up to isomorphism and structure-preserving morphisms from independently defined local data and compatibility conditions.For lenses and protocols, the framework also gives unique extensions from finite tables.Source: §R.6 · p. 218, Conclusions · p. 221

R.7 Situating AAT

  • AAT connects its constructions as theorems about common objects, presenting its approach as foundations that treat individual problems as cases of shared constructions.The conclusions group the results around foundational geometry, obstructions, diagnosis, transport, comparison, and reconstruction.Source: §R.7 · p. 219, Conclusions · p. 222

Further directions

  • Further directions include unifying reconstruction with comparison groups and finite determinacy, studying descent for families and representability, and connecting the framework to time-dependent structure and software measurements.The proposed measurement connection would require verifiable conditions on extracted observations and computed diagnoses.Source: Further directions · pp. 222–223
  • The paper proposes using change classification and reconstruction to model software evolution as motion among realizations and study which practices widen or narrow reachable designs.The Rising Sea approach extends this foundation by turning development-practice problems into theorems and, ultimately, measurements as the theory develops.Source: Further directions · p. 224

Correspondence with the Lean Formalization

  • The appendix links Lean declarations to the paper’s definitions, constructions, and results, recording relevant text locations and the conditions under which applications hold.Each link points to a definition and proof.Source: Correspondence with the Lean… · p. 228
  • The AAT Lean sources use fixed commits for general transport, lenses, base change, and comparison groups, and specify the Mathlib and Lean versions.The listed commits are 7e68ec6e77ef for those groups and 719f81f47d41 for the other declarations; Mathlib is 8f9d9cff6bd7 and Lean is v4.28.0.Source: Correspondence with the Lean… · p. 228

A.1 Chapter 1: Construction of Relative Architecture

This section develops the foundations of relative architectures, covering generated cores, local-law and Čech methods for global consistency and repair, diagnostic comparison, transport, normalization, and coherence. It also treats semantics-preserving encodings and operation-preserving changes, including reconstruction of geometries and morphisms from local tables under stated conditions, while noting limits of finite presentations and readouts for infinitely indexed families.

A.1 Chapter 1: Construction of Relative Architecture

  • Under soundness and required completeness, an object is equation-lawful exactly when no required equation circuit matches and is accepted.The circuit reading uses signed query sequences and finite detector syntax.Source: §A.1 · p. 229
  • A core generated from a finite extracted family satisfies a minimality principle: an algebra object is nonempty exactly when it is reachable by finite operation sequences.The construction uses a family-preserving composition and a configuration-preserving object reading.Source: §A.1 · pp. 229–230
  • Admissible presieves generate a Grothendieck topology, and set-valued presheaf sheafification has an adjunction with unique extensions.The sheaf condition identifies matching families on covers with the presieve condition.Source: §A.1 · p. 230
  • Base change transports raw quotient presentations by applying the coefficient map to generating relations and restrictions, coherently with identities and composition.The source map may be general while the Atom map is an equivalence; the construction commutes with normalization and extraction.Source: §A.1 · pp. 230–231
  • Lens and protocol semantics-preserving morphisms correspond mutually inversely to typed morphisms, preserving naming and role components.For protocols, naturality on paths follows from commutativity on edges, and restriction to components is inverse to the construction.Source: §A.1 · p. 232

Aggregation, source maps, and concrete lens examples

A.2 Chapter 2: Geometry of Laws and Local Consistency

  • Coordinate values satisfying structural relations are naturally in bijection with algebra homomorphisms out of the quotient by those relations.The presentation divides the polynomial ring in typed coordinates by the ideal generated by structural relations.Source: §A.2 · p. 233
  • Restriction composition makes the three-term Čech complex satisfy d1d0 = 0, and affine coefficient lifts yield a residual cocycle class independent of the lift choice.Freeness gives the cocycle, while transitivity makes the difference between choices a coboundary.Source: §A.2 · p. 234
  • An actual coefficient isomorphism induces isomorphisms of complexes and H1, while changing atlas choices changes the comparison by a coboundary.The accompanying theorem relates the coefficient comparison and residual to the cohomology classes.Source: §A.2 · p. 237
  • For SAGA inputs with the actual state sheaf and normalized empty intersections, a global repair exists exactly when the specified obstruction class vanishes.The result identifies global repair existence with vanishing of that class.Source: §A.2 · p. 237

Restriction of ideals, dimension lower bounds, and obstruction classes

  • Restriction preserves witness and obstruction ideals, while local-state mismatch classes agree with the obstruction class and remain invariant under correction of local states.An example establishes nonvanishing of the specified obstruction class with integer coefficients.Source: Restriction of ideals, dimension lower… · p. 237

A.3 Chapter 3: Canonical Resolution and Diagnostic Invariance

  • The joint-kernel reading is adequate and universal: every adequate reading factors uniquely through the quotient defined by agreement of all Laws.A finite-table partition agrees with the joint kernel; the chapter also gives presentable and non-presentable candidate families.Source: §A.3 · p. 238
  • Under Conditions C0–C6, the generated comparison map on H1 is bijective through its Law-value block decomposition and naturality.The construction uses connected fibers and a rational chain condition to produce primitives that kill cocycles on internal edges.Source: §A.3 · p. 239
  • Uniform invariance holds exactly when every nonempty subnerve has bijective H1 comparison, equivalently zero defect, and can be checked using rational matrices.Condition C on every nonempty subset is sufficient for uniform invariance.Source: §A.3 · p. 240
  • The actual mismatch of local data equals the independently generated diagnostic mismatch at the cochain level, and the equality descends to H1.The theorem compares the actual Čech and diagnostic mismatch classes.Source: §A.3 · p. 241
  • Diagnostic vanishing agrees with actual vanishing: adequacy and relation-connectedness construct an integer primitive, while the diagnostic comparison is bijective and reflects zero classes.The comparison square links actual and diagnostic H1 maps; the integer-primitive construction applies to the specified class.Source: §A.3 · pp. 241–242

Refinements, uniform invariance, and concrete examples of obstruction classes

  • T3 is uniform while T6 is not, and the examples compare four coarse- and fine-side vanishing conditions with both zero and nonzero outcomes.The uniformity result excludes Obs_loc from the objects; the specified refinement also has Condition C and a bijective comparison map.Source: Refinements, uniform invariance, and… · p. 242

A.4 Chapter 4: Transport and Coherence of Composition

  • Exact subsequent morphisms admit unique transport factors, and canonical core and geometry transport satisfy the strongly cocartesian universal property.The construction supplies the factor and proves uniqueness of its components; the geometric theorem also constructs the three canonical comparisons.Source: §A.4 · pp. 243–244
  • The typed AAT construction for relative lenses is fully faithful and matches comparison groups and the source projection; lens morphisms preserve reads when they preserve updates.The invertible relative lens morphisms form the put-preserving subgroup, which is contained strictly in the get-preserving group in the Bool example.Source: §A.4 · pp. 245–246

Canonical transport and coherence over the core

  • For selected strong lifts, fiber transport has coherent composition and unit isomorphisms, while obstruction vanishing is equivalent to reselection making all faces coherent.Two-step defects include conjugation by the later specified comparison; the vanishing criterion applies to the same comparison diagram over an arbitrary functor.Source: §A.4 · p. 245, Canonical transport and coherence over… · p. 247
  • In a two-level diagram, geometry mismatch decomposes into a kernel factor and a lifted outer factor, with kernel reselection characterizing geometric coherence.The outer factor projects to the core's raw defect; under a fixed edge section, inner-obstruction vanishing is equivalent to geometry coherence.Source: Canonical transport and coherence over… · pp. 248–249

A.5 Chapter 5: Base Change and Generated Comparisons

  • Exact doctrine cospans yield pullbacks, and compatible designated points admit a unique pointed lift.The pullback construction does not assume finiteness or a presentation by codes.Source: §A.5 · p. 249
  • From a semantic exact hom and target CoreFiber, the inverse core construction transports the extracted family backward and builds a covering core morphism.The constructed core includes operations, equations, invariants, and a signature.Source: §A.5 · p. 250
  • Exact semantic transport gives category equivalences and strong cartesian lifts; the canonical Beck–Chevalley mate is invertible, and its lift triangle characterizes the specified comparison.The equivalence requires neither injectivity nor surjectivity of the source map; the lift-triangle condition is equivalent to equality with the canonical mate.Source: §A.5 · pp. 250–251
  • With decidable Atom equality, finite Sources at both ends and finite-or-cofinite target extractions characterize presentability up to endpoint isomorphism.The result constructs equality of extraction codes on sources in the normalization image.Source: §A.5 · p. 251
  • For indexed diagrams, face relations descend along epi index morphisms, and uniform cancellation for arbitrary parallel morphisms holds exactly for epis.The finite inclusion Fin 1 → Fin 2 selecting 0 is not epi: identity and constant-at-0 maps differ but agree after composition with it.Source: §A.5 · p. 252
  • Indexed transport preserves and reflects coherence, obstruction-class vanishing, and edge-reselection orbits, while carrying package-fiber automorphisms by group isomorphism.Reselections can also be transported in reverse.Source: §A.5 · pp. 252–253
  • Reflection of extraction on realizable sources is equivalent to strong cartesian lifts to every target core; compatible refinement regimes exist exactly under the corresponding reflection condition and are closed under identity and composition.Source: §A.5 · p. 253

Reindexing and coherence of canonical lifts

A.6 Chapter 6: Idempotent Normalization and Realization

  • Normalization fixes exactly the selected objects, identifies configurations with those fixed points, and factors every map invariant under normalization uniquely through the configuration.The total normalization is idempotent as a morphism.Source: §A.6 · p. 256
  • Normalization is generally noninvertible and not an internal split, but its transport and pullback lifts preserve it, and generated comparisons admit aligned idempotents and Karoubi isomorphisms.The generated comparison is invertible exactly in the selected case.Source: §A.6 · pp. 257–259
  • The normalization retraction is natural at a morphism exactly when operation normalization is coherent, while Karoubi(Arrow E) is equivalent to Arrow(Karoubi E).The equivalence is natural with respect to functors and coherent with composition.Source: §A.6 · p. 260

Splitting of idempotents for lenses and in the Karoubi category

  • Idempotents split in arbitrary Karoubi categories, and lens-realization idempotents split by fixed states closed under put that preserve the lens laws and finite reference fibers.No idempotent-completeness assumption on the original category is needed for the Karoubi construction.Source: Splitting of idempotents for lenses… · p. 261

A.7 Chapter 7: Comparison-Preserving Changes and Information

  • Comparison-group projection kernels are opposite stabilizers and nonempty fibers are stabilizer torsors; when conjugation matches endpoint subgroups, the comparison group is their graph.For a fixed compatible generated input, intertwining along both routes is equivalent to the difference of changes lying in the pulled stabilizer kernel.Source: §A.7 · pp. 262–263
  • An observation predicate exists exactly when ker O ≤ Γ, and observation fibers are left cosets; the saturation is O^-1(OΓ) = Γ ker O without requiring surjectivity or normality.The coset results also characterize when a coset inside the kernel is a singleton.Source: §A.7 · p. 264
  • For a group homomorphism, reflection is equivalent to kernel inclusion plus the image-range condition; the restricted fiber action is free and transitive, and short exactness is equivalent to surjectivity.Source: §A.7 · p. 265
  • For comparisons generated by semantic squares, admissible source cores yield sections, split short exact sequences, torsor fibers, and non-identifiability; restriction reflects compatibility exactly when normalization is not selected.These results cover both full and base-fixing endpoint groups.Source: §A.7 · pp. 266–267
  • For arbitrary graphs and hidden types, operation-preserving following changes correspond to hidden permutations per connected component; identity-protocol adapters also preserve the group product and componentwise equations.Finiteness is not required for the graph correspondence.Source: §A.7 · pp. 267–268

Presentation changes, comparison groups, and finite examples

  • Presentation changes preserve observation kernels, compatible kernels, pointed cosets, and compatibility predicates; following pairs form a split short exact sequence with kernel-torsor fibers.The reindexing formula applies to arbitrary permitted subgroups, without a finiteness assumption; a Fin 3 example shows reflection can fail after restriction.Source: Presentation changes, comparison… · pp. 268–269
  • Changes preserving a selected section form a semidirect product of componentwise point-fixing permutations; the two-worker full change group has order eight.The visible worker exchange swaps the two hidden-permutation factors.Source: Presentation changes, comparison… · pp. 270–271
  • Operation-preserving changes correspond to hidden permutations and section-preserving changes, extending from product lenses to general total lenses.For two workers, 16 candidates follow the control-point readout for each of the identity change and session swap, while 4 changes preserve the operations as well.Source: Presentation changes, comparison… · pp. 270–271

A.8 Chapter 8: Presentation and Local Reconstruction

  • Finite-Atom predicate codes correspond to continuous maps from OnePoint, and default normalization gives a fully faithful decoder on false-default codes.Evaluation is injective for infinite Atoms; over finite Atoms, each predicate's code fiber is Bool.Source: §A.8 · pp. 272–273
  • Arbitrary functions correspond to typed total functional Bool tables, with relational table composition matching function composition.Compatible finite restrictions glue, but compatibility alone does not ensure totality or functionality.Source: §A.8 · pp. 273–274
  • The local graph category is equivalent to the category of realizations, reconstructing all morphisms, including non-invertible ones.For arbitrary functors, separation of Homs, agreement after assembly, and an assembly isomorphism yield fullness, faithfulness, and essential surjectivity.Source: §A.8 · pp. 274, 276
  • Primitive tables reconstruct lens and protocol semantics, preserving semantic morphisms and extending generating-edge naturality to paths and declared relations.The resulting equivalences preserve identities, composition, and primitive evaluation, and reflect isomorphisms.Source: §A.8 · pp. 277–278
  • Lens maps extend uniquely from a reference fiber without finiteness or invertibility assumptions; lens and protocol realization categories also admit Karoubi reconstruction, while countable decoders need not be surjective.With Nat Atoms, Nat subsets inject into semantic automorphisms, but there is no surjection from arbitrary countable syntax or finite-list syntax onto that automorphism group.Source: §A.8 · pp. 278–279

Covers, finite presentations, and infinitely indexed families

  • For finite sources, anchored coverage exists exactly when target extractions extend continuously to OnePoint → Bool; for discrete sources, finiteness is equivalent to compactness.When the index set is finite, gluing finite fragments recovers the whole table.Source: Covers, finite presentations, and… · p. 280
  • The five-factor and generated comparisons, together with both projectors, are recovered as the same morphisms in the reconstruction.The three-axis example selects normalization for a nonidentity defect and identity for the identity cochain.Source: Covers, finite presentations, and… · p. 281
  • Global Bool families are isomorphic as additive groups to compatible finite fragments, but finite readouts do not separate abstract families when the index set is infinite.A family true at a point outside a given finite subset has the same readout there as the zero family.Source: Covers, finite presentations, and… · pp. 281–282

Repository and Lean Build

  • The appendices give pinned Lean build instructions for the Formal and Research proof sources, including targets for transport, lenses, base change, and comparison groups.The listed proof sources use specified repository revisions and dependencies.Source: Repository and Lean Build · pp. 283–284

Disclosure of AI Use

  • The author led the research and retained responsibility for the manuscript; AI systems were used to construct the theory, formalize and prove theorems, draft the manuscript, and review it.The text maps propositions to Lean declarations and identifies the fixed proof-source version and build procedure.Source: Disclosure of AI Use · p. 285
Loading 2609.27638v1…