Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

The concrete two-sided response terminal

Abstract

The actual response output is reduced to two concrete finite split towers and a terminal finite graph relabeling.

G has finite vertex and edge types, decidable equality on both, a discrete edge topology and Essential G. pair and S carry the four arbitrary natural radii and the exact original two-table conjugacy. original bundles precisely G and hG as a Presentation. response bundles the existing countedGraph and obtains its essentiality from numbered_response_reduction; the original matrix and all counted edge numbers are unchanged.

The horizontal map is the actual numberedOutput, one-block by its literal edge-output formula. The first step uses the response output partition on the source and id on the target. splitOutput, splitRecover and response_recovery supply the changed homeomorphism and its total inverse table with radii a+c,b+d. reduce runs on the remaining sum (a+c)+(b+d), not on an assumed paired chain.

terminal prepends that actual outgoing stage to both towers. Its source and target depths are therefore k=(a+c)+(b+d+1). Its finite relabeling and terminal graph types come from the recursion. Its square is proved on every response history by the first changed square followed by the recursive square. No constructor accepts an arbitrary history-map leaf.

Combining the numbered response equation with the retained terminal square gives the original-domain equality. ConstructedTowerProfiles and ResponsePositiveShiftConsumer use that concrete terminal to produce the positive word and signed correction. OriginalPositiveWordAssembly supplies the full outgoing input identification.

Remark 1.1 (original).

Lean statement: D5/S3/ConceptDynamics/Coding/ResponseRealization/ResponseTwoSidedConsumer.original

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/ResponseTwoSidedConsumer.original (✓ std3).

Source. Repository-derived.

Commentary.

Bundles the original finite essential graph and its exact typeclass data as a Presentation. It is used by terminal, the output word, OriginalPositiveWordAssembly and the preserved original application; its fields are data, not new graph theorems.

Remark 1.2 (response).

Lean statement: D5/S3/ConceptDynamics/Coding/ResponseRealization/ResponseTwoSidedConsumer.response

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/ResponseTwoSidedConsumer.response (✓ std3).

Source. Repository-derived.

Commentary.

Bundles the exact numbered response graph with its unchanged counted edge type and essentiality from numbered_response_reduction. It is used by terminal and the output word. No new enumeration is supplied.

Remark 1.3 (terminal).

Lean statement: D5/S3/ConceptDynamics/Coding/ResponseRealization/ResponseTwoSidedConsumer.terminal

Formalization. D5/S3/ConceptDynamics/Coding/ResponseRealization/ResponseTwoSidedConsumer.terminal (✓ std3).

Source. Repository-derived.

Commentary.

Constructs the first outgoing step, the recursive tail, both concrete terminal presentations and the finite relabeling. It proves both depths and the literal all-history square. The profile and positive-word construction use this data.

References