glossary.md

Glossary

• MathGraph: a generative verification kernel and compounding verification metabolism.
• MathGraph Kernel: the layer that accepts only terminal certificates.
• LOGOS: lawful continuation under explicit verifier constraints.
• LOGOS Operator: the boundary that converts proposals into accepted or rejected certificate work.
• CuC / Continuation Under Constraint: propose, constrain, verify, promote.
• H-tilt: scheduler pressure for what to try next; never truth.
• Lawbook: persistent memory of verified primitive and derived certificates.
• Artifact Warehouse: SQLite-backed local index over external artifact files.
• DomainKernel: registered formal world with native language, host verifier, embedding kind, and trust policy.
• HostVerifier: verifier or host logic such as Isabelle/HOL, Lean, Z3, or the Python finite checker.
• SemanticEmbedding: representation of a target logic/theory in a host verifier.
• Shallow Semantic Embedding: embedding style that maps target semantics into host logic rather than implementing a full deep syntax.
• ImportedTheoryObject: imported axiom, definition, theorem, proof artifact, abstract object, proposition, term, or related formal-world node.
• ImportedTheoryRelation: typed relation between imported formal-world objects.
• AOTKernel: metadata registration of Abstract Object Theory as an Isabelle/HOL shallow semantic embedding precedent.
• Formal World: a theory/domain with native objects, relations, artifacts, and verifier trust rules.
• World-Kernel Metabolism: MathGraph's process of registering formal worlds, importing artifacts, verifying certificates, and compounding lawbook memory.
• Certificate Universe: the collection of promoted survivor certificates.
• Terminal Form Contract: accepted claims end as verified proof, refutation certificate, or named obstruction.
• Verified Proof: proof artifact accepted by a verifier.
• Refutation Certificate: artifact showing a claim fails.
• Finite Countermodel: current concrete magma refutation certificate.
• Named Obstruction: explicit residual/failure form, not a proof/refutation.
• Obstruction Atlas: indexed residual patterns and constructor pressure.
• Root Node: atom of discovery behind many certificates.
• Root Node Atlas: compressed map of load-bearing certificate motifs.
• Reason Node: atom of understanding that explains a recurring pattern.
• Reason Atlas: compressed explanations for roots and certificates.
• Certificate Factory: constructors plus verifiers plus promotion boundary.
• Constructor: builds candidate artifacts.
• Verifier: checks candidate artifacts.
• Promoter: imports only verified/revalidated terminal certificates.
• Residual: unresolved work left after construction/verification.
• Residual Membrane: boundary of unresolved cases left after current language, constructors, routes, and certificates are exhausted.
• Viability Ridge: structured high-pressure path along a residual membrane where failures remain nameable and fertile.
• Representation Elevator: movement from concrete failures up into motifs/obstructions/invariants and back down into constructors/certificates.
• Phase Gate: root-node location where a representation change turns stubborn residuals into constructible certificates or named obstructions.
• Root Spine: connected chain of persistent roots along a viability ridge.
• Shadow Duplication: repeated views or aliases of the same support pillar that can make support look stronger than it is.
• Effective Filtration Count: filtration support after overlap, shadow, and duplicate-evidence discounting.
• Null Lift: evidence that a candidate performs above null or background expectation.
• Route Plasticity: advisory update of route pressure from successes, failures, near misses, and replay outcomes.
• Replay Engine: system for reattempting constructor families near residuals to test reusable certificate production.
• Support Pillar: persistent load-bearing root candidate whose consequences compress residuals or generate certificate pressure.
• Better-shaped unknown: an unknown made more nameable and constructible.
• Trust level: confidence/provenance state orthogonal to terminal form.
• Provenance type: primitive, derived, imported, or human-reviewed origin.
• Primitive certificate: directly verified/imported terminal certificate.
• Derived certificate: logical composition of verified certificates.
• Table motif: recurring finite-table behavior.
• Algebra shape: coarse structural family for a table/certificate.
• Basin: source/target structural region.
• Source weakening: derived false rule requiring replay for finite elevation.
• Target strengthening: derived false rule often preserving the seed witness.
• Certificate preservation: whether a concrete witness survives derivation.
• Replay elevation: revalidating a logical derived row as a finite certificate.
• Canonical root consolidation: merging root aliases into stable root families.
• TypedObject: a formal MathGraph object with a type expression, identity mode, and uniqueness status.
• Encoding: predication mode where an abstract object carries or characterizes a property; not truth by itself.
• Exemplification: predication mode where an object instantiates a property; still requires verifier-backed trust to be authoritative.
• Denotation status: whether a formal object or complex term denotes, is non-denoting, unknown, or blocked by free-logic guardrails.
• Language Fragment: bounded object language declared by a DomainKernel or FormalWorld.
• Paradox Guard: pre-verification metadata/check that warns or blocks unsafe term patterns.
• Theory Objectification: mapping from theory symbols, claims, witnesses, or theorems to typed MathGraph objects.
• Analytic Reading: theory-relative reading of a statement through objectified denotations.
• Reason Containment: advisory explanation scaffold for source-containing-target or countermodel-separating-target patterns.
• Hyperintensional Identity: identity policy that refuses to collapse objects merely by same extension, examples, coverage, or truth value.
• Artifact Risk: explicit risk that a host-logic or embedding artifact is not yet a target-theory certificate.
• Object-Language IR: stable container for imported term/formula text before full parsing or verification.
• Theory Registry: advisory index of axioms, definitions, theorems, proof methods, and inference rules.
• AOT Scanner: metadata-only scanner for AOT .thy / .ML declarations; it does not run Isabelle.
• Host/Object Theorem Link: explicit record connecting host theorem metadata to target-theory theorem metadata.
• LogicWorkbench: layered metadata object for managing formal worlds, embeddings, backends, benchmarks, and lifecycle state.
• Workbench Layer: L0 meta-logical substrate, L1 logic/embedding layer, L2 domain theories, or L3 applications/episodes.
• Faithfulness Assessment: bridge-safety record for an embedding; it can reduce artifact risk but does not prove arbitrary claims.
• Embedding Strategy Profile: explicit shallow/deep/hybrid/native representation choice with automation strengths and risks.
• Logic Combination: advisory metadata for combining formal worlds or logics, including conflict policy and faithfulness status.
• Verifier Backend Profile: metadata for proof finders, model finders, certificate checkers, importers, and analyzers.
• Proof Finder Result: backend attempt record; no-proof-found is not refutation.
• Model Finder Result: backend attempt record; no-model-found is not proof.
• Benchmark Suite: regression/evidence set for a formal world or backend; benchmarks are not certificates.
• Correspondence Claim: proposed bridge between semantic condition and syntactic law, root motif and certificate family, or obstruction and blocked continuation.
• Interpretation Choice Point: explicit record of ambiguous symbol/objectification choices and selected/rejected readings.
• Proof Motif: repeated TRUE-side proof shape; advisory unless backed by verified proof artifacts.
• Proof Motif Atlas: compressed index of TRUE proof motifs and their support.
• Lemma Candidate: proposed reusable cut or theorem skeleton; not authoritative until verified.
• Cut Introduction: proof-shaping move that proposes an intermediate lemma for Lean to validate.
• Lean Artifact: theorem/proof/sketch metadata; generated sketches are not Lean verification.
• Lean Skeleton: conservative generated .lean text for a candidate lemma, marked advisory until checked.