Literal-input AC0 gates as bounded normal forms

A bottom AND or OR gate reads a finite family of signed input literals. Equal duplicates are harmless, while opposite occurrences of one variable make the conjunction false and the disjunction true. This module converts those cases symbolically to a DNF or CNF and proves semantic correctness and a width bound by the original fan-in.

The representative literal stored for each input coordinate is selected only at proof level. No truth-table enumeration or optimal-form search is defined.

def Algebraic.AC0.LiteralFamily.Compatible {literalCount n : ℕ} (literals : Fin literalCount → Literal n) : Prop

No coordinate occurs with two different satisfying values.

Equations

• Algebraic.AC0.LiteralFamily.Compatible literals = ∀ (left right : Fin literalCount), (literals left).index = (literals right).index → (literals left).value = (literals right).value

@[instance_reducible]

instance Algebraic.AC0.LiteralFamily.compatibleDecidable {literalCount n : ℕ} (literals : Fin literalCount → Literal n) : Decidable (Compatible literals)

Compatibility of a finite literal family is decidable.

Equations

• Algebraic.AC0.LiteralFamily.compatibleDecidable literals = id inferInstance

noncomputable def Algebraic.AC0.LiteralFamily.requirements {literalCount n : ℕ} (literals : Fin literalCount → Literal n) : PartialAssignment n

Partial assignment obtained by choosing the value of one occurrence of each coordinate. Its semantic specifications assume compatibility.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.AC0.LiteralFamily.toLiteralSet {literalCount n : ℕ} (literals : Fin literalCount → Literal n) : LiteralSet n

Literal set carried by the representative partial assignment.

Equations

• Algebraic.AC0.LiteralFamily.toLiteralSet literals = { requirements := Algebraic.AC0.LiteralFamily.requirements literals }

theorem Algebraic.AC0.LiteralFamily.requirements_eq_some_iff {literalCount n : ℕ} (literals : Fin literalCount → Literal n) (compatible : Compatible literals) (index : Fin n) (value : Bool) : requirements literals index = some value ↔ ∃ (argument : Fin literalCount), (literals argument).index = index ∧ (literals argument).value = value

For a compatible family, the representative assignment contains exactly the input literals occurring in the family.

theorem Algebraic.AC0.LiteralFamily.support_toLiteralSet_subset {literalCount n : ℕ} (literals : Fin literalCount → Literal n) : (toLiteralSet literals).support ⊆ Finset.image (fun (argument : Fin literalCount) => (literals argument).index) Finset.univ

Every coordinate in the representative literal set occurs in the source family.

theorem Algebraic.AC0.LiteralFamily.width_toLiteralSet_le {literalCount n : ℕ} (literals : Fin literalCount → Literal n) : (toLiteralSet literals).width ≤ literalCount

Collapsing repeated coordinates cannot make width exceed fan-in.

theorem Algebraic.AC0.LiteralFamily.term_satisfiedBy_toLiteralSet_iff {literalCount n : ℕ} (literals : Fin literalCount → Literal n) (compatible : Compatible literals) (input : Fin n → Bool) : Term.SatisfiedBy (toLiteralSet literals) input ↔ ∀ (argument : Fin literalCount), input (literals argument).index = (literals argument).value

A compatible family and its representative term have the same conjunctive semantics.

theorem Algebraic.AC0.LiteralFamily.clause_satisfiedBy_toLiteralSet_iff {literalCount n : ℕ} (literals : Fin literalCount → Literal n) (compatible : Compatible literals) (input : Fin n → Bool) : Clause.SatisfiedBy (toLiteralSet literals) input ↔ ∃ (argument : Fin literalCount), input (literals argument).index = (literals argument).value

A compatible family and its representative clause have the same disjunctive semantics.

theorem Algebraic.AC0.LiteralFamily.exists_conflict_of_not_compatible {literalCount n : ℕ} (literals : Fin literalCount → Literal n) (notCompatible : ¬Compatible literals) : ∃ (left : Fin literalCount) (right : Fin literalCount), (literals left).index = (literals right).index ∧ (literals left).value ≠ (literals right).value

Failure of compatibility supplies two opposite occurrences of one coordinate.

theorem Algebraic.AC0.LiteralFamily.not_all_satisfied_of_not_compatible {literalCount n : ℕ} (literals : Fin literalCount → Literal n) (notCompatible : ¬Compatible literals) (input : Fin n → Bool) : ¬∀ (argument : Fin literalCount), input (literals argument).index = (literals argument).value

An incompatible literal family cannot be satisfied conjunctively.

theorem Algebraic.AC0.LiteralFamily.exists_satisfied_of_not_compatible {literalCount n : ℕ} (literals : Fin literalCount → Literal n) (notCompatible : ¬Compatible literals) (input : Fin n → Bool) : ∃ (argument : Fin literalCount), input (literals argument).index = (literals argument).value

Every input satisfies some literal in an incompatible family.

noncomputable def Algebraic.AC0.LiteralFamily.conjunction {literalCount n : ℕ} (literals : Fin literalCount → Literal n) : DNF n

A literal-input AND gate as a DNF: one term when compatible, otherwise constant false.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.AC0.LiteralFamily.disjunction {literalCount n : ℕ} (literals : Fin literalCount → Literal n) : CNF n

A literal-input OR gate as a CNF: one clause when compatible, otherwise constant true.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.AC0.LiteralFamily.conjunction_eval {literalCount n : ℕ} (literals : Fin literalCount → Literal n) (input : Fin n → Bool) : (conjunction literals).eval input = interpretation (Op.and literalCount) fun (argument : Fin (signature.Arity (Op.and literalCount))) => (literals argument).eval input

The DNF conversion computes the original unbounded conjunction.

theorem Algebraic.AC0.LiteralFamily.disjunction_eval {literalCount n : ℕ} (literals : Fin literalCount → Literal n) (input : Fin n → Bool) : (disjunction literals).eval input = interpretation (Op.or literalCount) fun (argument : Fin (signature.Arity (Op.or literalCount))) => (literals argument).eval input

The CNF conversion computes the original unbounded disjunction.

theorem Algebraic.AC0.LiteralFamily.conjunction_widthAtMost {literalCount n : ℕ} (literals : Fin literalCount → Literal n) : (conjunction literals).WidthAtMost literalCount

The conjunction DNF has width at most the gate fan-in.

theorem Algebraic.AC0.LiteralFamily.disjunction_widthAtMost {literalCount n : ℕ} (literals : Fin literalCount → Literal n) : (disjunction literals).WidthAtMost literalCount

The disjunction CNF has width at most the gate fan-in.